= 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();
   * BigInteger intValue();
   * BigInteger numerator();
   * BigInteger denominator();
   * BigInteger floor();
   * BigInteger ceil();
   * boolean isGT0();
   * boolean isGTE0();
   * boolean is0();

== Implementation ==

Package cexpression will implement the interface defined above.
The idea is to aggressively put every expression into a canonical form.  It assumes real arithmetic, so addition and multiplication are as in the real numbers.

Classes:

 * CExpression implements SymbolicExpressionIF
 * AndCExpression extends CExpression
    * clauses: set of OrCExpression
 * OrCExpression extends CExpression
    * clauses: set of SBasicExpression
 * BasicCExpression extends CExpression
    * RelationalCExpression, or
    * PrimitiveCExpression, where PrimitiveCExpression has boolean type, or
    * !PrimitiveCExpression
 * RelationalCExpression extends CExpression
   * e>0, e>=0, e=0, e!=0, where e is a PolynomialCExpression
 * PrimitiveCExpression extends CExpression
   * X, where X is a symbolic constant
   * a[e], a is a CExpression of array type, e a CExpression of integer type
   * r.f, where r is an CExpression of tuple type and f is a nonnegative integer
 * PolynomialCExpression extends CExpression
    * terms: set of MonomialCExpression
 * MonomialCExpression extends CExpression
    * coefficient: Rational
    * factors: set of pairs (PrimitiveCExpression, n), where n is a positive integer
 * RationalCExpression extends CExpression
    * numerator, denominator: PolynomialCExpression

=== CExpressionFactory ===

 * CExpression symbolicConstant(...)
 * AndCExpression and(Collection<OrCExpression>)
 * OrCExpression or(Collection<BasicCExpression>)
etc.


=== CExpressionUniverse implements SymbolicUniverseIF ===

uses CExpressionFactory