| 8 | | * AndExpression: set of OrSExpression |
| 9 | | * OrSExpression: set of BasicSExpression: |
| 10 | | * BasicSExpression: RelationalSExpression or PrimitiveSExpression or !PrimitiveSExpression |
| 11 | | * RelationalSExpression |
| 12 | | ** e>0, e>=0, e=0, e!=0, where e is a PolynomialSExpression |
| 13 | | * PrimitiveSExpression |
| 14 | | ** X, where X has boolean type |
| 15 | | ** a[e], where element type of a is boolean |
| 16 | | ** r.f, where r.f has boolean type |
| | 8 | * SAndExpression |
| | 9 | * clauses: set of SOrExpression |
| | 10 | * SOrExpression |
| | 11 | * clauses: set of SBasicExpression |
| | 12 | * SBasicExpression: SRelationalExpression or SPrimitiveExpression or !SPrimitiveExpression of boolean type |
| | 13 | * SRelationalExpression |
| | 14 | * e>0, e>=0, e=0, e!=0, where e is an SPolynomialExpression |
| | 15 | * SPrimitiveExpression |
| | 16 | * X, where X is a symbolic constant |
| | 17 | * a[e], a is an SExpression of array type, e an SExpression of integer type |
| | 18 | * r.f, where r is an SExpression of tuple type and f is a nonnegative integer |
| | 19 | * SPolynomialExpression |
| | 20 | * terms: set of SMonomialExpression |
| | 21 | * SMonomialExpression |
| | 22 | * coefficient: Number |
| | 23 | * factors: set of pairs (SPrimitiveExpression, n), where n is a positive integer |
| | 24 | * SRationalExpression |
| | 25 | * numerator, denominator: SPolynomialExpression |
| | 26 | |
| | 27 | Numbers |
| | 28 | |
| | 29 | Infinite-precision rational number. |
