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:

- A list of quantified variables
- A floating point bounding box on these variables
- 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 |