The Input

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]]

The three elements represent the following objects:

• the variables that span the solution space (i.e., free variables),
• the quantified constraint exist z in [-2,2] [ x²+y²+z² <= 1 /\ y >= x²],
• 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

There are additional predicates calling efficient external solvers. These are documented in Section 

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:

1. a list of quantified variables,
2. a floating point bounding box on these variables, and
3. 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 does not produce satisfying answers. Work on constraints with equalities is in progress.

The Input