This commit removes the CONST_INTEGER kind from nodes. This code comes from the branch arithmetic/remove_const_int.

7 files changed, 27 insertions, 130 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 863eb5c31..d7a6c0443 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -40,9 +40,9 @@ bool ArithRewriter::isAtom(TNode n) {
 
 RewriteResponse ArithRewriter::rewriteConstant(TNode t){
   Assert(t.getMetaKind() == kind::metakind::CONSTANT);
-  Node val = coerceToRationalNode(t);
+  Assert(t.getKind() == kind::CONST_RATIONAL);
 
-  return RewriteResponse(REWRITE_DONE, val);
+  return RewriteResponse(REWRITE_DONE, t);
 }
 
 RewriteResponse ArithRewriter::rewriteVariable(TNode t){
@@ -91,27 +91,23 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
   }else if(t.getKind() == kind::UMINUS){
     return rewriteUMinus(t, true);
   }else if(t.getKind() == kind::DIVISION){
-    if(t[0].getKind()== kind::CONST_RATIONAL){
-      return rewriteDivByConstant(t, true);
-    }else{
-      return RewriteResponse(REWRITE_DONE, t);
-    }
+    return RewriteResponse(REWRITE_DONE, t); // wait until t[1] is rewritten
   }else if(t.getKind() == kind::PLUS){
     return preRewritePlus(t);
   }else if(t.getKind() == kind::MULT){
     return preRewriteMult(t);
   }else if(t.getKind() == kind::INTS_DIVISION){
-    Integer intOne(1);
-    if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){
+    Rational intOne(1);
+    if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst<Rational>() == intOne){
       return RewriteResponse(REWRITE_AGAIN, t[0]);
     }else{
       return RewriteResponse(REWRITE_DONE, t);
     }
   }else if(t.getKind() == kind::INTS_MODULUS){
-    Integer intOne(1);
-    if(t[1].getKind()== kind::CONST_INTEGER && t[1].getConst<Integer>() == intOne){
-      Integer intZero(0);
-      return RewriteResponse(REWRITE_AGAIN, mkIntegerNode(intZero));
+    Rational intOne(1);
+    if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst<Rational>() == intOne){
+      Rational intZero(0);
+      return RewriteResponse(REWRITE_AGAIN, mkRationalNode(intZero));
     }else{
       return RewriteResponse(REWRITE_DONE, t);
     }
@@ -147,8 +143,6 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode t){
   Assert(t.getKind()== kind::MULT);
 
   // Rewrite multiplications with a 0 argument and to 0
-  Integer intZero;
-
   Rational qZero(0);
 
   for(TNode::iterator i = t.begin(); i != t.end(); ++i) {
@@ -156,14 +150,6 @@ RewriteResponse ArithRewriter::preRewriteMult(TNode t){
       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, mkRationalNode(qZero));
-        }
-      }
     }
   }
   return RewriteResponse(REWRITE_DONE, t);
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 8ecc3abdc..e88ec073d 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -152,10 +152,9 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
     }
     break;
   case CONST_RATIONAL:
-  case CONST_INTEGER:
     // Mark constants as minmax
-    d_minMap[n] = coerceToRational(n);
-    d_maxMap[n] = coerceToRational(n);
+    d_minMap[n] = n.getConst<Rational>();
+    d_maxMap[n] = n.getConst<Rational>();
     break;
   case OR: {
     // Look for things like "x = 0 OR x = 1" (that are defTrue) and
@@ -193,46 +192,6 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
       break;
     }
 
