# The IDP Language¶

## Overview¶

The IDP language is used to create knowledge bases. An IDP program is made of the following blocks of code:

- vocabulary
specify the types, predicates, functions and constants used to describe the problem domain.

- theory
specify the definitions and constraints satisfied by any solutions.

- structure
(optional) specify the interpretation of some predicates, functions and constants.

- display
(optional) configure the user interface of the Interactive Consultant

The basic skeleton of an IDP knowledge base is thus as follows:

```
vocabulary {
// here comes the specification of the vocabulary
}
theory {
// here comes the definitions and constraints
}
structure {
// here comes the interpretation of some symbols
}
display {
// here comes the configuration of the user interface
}
```

Everything between `//`

and the end of the line is a comment.

## Environment¶

Often, some elements of a problem instance are under the control of the user (possibly indirectly), while others are not.

To capture this difference, the IDP language allows the creation of 2 vocabularies and 2 theories. The first one is called ‘environment’, the second ‘decision’. Hence, a more advanced skeleton of an IDP knowledge base is:

```
vocabulary environment {
// here comes the specification of the vocabulary to describe the environment
}
vocabulary decision {
extern vocabulary environment
// here comes the specification of the vocabulary to describe the decisions and their consequences
}
theory environment:environment {
// here comes the definitions and constraints satisfied by any environment possibly faced by the user
}
theory decision:decision {
// here comes the definitions and constraints to be satisfied by any solution
}
structure {
// here comes the interpretation of some symbols
}
display {
// here comes the configuration of the user interface
}
```

## Vocabulary¶

```
vocabulary V {
// here comes the vocabulary named V
}
```

The vocabulary block specifies the types, predicates, functions and constants used to describe the problem domain. Each declaration goes on a new line (or are space separated).

Symbols begins with an alphabetic character or `_`

, followed by alphanumeric characters or `_`

.
Symbols can also be string literals delimited by `'`

, e.g., `'blue planet'`

.

### Types¶

IDP-Z3 has the following built-in types: `bool`

, `int`

, `real`

, ``Symbols`

.

Custom types can be defined by specifying a range of numeric literals, or a list of constructors (of arity 0).

```
type side = {1..4}
type color constructed from {red, blue, green}
```

### Functions¶

A function with name `MyFunc`

, input types `T1`

, `T2`

, `T3`

and output type `T`

, is declared by:

```
MyFunc(T1, T2, T3) : T
```

IDP-Z3 does not support partial functions.

### Predicates¶

A predicate with name `MyPred`

and argument types `T1`

, `T2`

, `T3`

is declared by:

```
MyPred(T1, T2, T3)
```

### Propositions and Constants¶

A proposition is a predicate of arity 0; a constant is a function of arity 0.

```
MyProp1 MyProp2.
MyConstant: int
```

### Symbols type¶

The type ``Symbols`

has one constructor for each function/predicate/constant declared in the vocabulary.
For the above example, the constructors of ``Symbols`

are : ``MyFunc`

, ``MyPred`

, ``MyProp1`

, ``MyProp1`

, ``MyConst`

.

### Vocabulary annotations¶

To improve the display of functions and predicates in the Interactive Consultant,
they can be annotated with their intended meaning, a short comment, or a long comment.
These annotations are enclosed in `[`

and `]`

, and come before the symbol declaration.

- Intended meaning
`[this is a text]`

specifies the intended meaning of the symbol. This text is shown in the header of the symbol’s box.- Short info
`[short:this is a short comment]`

specifies the short comment of the symbol. This comment is shown when the mouse is over the info icon in the header of the symbol’s box.- Long info
`[long:this is a long comment]`

specifies the long comment of the symbol. This comment is shown when the user clicks the info icon in the header of the symbol’s box.

### Include another vocabulary¶

A vocabulary W may include a previously defined vocabulary V:

```
vocabulary W {
extern vocabulary V
// here comes the vocabulary named V
}
```

## Theory¶

```
theory T:V {
// here comes the theory named T, on vocabulary named V
}
```

A *theory* is a set of constraints and definitions to be satisfied.
Before explaining their syntax, we need to introduce the concept of term.

### Mathematical expressions and Terms¶

A *term* is inductively defined as follows:

- Numeric literal
Numeric literals that follow the Python conventions are numerical terms of type

`int`

or`real`

.- Constructor
Each constructor of a type is a term having that type.

- Constant
a constant is a term whose type is derived from its declaration in the vocabulary.

- Function application
\(F(t_1, t_2,.., t_n)\) is a term, when \(F\) is a function symbol of arity \(n\), and \(t_1, t_2,.., t_n\) are terms. Each term must be of the appropriate type, as defined in the function declaration in the vocabulary. The resulting type of the function application is also defined in the function declaration.

- Negation
-\(t\) is a numerical term, when \(t\) is a numerical term.

- Arithmetic
\(t_1 ꕕ t_2\) is a numerical term, when \(t_1\), \(t_2\) are two numerical terms, and \(ꕕ\) is one of the following math operators \(+, -, *, /, \hat{}, \%\). Mathematical operators can be chained as customary (e.g. \(x+y+z\)). The usual order of binding is used.

- Parenthesis
(\(t\)) is a term, when \(t\) is a term

