Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.

1 files changed, 49 insertions, 25 deletions

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index f7ef8c0c7..e161bd8d6 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -17,10 +17,13 @@
  ** \todo document this file
  **/
 
-#include "theory/arith/arith_constants.h"
 #include "theory/theory.h"
+#include "theory/arith/arith_constants.h"
+#include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
 
+#include "theory/rewriter.h"
+
 #ifndef __CVC4__THEORY__ARITH__REWRITER_H
 #define __CVC4__THEORY__ARITH__REWRITER_H
 
@@ -28,46 +31,67 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-class ArithRewriter{
+class ArithRewriter {
+
 private:
-  ArithConstants* d_constants;
 
-  Node makeSubtractionNode(TNode l, TNode r);
-  Node makeUnaryMinusNode(TNode n);
+  static arith::ArithConstants* s_constants;
+
+  static Node makeSubtractionNode(TNode l, TNode r);
+  static Node makeUnaryMinusNode(TNode n);
 
-  RewriteResponse preRewriteTerm(TNode t);
-  RewriteResponse postRewriteTerm(TNode t);
+  static RewriteResponse preRewriteTerm(TNode t);
+  static RewriteResponse postRewriteTerm(TNode t);
 
-  RewriteResponse rewriteVariable(TNode t);
-  RewriteResponse rewriteConstant(TNode t);
-  RewriteResponse rewriteMinus(TNode t, bool pre);
-  RewriteResponse rewriteUMinus(TNode t, bool pre);
-  RewriteResponse rewriteDivByConstant(TNode t, bool pre);
+  static RewriteResponse rewriteVariable(TNode t);
+  static RewriteResponse rewriteConstant(TNode t);
+  static RewriteResponse rewriteMinus(TNode t, bool pre);
+  static RewriteResponse rewriteUMinus(TNode t, bool pre);
+  static RewriteResponse rewriteDivByConstant(TNode t, bool pre);
 
-  RewriteResponse preRewritePlus(TNode t);
-  RewriteResponse postRewritePlus(TNode t);
+  static RewriteResponse preRewritePlus(TNode t);
+  static RewriteResponse postRewritePlus(TNode t);
 
-  RewriteResponse preRewriteMult(TNode t);
-  RewriteResponse postRewriteMult(TNode t);
+  static RewriteResponse preRewriteMult(TNode t);
+  static RewriteResponse postRewriteMult(TNode t);
 
 
-  RewriteResponse preRewriteAtom(TNode t);
-  RewriteResponse postRewriteAtom(TNode t);
-  RewriteResponse postRewriteAtomConstantRHS(TNode t);
+  static RewriteResponse preRewriteAtom(TNode t);
+  static RewriteResponse postRewriteAtom(TNode t);
+  static RewriteResponse postRewriteAtomConstantRHS(TNode t);
 
 public:
-  ArithRewriter(ArithConstants* ac) : d_constants(ac) {}
 
-  RewriteResponse preRewrite(TNode n);
-  RewriteResponse postRewrite(TNode n);
+  static RewriteResponse preRewrite(TNode n);
+  static RewriteResponse postRewrite(TNode n);
+
+  static void init() {
+    if (s_constants == NULL) {
+      s_constants = new arith::ArithConstants(NodeManager::currentNM());
+    }
+  }
+
+  static void shutdown() {
+    if (s_constants != NULL) {
+      delete s_constants;
+      s_constants = NULL;
+    }
+  }
 
 private:
-  bool isAtom(TNode n) const { return isRelationOperator(n.getKind()); }
-  bool isTerm(TNode n) const { return !isAtom(n); }
+
+  static inline bool isAtom(TNode n) {
+    return arith::isRelationOperator(n.getKind());
+  }
+
+  static inline bool isTerm(TNode n) {
+    return !isAtom(n);
+  }
+
 };
 
 
-}; /* namesapce arith */
+}; /* namesapce rewrite */
 }; /* namespace theory */
 }; /* namespace CVC4 */