Symbolic Expressions

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

Organization of Symbolic Module

The following directory/package structure will be used:

symbolic

• symbolic.IF: interface. All items that will be exported go in here.
  • symbolic.IF.type: types of symbolic expressions
  • symbolic.IF.expression: symbolic expressions
• symbolic.real: this is an implementation based on real-arithmetic and canonical forms.
  • symbolic.real.type
  • symbolic.real.expression
• SymbolicModule: entry point
  • public static SymbolicUniverseIF newRealUniverse();

Infinite Precision Rational Numbers

This has been added in a new package numbers. There are types IntegerNumberIF, RationalNumberIF, both of which extend NumberIF. There is a NumberFactoryIF type for creating numbers, performing operations on them, etc. There is a RealFactory implementing NumberFactoryIF which provides this perfect precision feature.

Interface to Symbolic Module

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.IF:

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

An Implementation of the Symbolic Module

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

symbolic.real.expression 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:

• f/g>0 <=> ((f>0 && g>0) || (f<0 && g<0))
• f/g=0 <=> f=0
• 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.