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

Additional Interfaces:
* PrimitiveCExpressionIF
    * classes implementing this interface
       * ArrayRead
       * ArrayWrite
       * TupleRead
       * TupleWrite
       * SymbolicConstant
       * RelationalCExpression
       * EvaluatedFunction

Classes:
 * CExpression implements SymbolicExpressionIF
 * AndCExpression extends CExpression
    * clauses: set of OrCExpression
 * OrCExpression extends CExpression
    * clauses: set of BasicCExpression
 * BasicCExpression extends CExpression
    * boolean not(); /* if true insert not here */
    * PrimitiveCExpressionIF primitiveExpression();
 * RelationalCExpression extends CExpression implements PrimitiveCExpressionIF
   * enum RelationKind { GT0, EQ0 };
   * RelationKind kind();
   * PolynomialCExpression expression();
 * 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

Some facts which show how to put any expression into this canonical form:
 * x>=y <=> !(y-x>0)
 * x<y <=> y-x>0
 * x<=y <=> !(x-y>0)

Big question: how to find command factors in denominator?
 

=== CExpressionFactory ===

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


=== CExpressionUniverse implements SymbolicUniverseIF ===

uses CExpressionFactory