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 */
• 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
  • 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);

• SymbolicSimplifierIF
  • SymbolicExpressionIF newAssumption();
  • SymbolicExpressionIF simplify(SymbolicExpressionIF expression);

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.