- 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, 17 insertions, 10 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index cc80e2dd8..941394138 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -30,8 +30,6 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
-arith::ArithConstants* ArithRewriter::s_constants = NULL;
-
 bool isVariable(TNode t){
   return t.getMetaKind() == kind::metakind::VARIABLE;
 }
@@ -52,7 +50,11 @@ RewriteResponse ArithRewriter::rewriteVariable(TNode t){
 RewriteResponse ArithRewriter::rewriteMinus(TNode t, bool pre){
   Assert(t.getKind()== kind::MINUS);
 
-  if(t[0] == t[1]) return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE);
+  if(t[0] == t[1]){
+    Rational zero(0);
+    Node zeroNode  = mkRationalNode(zero);
+    return RewriteResponse(REWRITE_DONE, zeroNode);
+  }
 
   Node noMinus = makeSubtractionNode(t[0],t[1]);
   if(pre){
@@ -121,17 +123,19 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode t){
   // Rewrite multiplications with a 0 argument and to 0
   Integer intZero;
 
+  Rational qZero(0);
+
   for(TNode::iterator i = t.begin(); i != t.end(); ++i) {
     if((*i).getKind() == kind::CONST_RATIONAL) {
-      if((*i).getConst<Rational>() == s_constants->d_ZERO) {
-        return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE);
+      if((*i).getConst<Rational>() == qZero) {
+        return RewriteResponse(REWRITE_DONE, mkRationalNode(qZero));
       }
     } else if((*i).getKind() == kind::CONST_INTEGER) {
       if((*i).getConst<Integer>() == intZero) {
         if(t.getType().isInteger()) {
           return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(intZero));
         } else {
-          return RewriteResponse(REWRITE_DONE, s_constants->d_ZERO_NODE);
+          return RewriteResponse(REWRITE_DONE, mkRationalNode(qZero));
         }
       }
     }
@@ -222,7 +226,8 @@ RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){
   }else{
     //Transform this to: (left - right) |><| 0
     Node diff = makeSubtractionNode(left, right);
-    Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, s_constants->d_ZERO_NODE);
+    Rational qZero(0);
+    Node reduction = NodeManager::currentNM()->mkNode(atom.getKind(), diff, mkRationalNode(qZero));
     return RewriteResponse(REWRITE_AGAIN_FULL, reduction);
   }
 }
@@ -246,7 +251,8 @@ RewriteResponse ArithRewriter::preRewriteAtom(TNode atom){
 
     //Transform this to: (left - right) |><| 0
     Node diff = makeSubtractionNode(left, right);
-    reduction = currNM->mkNode(atom.getKind(), diff, s_constants->d_ZERO_NODE);
+    Rational qZero(0);
+    reduction = currNM->mkNode(atom.getKind(), diff, mkRationalNode(qZero));
   }
 
   if(reduction.getKind() == kind::GT){
@@ -291,7 +297,8 @@ RewriteResponse ArithRewriter::preRewrite(TNode t){
 }
 
 Node ArithRewriter::makeUnaryMinusNode(TNode n){
-  return NodeManager::currentNM()->mkNode(kind::MULT,s_constants->d_NEGATIVE_ONE_NODE,n);
+  Rational qNegOne(-1);
+  return NodeManager::currentNM()->mkNode(kind::MULT, mkRationalNode(qNegOne),n);
 }
 
 Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){
@@ -311,7 +318,7 @@ RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){
 
   const Rational& den = right.getConst<Rational>();
 
-  Assert(den != s_constants->d_ZERO);
+  Assert(den != Rational(0));
 
   Rational div = den.inverse();