- Cardinality aggregate
\(\#\{v_1[typeOfV_1] .. v_n[typeOfV_n] : \phi\}\) is a numerical term when \(v_1 v_2 .. v_n\) are variables, and \(\phi\) is a sentence containing these variables.

The term denotes the number of tuples of distinct values for \(v_1 v_2 .. v_n\) which make \(\phi\) true.

- Arithmetic aggregate
\(ꕕ\{v_1[typeOfV_1] .. v_n[typeOfV_n] : \phi : t\}\) is a numerical term when \(ꕕ\) is \(sum\), \(v_1 v_2 .. v_n\) are variables, \(\phi\) is a sentence, and \(t\) is a term.

The term denotes the sum of \(t\) for each distinct tuple of values for \(v_1 v_2 .. v_n\) which make \(\phi\) true.

- Variable
a variable is a term. Its type is derived from the quantifier expression that declares it (see below).

### Sentences and constraints¶

A *constraint* is a sentence followed by `.`

.
A *sentence* is inductively defined as follows:

- true and false
`true`

and`false`

are sentences.

- Predicate application
\(P(t_1, t_2,.., t_n)\) is a sentence, when \(P\) is a predicate symbol of arity \(n\), and \(t_1, t_2,.., t_n\) are terms. Each term must be of the appropriate type, as defined in the predicate declaration. If the arity of \(P\) is 0, i.e., if \(P\) is a proposition, then \(P\) and \(P()\) are sentences.

- Comparison
\(t_1 ꕕ t_2\) is a sentence, when \(t_1\), \(t_2\) are two numerical terms and \(ꕕ\) is one of the following comparison operators \(<, ≤, =, ≥, >, ≠\) (or, using ascii characters: \(=<, >=, \sim=\)). Comparison operators can be chained as customary.

- Negation
\(\lnot\) \(\phi\) is a sentence (or, using ascii characters: \(\sim \phi\)) when \(\phi\) is a sentence.

- Logic connectives
\(\phi_1 ꕕ \phi_2\) is a sentence when \(\phi_1, \phi_2\) are two sentences and \(ꕕ\) is one of the following logic connectives \(\lor, \land, \Rightarrow, \Leftarrow, \Leftrightarrow\) (or using ascii characters: \(|, \&, =>, <=, <=>\) respectively). Logic connectives can be chained as customary.

- Parenthesis
(\(\phi\)) is a sentence when \(\phi\) is a sentence.

- Quantified formulas
*Quantified formulas*are sentences. They have one of these two forms, where \(v_1, .., v_n\) are variables and \(\phi\) is a sentence:\[ \begin{align}\begin{aligned}\exists v_1[typeOfV_1] .. v_n[typeOfV_n]: \phi\\\forall v_1[typeOfV_1] .. v_n[typeOfV_n]: \phi\end{aligned}\end{align} \]Alternatively, ascii characters can be used:

`?`

,`!`

, respectively. For example,`!x[int] y[int]: f(x,y)=f(y,x).`

A variable may only occur in the \(\phi\) sentence of a quantifier declaring that variable.

### Definitions¶

A *definition* defines concepts, i.e. predicates or functions, in terms of other concepts.
A definition consists of a set of rules, enclosed by `{`

and `}`

.

*Rules* have one of the following forms:

where P is a predicate symbol, F is a function symbol, \(t\), \(t_1, t_2,.., t_n\) are terms that may contain the variables \(v_1 v_2 .. v_n\) and \(\phi\) is a formula that may contain these variables.
\(P(t_1, t_2,.., t_n)\) is called the *head* of the rule and \(\phi\) the *body*.
`<-`

can be used instead of ‘\(\leftarrow\)’.
If the body is `true`

, the left arrow and body of the rule can be omitted.

## Structure¶

A *structure* specifies the interpretation of some predicates and functions.
A structure is a set of enumerations, having one of the following forms:

where \(P\) is a predicate of arity \(n\), \(F\) is a function of arity \(n\), and \(el_i^j\) are constructors or numeric literals. For function \(F\), \(el_i^n\) specify the values of the function for the preceding tuple of \(el_i^j\) arguments, and the element after \(else\) specifies the value of the function for non-enumerated tuples of arguments.

## Display¶

The *display block* configures the user interface of the Interactive Consultant.
It consists of a set of *display facts*, i.e., predicate and function applications terminated by `.`

.

The following predicates and functions are available:

- expand
\(expand(s_1, .., s_n)\) specifies that symbols \(s_1, .., s_n\) are shown expanded, i.e., that all sub-sentences of the theory where they occur are shown on the screen.

For example,

`expand(`Length).`

will force the Interactive Consultant to show all sub-sentences containing Length.- hide
\(hide(s_1, .., s_n)\) specifies that symbols \(s_1, .., s_n\) are not shown on the screen.

For example,

`hide(`Length).`

will force the Interactive Consultant to not display the box containing Length information.- view
`view = normal.`

(default) specifies that symbols are displayed in normal mode.`view = expanded.`

specifies that symbols are displayed expanded.- relevant
\(relevant(s_1, .., s_n)\) specifies that symbols \(s_1, .., s_n\) are relevant, i.e. that they should never be greyed out.

Irrelevant symbols and sub-sentences, i.e. symbols whose interpretation do not constrain the interpretation of the relevant symbols, are greyed out by the Interactive Consultant.

- goal
\(goal(s)\) specifies that symbols \(s\) is a goal, i.e. that it is relevant and shown expanded.

- moveSymbols
When the

*display block*contains`moveSymbols.`

, the Interactive Consultant is allowed to change the layout of symbols on the screen, so that relevant symbols come first.By default, the symbols do not move.