= Symbolic Expressions =

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

== Interface ==

These are the items exported by the symbolic module:
 * SymbolicExpressionIF
 * SymbolicConstantIF
 * ArrayReadIF
 * TupleReadIF
 * ArrayWriteIF
 * TupleWriteIF
 * ???
 * SymbolicUniverseIF
  




== SExpression implements SymbolicExpressionIF ==

a canonical-form based implementation of symbolic expression

 * SAndExpression extends SExpression
    * clauses: set of SOrExpression
 * SOrExpression extends SExpression
    * clauses: set of SBasicExpression
 * SBasicExpression extends SExpression
    * SRelationalExpression, or
    * SPrimitiveExpression, where SPrimitiveExpression has boolean type, or
    * !SPrimitiveExpression
 * SRelationalExpression extends SExpression
   * e>0, e>=0, e=0, e!=0, where e is an SPolynomialExpression
 * SPrimitiveExpression extends SExpression
   * 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 extends SExpression
    * terms: set of SMonomialExpression
 * SMonomialExpression extends SExpression
    * coefficient: Number
    * factors: set of pairs (SPrimitiveExpression, n), where n is a positive integer
 * SRationalExpression extends SExpression
    * numerator, denominator: SPolynomialExpression

Numbers

Infinite-precision rational number.

== SExpressionFactory ==

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


== SExpressionUniverse implements SymbolicUniverseIF ==

uses SExpressionFactory

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