= Symbolic Expressions =

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

== Organization ==

The following directory/package structure will be used:
 * `symbolic.IF`: interface.  All items that will be exported go in here.
    * `symbolic.IF.type`
    * `symbolic.IF.expression`
 * `symbolic.real`: this is an implementation based on real-arithmetic and canonical forms.
    * `symbolic.real.type`
    * `symbolic.real.expression`
 * `SymbolicModule`
    * `public static SymbolicUniverseIF newRealUniverse();`

== Interface `symbolic.IF` ==

Package `symbolic.IF.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();`

Package `symbolic.IF.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();`

package `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: `symbolic.real` ==

Package `symbolic.real` 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:
 * `PrimitiveExpression`
    * these are expressions that are not formed by numerical or logical operators
    * classes implementing this interface
       * `ArrayRead`
       * `ArrayWrite`
       * `TupleRead`
       * `TupleWrite`
       * `SymbolicConstant`
       * `RelationalExpression`
       * `EvaluatedFunction`
       * `ConcreteExpression`

Classes:
 * `RealExpression implements SymbolicExpressionIF`
 * `ConcreteExpression extends RealExpression implements ConcreteExpressionIF`
 * `RealFunction extends RealExpression implements SymbolicFunctionIF`
 * `EvaluatedFunction extends RealExpression implements SymbolicEvaluatedFunctionIF`
 * `ArrayRead extends RealExpression`
 * `ArrayWrite extends RealExpression`
 * `TupleRead extends RealExpression`
 * `TupleWrite extends RealExpression`
 * `SymbolicConstant  extends RealExpression implements SymbolicConstantIF`
 * `AndExpression extends RealExpression`
    * clauses: set of `OrExpression`
 * `OrExpression extends RealExpression`
    * clauses: set of `BasicExpression`
 * `BasicExpression extends RealExpression`
    * `boolean not();` /* if true insert not operator here */
    * `PrimitiveExpression primitiveExpression();`
 * `RelationalExpression extends RealExpression implements PrimitiveExpression`
   * `enum RelationKind { GT0, EQ0 };`
   * `RelationKind kind();`
   * `Polynomial expression();`
 * `Polynomial extends RealExpression`
    * terms: set of `Monomial`
    * factorization: set of `Polynomial`
       * this is redundant information giving a factorization of the polynomial into polynomials of lower degree.  It is used for simplification.
 * `Monomial extends RealExpression`
    * coefficient: `Rational`
    * factors: set of pairs (`PrimitiveExpression X, int i`), where i>0, representing the product X_1^{i_1}...X_n^{i_n}
 * `RationalExpression extends RealExpression`
    * numerator, denominator: `Polynomial`

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)`
 * `x>y <=> x-y>0`
 * `x!=y <=> !(x=y)`
 * `!(p&&q) <=> (!p)||(!q)`
 * `(p&&q)||r <=> (p||r)&&(q||r)`
 * `!(p||q) <=> (!p)&&(!q)` 

=== `RealExpressionFactory` ===

`public class RealExpressionFactory`
 * `RealExpression symbolicConstant(...)`
 * `AndExpression and(Collection<OrExpression>)`
 * `OrExpression or(Collection<BasicExpression>)`
etc.


=== `RealUniverse implements SymbolicUniverseIF` ===

`public class RealUniverse implements SymbolicUniverseIF`
 * `RealExpression SymbolicConstant(...)`
 * `RealExpression and(SymbolicExpressionIF arg0, SymbolicExpressionIF arg1)`
etc.