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

2 files changed, 3 insertions, 17 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 857513fa3..1f147479d 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -94,18 +94,13 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     case kind::CONST_RATIONAL: {
       const Rational& rat = n.getConst<Rational>();
-      if(rat.getDenominator() == 1) {
+      if(rat.isIntegral()) {
         out << rat.getNumerator();
       } else {
         out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
       }
       break;
     }
-    case kind::CONST_INTEGER: {
-      const Integer& num = n.getConst<Integer>();
-      out << num;
-      break;
-    }
     case kind::CONST_PSEUDOBOOLEAN: {
       const Pseudoboolean& num = n.getConst<Pseudoboolean>();
       out << num;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 03422c162..2b686441a 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -100,25 +100,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     case kind::BUILTIN:
       out << smtKindString(n.getConst<Kind>());
       break;
-    case kind::CONST_INTEGER: {
-      Integer i = n.getConst<Integer>();
-      if(i < 0) {
-        out << "(- " << -i << ')';
-      } else {
-        out << i;
-      }
-      break;
-    }
     case kind::CONST_RATIONAL: {
       Rational r = n.getConst<Rational>();
       if(r < 0) {
-        if(r.getDenominator() == 1) {
+        if(r.isIntegral()) {
           out << "(- " << -r << ')';
         } else {
           out << "(- (/ " << (-r).getNumerator() << ' ' << (-r).getDenominator() << "))";
         }
       } else {
-        if(r.getDenominator() == 1) {
+        if(r.isIntegral()) {
           out << r;
         } else {
           out << "(/ " << r.getNumerator() << ' ' << r.getDenominator() << ')';