The Input

The following is an example program input:

[x, y]

EXISTS [z] [[-2, 2]] [ x^2+y^2+z^2<=1 /\ y>=x^2 ];

[[-2,2], [-2,2]]

EXISTS [z] [[-2, 2]] [ x^2+y^2+z^2<=1 /\ y>=x^2 ];

[[-2,2], [-2,2]]

The three elements represent the following objects:

- the variables that span the solution space (i.e., free variables),
- the quantified constraint ∃z ∈ [-2,2][x
^{2}+ y^{2}+ z^{2}≤ 1 ∧ y ≥ x^{2}], - a box (i.e., Cartesian product of closed intervals) of the same dimension as the free variables.

In general, the representation of the input constraint can contain the following symbols:

- Quantifiers:
- FORALL, EXISTS
- Connectives:
- \ /, / \ , ==>
- Predicates:
- <, <=, >, >=
- Function Symbols:
- *, +, , SIN, COS, EXP, ASIN, ACOS, ATAN, LOG
- Constants:
- floating point numbers, PI, E
- Variables:
- lowercase alphanumeric strings starting with a letter

All binary symbols are infix, and all other prefix. One can use parenthesis for the term structure and brackets for the logical structure. Quantifiers have three arguments:

- a list of quantified variables,
- a floating point bounding box on these variables, and
- the quantified constraint.

Note that quantifiers bind stronger than connectives. Hence the input

EXISTS [x] [[ 1,3 ]] x>0 /\ x<2;

will result in the error message that the variable x cannot be found. Using brackets, arriving at

EXISTS [x] [[ 1,3 ]] [ x>0 /\ x<2 ];

solves the problem.

Although the software also allows equality predicates = it currently is not able to deduce positive information for them. Work on constraints with equalities is in progress.

Trigonometric functions expect their input in radians.