# IDP4 playground

### Open Source Your Knowledge, Become a Contributor

Technology knowledge has to be shared and made accessible for free. Join the movement.

## First Steps: IDP4 as a calculator

### Sums

Let's see how we can use IDP4 as a calculator. We can define an identifier like `x`

to be a numeric value like `4+5`

as:
`x := 4 + 5.`

Don't forget the dot at the end (every statement ends with it)

You didn't write a constraint which uses your newly defined `x`

. As a result of this, IDP4 thinks you can't be interested in this as it tries to prune as much things away as possible.
If you don't want to write a constraint about `x`

, we can use the library function `relevant`

to cheat our way out of this. Now we can write down a working example:

The standard operations +/*- are available. Take care that the division operator is integer division, so it truncates.
Also the `abs`

function is available which takes the absolute value of a number.

### Multiple symbols

It is possible to define multiple symbols and use one to define another. The order of your statements is irrelevant. Now we can define `y`

to be the double of `x`

.

### Symbols with local scopes

Sometimes it will be useful to introduce a symbol locally, for example when you want to reuse the result of a complex expression multiple times. This can be done with the *let*-construct. You could for instance use a let-construct to simplify the expression `(3+4)*2+(3+4)`

to `let y:=3+4 in y*2+y`

. This helps the readability of your expressions. You can also introduce multiple new symbols in a let-construct if you separate them with a semicolon. The order in which these symbols are introduced again does not matter.

A let-construct can introduce *shadowing*. When you locally define an identifier which was in scope already. The outer-scoped one is hidden and unreachable in the inner expressions.

### The other way around

Unlike simple calculators, IDP4 allows you to solve equations with multiple solutions. For this we use variables that can take a range of possible values, and constraints (equations) over these variables.

Declaring a ranged variable is done through `name :: element of setExpression`

. For now we only introduce two kinds of sets (ranges):

- Contiguous ranges of integers. A range from
`a`

to`b`

can be written down as`{a..b}`

. - Enumerations. The enumeration of a few constants like
`{1,2,8,6}`

.

Then, you can write down the constraints which should hold. All global variables occurring in a constraint are considered relevant, so we do not have to explicitly state this anymore.

Using constraints, it possible to have multiple results. By default all possible results are printed. If you want to override this you can use the statement `nbModels n`

at the top of your file, where the `n`

represents the number of solutions you are interested in. If you set `n`

to `0`

it means that you are interested in all solutions.

Note that for constraints we use the equals symbol `=`

instead of the definitional equality `:=`

.

#### Optimization

When there are multiple solutions it is possible that you're interested in an optimal one according to a certain criterion. For this you can add an optimization statement: `$minimize`

or `$maximize`

with a term which needs to be optimized.

In this case multiple solutions will still be printed. But each subsequent solution is guaranteed to be better than the previous one.

### More than numbers

#### Strings

IDP4 also supports strings between double quotes wherever you write a number. The standard lexicographic order applies when comparing strings.

#### Booleans

The Boolean values `true`

and `false`

are available through the standard library. You can introduce a Boolean variable as a proposition through `p :: proposition`

.
This behaves just like `p :: element of {true,false}`

, but it allows for a more efficient implementation.
Constraints over propositions can be written with logical connectives `|`

(or), `&`

(and), `~`

(not), `=>`

`<=`

(implies), `<=>`

(if and only if).