Input Syntax

Input Syntax

Quantified constraints can contain the following symbols:

Quantifiers:

FORALL, EXISTS

Connectives:

~, \/, /\, ==>, <==>, not, and, or, implies, iff

Predicates:

<, <=, >, >=

Functions:

*, +

Constants:

Integers, floating point intervals

Variables:

All alphanumeric symbols are prefix and use functional notation (i.e., arguments in parenthesis), the other symbols are infix. Quantifiers have three arguments:

1. A list of quantified variables
2. A floating point bounding box on these variables
3. The quantified constraint

Although the software also allows equality predicates = it currently does not produce satisfying answers. Work on constraints with equalities is in progress.

Input Syntax