Chapter 3
The Input

The following is an example program input:

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² + 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

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

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

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.