Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.






Give me n solutions with n=
Give me all solutions (Warning: There can be a lot and your browser might crash!)
Minimize the term
Maximize the term

Welcome to the Solver for Presburger Arithmetics! Please enter your equation above.

Welcome to the Macro Manager! Here you ca add macros that you want to use in your formulae.




Welcome to the Solver for Presburger Arithmetics! Just Click '+' to add a equation.

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