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, 13 insertions, 0 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 393ad664b..691e96ed7 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -127,6 +127,19 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       break;
     }
 
+    case kind::SUBRANGE_TYPE: {
+      const SubrangeBounds& bounds = n.getConst<SubrangeBounds>();
+      // No way to represent subranges in SMT-LIBv2; this is inspired
+      // by yices format (but isn't identical to it).
+      out << "(subrange " << bounds.lower << ' ' << bounds.upper << ')';
+      break;
+    }
+    case kind::SUBTYPE_TYPE:
+      // No way to represent predicate subtypes in SMT-LIBv2; this is
+      // inspired by yices format (but isn't identical to it).
+      out << "(subtype " << n.getConst<Predicate>() << ')';
+      break;
+
     default:
       // fall back on whatever operator<< does on underlying type; we
       // might luck out and be SMT-LIB v2 compliant