* New normal form for arithmetic is in place.

* src/theory/arith/normal_form.{h,cpp} contains the description for the new
  normal form as well as utilities for dealing with the normal form.
* src/theory/arith/next_arith_rewriter.{h,cpp} contains the new rewriter.
  The new rewriter implements preRewrite() and postRewrite() for arithmetic.
* src/theory/arith/arith_rewriter.{h,cpp} have been removed.
* TheoryArith::rewrite() has been removed.
* Arithmetic with the new normal form outperforms the trunk where the branch
  occurred (-r797) on 46% of the examples in QF_LRA. (33% have no noticeable
  difference.) Some important optimizations are stilling pending to the code
  for handling the new normal form. (Bug 196.)

1 files changed, 3 insertions, 8 deletions

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 7367f5726..03be7a77b 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -28,7 +28,7 @@
 
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/tableau.h"
-#include "theory/arith/arith_rewriter.h"
+#include "theory/arith/next_arith_rewriter.h"
 #include "theory/arith/partial_model.h"
 #include "theory/arith/arith_propagator.h"
 
@@ -94,7 +94,7 @@ private:
   /**
    * The rewriter module for arithmetic.
    */
-  ArithRewriter d_rewriter;
+  NextArithRewriter d_nextRewriter;
 
   ArithUnatePropagator d_propagator;
 
@@ -103,11 +103,6 @@ public:
   ~TheoryArith();
 
   /**
-   * Rewrites a node to a unique normal form given in normal_form_notes.txt
-   */
-  Node rewrite(TNode n);
-
-  /**
    * Rewriting optimizations.
    */
   RewriteResponse preRewrite(TNode n, bool topLevel);
@@ -116,7 +111,7 @@ public:
    * Plug in old rewrite to the new (pre,post)rewrite interface.
    */
   RewriteResponse postRewrite(TNode n, bool topLevel) {
-    return RewriteComplete(topLevel ? rewrite(n) : Node(n));
+    return d_nextRewriter.postRewrite(n);
   }
 
   /**