Symbolic Expressions

Write here your thoughts on the new design of the symbolic module

Canonical Form: SExpression

• SAndExpression
  • clauses: set of SOrExpression
• SOrExpression
  • clauses: set of SBasicExpression
• SBasicExpression: SRelationalExpression or SPrimitiveExpression or !SPrimitiveExpression of boolean type
• SRelationalExpression
  • e>0, e>=0, e=0, e!=0, where e is an SPolynomialExpression
• SPrimitiveExpression
  • X, where X is a symbolic constant
  • a[e], a is an SExpression of array type, e an SExpression of integer type
  • r.f, where r is an SExpression of tuple type and f is a nonnegative integer
• SPolynomialExpression
  • terms: set of SMonomialExpression
• SMonomialExpression
  • coefficient: Number
  • factors: set of pairs (SPrimitiveExpression, n), where n is a positive integer
• SRationalExpression
  • numerator, denominator: SPolynomialExpression

Numbers

Infinite-precision rational number.