An Advanced Solver for Presburger Arithmetic

An Error occured. Here's what the Server said:

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