-    Integer k1, k2;
-    if(c1.getType().getConst<TypeConstant>() == INTEGER_TYPE) {
-      k1 = c1.getConst<Integer>();
-    } else {
-      Rational r = c1.getConst<Rational>();
-      if(r.getDenominator() == 1) {
-        k1 = r.getNumerator();
-      } else {
-        break;
-      }
-    }
-    if(c2.getType().getConst<TypeConstant>() == INTEGER_TYPE) {
-      k2 = c2.getConst<Integer>();
-    } else {
-      Rational r = c2.getConst<Rational>();
-      if(r.getDenominator() == 1) {
-        k2 = r.getNumerator();
-      } else {
-        break;
-      }
-    }
-    if(k1 > k2) {
-      swap(k1, k2);
-    }
-    if(k1 + 1 == k2) {
-      Debug("arith::static") << "==> found " << n << endl
-                             << "    which indicates " << var << " \\in { "
-                             << k1 << " , " << k2 << " }" << endl;
-      c1 = NodeManager::currentNM()->mkConst(k1);
-      c2 = NodeManager::currentNM()->mkConst(k2);
-      Node lhs = NodeBuilder<2>(kind::GEQ) << var << c1;
-      Node rhs = NodeBuilder<2>(kind::LEQ) << var << c2;
-      Node l = lhs && rhs;
-      Debug("arith::static") << "    learned: " << l << endl;
-      learned << l;
-      if(k1 == 0) {
-        Assert(k2 == 1);
-        replaceWithPseudoboolean(var);
-      }
-    }
     break;
   }
   default: // Do nothing
@@ -466,7 +425,7 @@ void ArithStaticLearner::addBound(TNode n) {
   NodeToMinMaxMap::iterator minFind = d_minMap.find(n[0]);
   NodeToMinMaxMap::iterator maxFind = d_maxMap.find(n[0]);
 
-  Rational constant = coerceToRational(n[1]);
+  Rational constant = n[1].getConst<Rational>();
   DeltaRational bound = constant;
 
   switch(Kind k = n.getKind()) {
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index af32c3f87..fb669cce4 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -41,50 +41,12 @@ inline Node mkRationalNode(const Rational& q){
   return NodeManager::currentNM()->mkConst<Rational>(q);
 }
 
-inline Node mkIntegerNode(const Integer& z){
-  return NodeManager::currentNM()->mkConst<Integer>(z);
-}
-
 inline Node mkBoolNode(bool b){
   return NodeManager::currentNM()->mkConst<bool>(b);
 }
 
 
 
-inline Rational coerceToRational(TNode constant){
-  switch(constant.getKind()){
-  case kind::CONST_INTEGER:
-    {
-      Rational q(constant.getConst<Integer>());
-      return q;
-    }
-  case kind::CONST_RATIONAL:
-    return constant.getConst<Rational>();
-  default:
-    Unreachable();
-  }
-  Rational unreachable(0,0);
-  return unreachable;
-}
-
-inline Node coerceToRationalNode(TNode constant){
-  switch(constant.getKind()){
-  case kind::CONST_INTEGER:
-    {
-      Rational q(constant.getConst<Integer>());
-      Node n = mkRationalNode(q);
-      return n;
-    }
-  case kind::CONST_RATIONAL:
-    return constant;
-  default:
-    Unreachable();
-  }
-  return Node::null();
-}
-
-
-
 /** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
 inline bool isRelationOperator(Kind k){
   using namespace kind;
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 95d7d6ed1..e00d8dc5e 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -31,7 +31,7 @@ sort REAL_TYPE \
 sort INTEGER_TYPE \
     Cardinality::INTEGERS \
     well-founded \
-        "NodeManager::currentNM()->mkConst(Integer(0))" \
+        "NodeManager::currentNM()->mkConst(Rational(0))" \
         "expr/node_manager.h" \
     "Integer type"
 sort PSEUDOBOOLEAN_TYPE \
@@ -59,11 +59,7 @@ constant CONST_RATIONAL \
     ::CVC4::RationalHashStrategy \
     "util/rational.h" \
     "a multiple-precision rational constant"
-constant CONST_INTEGER \
-    ::CVC4::Integer \
-    ::CVC4::IntegerHashStrategy \
-    "util/integer.h" \
-    "a multiple-precision integer constant"
+
 constant CONST_PSEUDOBOOLEAN \
     ::CVC4::Pseudoboolean \
     ::CVC4::PseudobooleanHashStrategy \
@@ -83,7 +79,6 @@ typerule DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule POW ::CVC4::theory::arith::ArithOperatorTypeRule
 
 typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule
-typerule CONST_INTEGER ::CVC4::theory::arith::ArithConstantTypeRule
 
 typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule
 typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 434be42a2..d67cd46a9 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -232,7 +232,6 @@ public:
 
   // TODO: check if it's a theory leaf also
   static bool isMember(Node n) {
-    if (n.getKind() == kind::CONST_INTEGER) return false;
     if (n.getKind() == kind::CONST_RATIONAL) return false;
     if (isRelationOperator(n.getKind())) return false;
     return Theory::isLeafOf(n, theory::THEORY_ARITH);
@@ -283,7 +282,8 @@ public:
   bool isNormalForm() { return isMember(getNode()); }
 
   static Constant mkConstant(Node n) {
-    return Constant(coerceToRationalNode(n));
+    Assert(n.getKind() == kind::CONST_RATIONAL);
+    return Constant(n);
   }
 
   static Constant mkConstant(const Rational& rat) {
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index d660cb4cd..1bd3277cd 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1239,8 +1239,8 @@ Node TheoryArith::roundRobinBranch(){
     Integer floor_d = d.floor();
     Integer ceil_d = d.ceiling();
 
-    Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkIntegerNode(floor_d)));
-    Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkIntegerNode(ceil_d)));
+    Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
+    Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, mkRationalNode(ceil_d)));
 
 
     Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
@@ -1436,9 +1436,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
 
   switch(n.getKind()) {
 
-  case kind::CONST_INTEGER:
-    return Rational(n.getConst<Integer>());
-
   case kind::CONST_RATIONAL:
     return n.getConst<Rational>();
 
@@ -1456,9 +1453,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
   case kind::MULT: { // 2+ args
     Assert(n.getNumChildren() == 2 && n[0].isConst());
     DeltaRational value(1);
-    if (n[0].getKind() == kind::CONST_INTEGER) {
-      return getDeltaValue(n[1]) * n[0].getConst<Integer>();
-    }
     if (n[0].getKind() == kind::CONST_RATIONAL) {
       return getDeltaValue(n[1]) * n[0].getConst<Rational>();
     }
@@ -1478,9 +1472,6 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
     if (n[1].getKind() == kind::CONST_RATIONAL) {
       return getDeltaValue(n[0]) / n[0].getConst<Rational>();
     }
-    if (n[1].getKind() == kind::CONST_INTEGER) {
-      return getDeltaValue(n[0]) / n[0].getConst<Integer>();
-    }
     Unreachable();
 
 
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 8d0d79f0a..69c98a255 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -32,8 +32,12 @@ class ArithConstantTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
       throw (TypeCheckingExceptionPrivate, AssertionException) {
-    if (n.getKind() == kind::CONST_RATIONAL) return nodeManager->realType();
-    return nodeManager->integerType();
+    Assert(n.getKind() == kind::CONST_RATIONAL);
+    if(n.getConst<Rational>().isIntegral()){
+      return nodeManager->integerType();
+    }else{
+      return nodeManager->realType();
+    }
   }
 };/* class ArithConstantTypeRule */
 
@@ -101,12 +105,12 @@ public:
 
     const SubrangeBounds& bounds = type.getConst<SubrangeBounds>();
     if(bounds.lower.hasBound()) {
-      return NodeManager::currentNM()->mkConst(bounds.lower.getBound());
+      return NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
     }
     if(bounds.upper.hasBound()) {
-      return NodeManager::currentNM()->mkConst(bounds.upper.getBound());
+      return NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
     }
-    return NodeManager::currentNM()->mkConst(Integer(0));
+    return NodeManager::currentNM()->mkConst(Rational(0));
   }
 };/* class SubrangeProperties */