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

1 files changed, 2 insertions, 11 deletions

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();