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

4 files changed, 14 insertions, 21 deletions

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 853d0086b..491f99584 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -66,8 +66,8 @@ public:
       d_apply_fun_bool = new Expr(d_em->mkExpr(APPLY_UF, *fun_op, *a_bool));
       null = new Expr;
 
-      i1 = new Expr(d_em->mkConst(Integer("0")));
-      i2 = new Expr(d_em->mkConst(Integer(23)));
+      i1 = new Expr(d_em->mkConst(Rational("0")));
+      i2 = new Expr(d_em->mkConst(Rational(23)));
       r1 = new Expr(d_em->mkConst(Rational(1, 5)));
       r2 = new Expr(d_em->mkConst(Rational("0")));
     } catch(Exception e) {
@@ -218,8 +218,8 @@ public:
     TS_ASSERT(d_apply_fun_bool->getKind() == APPLY_UF);
     TS_ASSERT(null->getKind() == NULL_EXPR);
 
-    TS_ASSERT(i1->getKind() == CONST_INTEGER);
-    TS_ASSERT(i2->getKind() == CONST_INTEGER);
+    TS_ASSERT(i1->getKind() == CONST_RATIONAL);
+    TS_ASSERT(i2->getKind() == CONST_RATIONAL);
     TS_ASSERT(r1->getKind() == CONST_RATIONAL);
     TS_ASSERT(r2->getKind() == CONST_RATIONAL);
   }
@@ -292,8 +292,8 @@ public:
     TS_ASSERT(d_apply_fun_bool->toString() == "(APPLY_UF f a)");
     TS_ASSERT(null->toString() == "null");
 
-    TS_ASSERT(i1->toString() == "(CONST_INTEGER 0)");
-    TS_ASSERT(i2->toString() == "(CONST_INTEGER 23)");
+    TS_ASSERT(i1->toString() == "(CONST_RATIONAL 0)");
+    TS_ASSERT(i2->toString() == "(CONST_RATIONAL 23)");
     TS_ASSERT(r1->toString() == "(CONST_RATIONAL 1/5)");
     TS_ASSERT(r2->toString() == "(CONST_RATIONAL 0)");
   }
@@ -324,8 +324,8 @@ public:
     TS_ASSERT(sd.str() == "(APPLY_UF f a)");
     TS_ASSERT(snull.str() == "null");
 
-    TS_ASSERT(si1.str() == "(CONST_INTEGER 0)");
-    TS_ASSERT(si2.str() == "(CONST_INTEGER 23)");
+    TS_ASSERT(si1.str() == "(CONST_RATIONAL 0)");
+    TS_ASSERT(si2.str() == "(CONST_RATIONAL 23)");
     TS_ASSERT(sr1.str() == "(CONST_RATIONAL 1/5)");
     TS_ASSERT(sr2.str() == "(CONST_RATIONAL 0)");
   }
@@ -362,14 +362,14 @@ public:
     TS_ASSERT_THROWS(b_bool->getConst<Kind>(), IllegalArgumentException);
     TS_ASSERT_THROWS(c_bool_and->getConst<Kind>(), IllegalArgumentException);
     TS_ASSERT(and_op->getConst<Kind>() == AND);
-    TS_ASSERT_THROWS(and_op->getConst<Integer>(), IllegalArgumentException);
+    TS_ASSERT_THROWS(and_op->getConst<Rational>(), IllegalArgumentException);
     TS_ASSERT(plus_op->getConst<Kind>() == PLUS);
     TS_ASSERT_THROWS(plus_op->getConst<Rational>(), IllegalArgumentException);
     TS_ASSERT_THROWS(d_apply_fun_bool->getConst<Kind>(), IllegalArgumentException);
     TS_ASSERT_THROWS(null->getConst<Kind>(), IllegalArgumentException);
 
-    TS_ASSERT(i1->getConst<Integer>() == 0);
-    TS_ASSERT(i2->getConst<Integer>() == 23);
+    TS_ASSERT(i1->getConst<Rational>() == 0);
+    TS_ASSERT(i2->getConst<Rational>() == 23);
     TS_ASSERT(r1->getConst<Rational>() == Rational(1, 5));
     TS_ASSERT(r2->getConst<Rational>() == Rational("0"));
 
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index c30e4badb..cca2ff4fc 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -168,13 +168,6 @@ public:
     TS_ASSERT_EQUALS(ff.getConst<bool>(),false);
   }
 
-
-  void testMkConstInt() {
-    Integer i("3");
-    Node n = d_nodeManager->mkConst(i);
-    TS_ASSERT_EQUALS(n.getConst<Integer>(),i);
-  }
-
   void testMkConstRat() {
     Rational r("3/2");
     Node n = d_nodeManager->mkConst(r);
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index 735fe2ac8..15a178b5c 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -50,8 +50,8 @@ public:
     delete d_ctxt;
   }
 
-  void testMkConstInt() {
-    Integer i("3");
+  void testMkConstRational() {
+    Rational i("3");
     Node n = d_nm->mkConst(i);
     Node m = d_nm->mkConst(i);
     TS_ASSERT_EQUALS(n.getId(), m.getId());
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index ce67004c6..a042b1752 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -73,7 +73,7 @@ public:
     Node x = d_nm->mkVar("x", d_nm->integerType());
     Node y = d_nm->mkVar("y", d_nm->integerType());
     Node x_plus_y = d_nm->mkNode(PLUS, x, y);
-    Node two = d_nm->mkConst(Integer(2));
+    Node two = d_nm->mkConst(Rational(2));
     Node x_times_2 = d_nm->mkNode(MULT, x, two);
 
     Node n = d_nm->mkNode(PLUS, x_times_2, x_plus_y, y);