- Removes arith_constants.h

- Adds ArithStaticLearner.  Consolidates and cleans up the code for static learning in arithmetic.  Static learning is now associated with a small amount of state between calls. This is used to track the data for the miplib trick.  The goal is to make this inference work without relying on the fact that all of the miplib problem is asserted under the same AND node.
- This commit contains miscellaneous other arithmetic cleanup.

1 files changed, 2 insertions, 14 deletions

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 3a8fc191a..d88a7ae92 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -23,7 +23,6 @@
 #define __CVC4__THEORY__ARITH__ARITH_REWRITER_H
 
 #include "theory/theory.h"
-#include "theory/arith/arith_constants.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
 
@@ -37,8 +36,6 @@ class ArithRewriter {
 
 private:
 
-  static arith::ArithConstants* s_constants;
-
   static Node makeSubtractionNode(TNode l, TNode r);
   static Node makeUnaryMinusNode(TNode n);
 
@@ -67,18 +64,9 @@ public:
   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 init() { }
 
-  static void shutdown() {
-    if (s_constants != NULL) {
-      delete s_constants;
-      s_constants = NULL;
-    }
-  }
+  static void shutdown() { }
 
 private: