# Help

## Grammar for formulae

Each formula has to be in a certain format to be recognized by the parser.

The simplified grammar for formulae looks as follows:

Formula =

Predicate **(e.g. x+y <= 13)**

**|** (Formula) **(e.g. (x+y <= 13) )**

**|** Formula (&& Formula)* **(e.g. x<=10 && y<=10)**

**|** Formula (|| Formula)* **(e.g. x<=10 || y<=10)**

**|** Formula -> Formula **(e.g. x==10 -> y<=10)**

**|** E(var)*:Formula **(e.g. Ex:x+y==5)**

**|** A(var)*:Formula **(e.g. Ax:x>=0)**

**|** &&([var=a..b])* This is a and-forall-Formula. var will be replaces by each value in the range between a and b.**(e.g. &&[i=1..4] x[i]<=i or &&[i=1..2][j=1..2] x[i] == y[j] )**

**|** ||([var=a..b])* The same as the and-forall-Formula, but with or instead of and **(e.g. ||[i=1..4] x[i]<=i)**

A variable consists of one lower-case letter. You can also define arrays, e.g. x[1].

### Examples

Ex:x+y==4

x <=10 && y<=10

## Macros

To define a Macro please go to the Macro-Tab. A Macro definition has to be of the following form:

[A-Z] [a-z]* (var(,var)*) := Formula

The first letter has to be a upper-case letter, followed be an arbitrary number of lower-case letters.

### Example

Test(x) := x==15