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