= Symbolic Expressions =

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

== Interface ==

These are the items exported by the symbolic module:

In symbolic.type:
 * SymbolicTypeIF
 * SymbolicPrimitiveTypeIF /* int, real, boolean */
 * SymbolicArrayTypeIF
    * SymbolicExpressionIF extent();
    * SymbolicExpressionIF elementType();
 * SymbolicTupleTypeIF
    * int numFields();
    * SymbolicTypeIF fieldType(int index);
 * SymbolicFunctionTypeIF
    * int numInputs();
    * SymbolicTypeIF inputType(int index);
    * SymbolicTypeIF outputType();

In symbolic.expression:
 * SymbolicExpressionIF
    * int id(); /* every expression has a unique id number */
    * SymbolicTypeIF type();
 * SymbolicConstantIF extends SymbolicExpressionIF
 * ConcreteExpressionIF extends SymbolicExpressionIF
    * Rational value();
 * SymbolicFunctionIF extends SymbolicConstantIF
    * SymbolicFunctionTypeIF type();
 * SymbolicEvaluatedFunctionIF extends SymbolicExpressionIF
    * SymbolicFunctionIF function();
    * SymbolicExpressionIF argument(int index);
    * SymbolicExpressionIF[] arguments();

In symbolic:
 * SymbolicUniverseIF
    * SymbolicPrimitiveTypeIF booleanType();
    * SymbolicPrimitiveTypeIF integerType();
    * SymbolicPrimitiveTypeIF realType();
    * SymbolicArrayTypeIF arrayType(SymbolicTypeIF elementType, SymbolicExpressionIF extent);
    * SymbolicTupleTypeIF tupleType(SymbolicTypeIF[] fieldTypes);
    * ConcreteExpressionIF concreteExpression(Rational rational);
    * ConcreteExpressionIF concreteExpression(int value);
    * ConcreteExpressionIF concreteExpression(double value);
    * SymbolicConstantIF symbolicConstant(SymbolicTypeIF type, String name);
    * SymbolicExpressionIF add(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    * SymbolicExpressionIF subtract(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    * SymbolicExpressionIF multiply(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    * SymbolicExpressionIF divide(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    * SymbolicExpressionIF minus(SymbolicExpressionIF arg);
    * SymbolicExpressionIF and(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    * SymbolicExpressionIF or(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    * SymbolicExpressionIF not(SymbolicExpressionIF arg);
    * SymbolicExpressionIF cond(SymbolicExpressionIF predicate, SymbolicExpressionIF trueValue, SymbolicExpressionIF falseValue);
    * SymbolicExpressionIF lessThan(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    * SymbolicExpressionIF lessThanEquals(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    * SymbolicExpressionIF equals(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1);
    * SymbolicExpressionIF arrayRead(SymbolicExpressionIF array, SymbolicExpressionIF index);
    * SymbolicExpressionIF arrayWrite(SymbolicExpressionIF array, SymbolicExpressionIF index, SymbolicExpressionIF value);
    * SymbolicExpressionIF tupleRead(SymbolicExpressionIF tuple, int index);
    * SymbolicExpressionIF tupleWrite(SymbolicExpressionIF tuple, int index, SymbolicExpressionIF value);
 * SymbolicSimplifierIF
    * SymbolicExpressionIF newAssumption();
    * SymbolicExpressionIF simplify(SymbolicExpressionIF expression);
 
  
In util wee need to export:
* Rational /* infinite precision rational numbers */
   * static Rational rational(int value);
   * static Rational rational(double value);
   * static Rational rational(BigInteger value);
   * static Rational add(Rational arg0, Rational arg1);
   * static Rational subtract(Rational arg0, Rational arg1);
   * static Rational multiply(Rational arg0, Rational arg1);
   * static Rational divide(Rational arg0, Rational arg1);
   * static Rational minus(Rational arg);
   * static int compare(Rational arg0, Rational arg1); /* +-0 */
   * boolean isInteger();
   * Rational intValue();
   * BigInteger numerator();
   * BigInteger denominator();
   * BigInteger floor();
   * BigInteger ceil();
   * boolean isGT0();
   * boolean isGTE0();
   * boolean is0();

    





== SExpression implements SymbolicExpressionIF ==

This an implementation of the interface defined above.    The idea is to aggressively put every expression into a canonical form.

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.