Changes between Version 2 and Version 3 of Things To Do

Timestamp:

01/23/10 16:23:02 (16 years ago)

Author:

Stephen Siegel

Comment:

--

Things To Do

@@ -1 +1 @@
 = Things To Do =
+
+== General ==
 
  * change names of MiniMP to TASS throughout project
@@ -6 +8 @@
  * achieve much better statement and branch coverage in JUnit tests
  * create separate test tree which mirrors the source tree but contains only JUnit tests
+
+== Symbolic Module ==
+
+Consider re-designing the symbolic module based on lessons learned.
+
+First, is the assumption argument necessary?   Is it ever used for anything?  How about removing it?
+
+Then we can separate entirely the code for manipulating symbolic expressions from the code responsible for proving things and simplifying expressions based on an assumption.
+
+How about multiple layers for the symbolic package:
+
+ 1.  Layer 0: Herbrand arithmetic.   No simplifications of anything.  This just produces new symbolic expressions based on the given arguments.  Straightforward factory; operator, arguments type of thing.
+ 1.  Layer 1: Very basic simplifications only, such as  x+0->x, 1*x->x, x+y->y+x.  Integers commutative/associative, etc.  All of which are applicable to IEEE arithmetic.   Place boolean expressions in canonical form, such as CNF?
+ 1.  Layer 2: rational canonical form for real expressions.  Valid for real arithmetic but does not necessarily preserve IEEE arithmetic.
+
+Each layer could implement the same interface, SymbolicUniverseIF.  
+
+Add: a SymbolicSimplifierIF interface and a TheoremProverIF interface.
+
+So, the following are the items exported by the symbolic module:
+
+ * {{{SymbolicUniverseIF}}}
+   * methods for creating and manipulating symbolic expressions
+   * {{{SymbolicExpressionIF}}} and all kinds of subtypes, operators, and so on
+ * {{{SymbolicSimplifierIF}}}
+   * see the simplifier class currently in the value package
+ * {{{TheoremProverIF}}}
+   * {{{boolean valid(BooleanSymbolicExpressionIF assumption, BooleanSymbolicExpressionIF predicate);}}}
+
+
+