= 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.

== SExpressionFactory ==

 * SExpression symbolicConstant()
 * SAndExpression and(Collection<SOrExpression>)
 * SOrExpression or(Collection<SBasicExpression>)
etc.


== SymbolicUniverse ==

 * SExpression symbolicConstant()
 * SExpression and(SExpression,SExpression);
 * SExpression or(SExpression,SExpression);
etc.