Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

1 files changed, 20 insertions, 1 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 283cdd725..04690f500 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -94,7 +94,11 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     case kind::CONST_RATIONAL: {
       const Rational& rat = n.getConst<Rational>();
-      out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
+      if(rat.getDenominator() == 1) {
+        out << rat.getNumerator();
+      } else {
+        out << '(' << rat.getNumerator() << '/' << rat.getDenominator() << ')';
+      }
       break;
     }
     case kind::CONST_INTEGER: {
@@ -107,6 +111,12 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << num;
       break;
     }
+    case kind::SUBRANGE_TYPE:
+      out << '[' << n.getConst<SubrangeBounds>() << ']';
+      break;
+    case kind::SUBTYPE_TYPE:
+      out << "SUBTYPE(" << n.getConst<Predicate>() << ")";
+      break;
     case kind::TYPE_CONSTANT:
       switch(TypeConstant tc = n.getConst<TypeConstant>()) {
       case REAL_TYPE:
@@ -129,6 +139,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
         break;
       }
       break;
+
     default:
       Warning() << "Constant printing not implemented for the case of " << n.getKind() << endl;
       out << n.getKind();
@@ -340,6 +351,14 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << '/';
       opType = INFIX;
       break;
+    case kind::INTS_DIVISION:
+      op << "DIV";
+      opType = INFIX;
+      break;
+    case kind::INTS_MODULUS:
+      op << "MOD";
+      opType = INFIX;
+      break;
     case kind::LT:
       op << '<';
       opType = INFIX;