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, 56 insertions, 14 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 46a7bb82c..533a4dd7f 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -97,24 +97,33 @@ ExprManager::ExprManager(const Options& options) :
 #endif
 }
 
-ExprManager::~ExprManager() {
-#ifdef CVC4_STATISTICS_ON
+ExprManager::~ExprManager() throw() {
   NodeManagerScope nms(d_nodeManager);
-  for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
-    if (d_exprStatistics[i] != NULL) {
-      StatisticsRegistry::unregisterStat(d_exprStatistics[i]);
-      delete d_exprStatistics[i];
+
+  try {
+
+#ifdef CVC4_STATISTICS_ON
+    for (unsigned i = 0; i < kind::LAST_KIND; ++ i) {
+      if (d_exprStatistics[i] != NULL) {
+        StatisticsRegistry::unregisterStat(d_exprStatistics[i]);
+        delete d_exprStatistics[i];
+      }
     }
-  }
-  for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
-    if (d_exprStatisticsVars[i] != NULL) {
-      StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]);
-      delete d_exprStatisticsVars[i];
+    for (unsigned i = 0; i <= LAST_TYPE; ++ i) {
+      if (d_exprStatisticsVars[i] != NULL) {
+        StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]);
+        delete d_exprStatisticsVars[i];
+      }
     }
-  }
 #endif
-  delete d_nodeManager;
-  delete d_ctxt;
+
+    delete d_nodeManager;
+    delete d_ctxt;
+
+  } catch(Exception& e) {
+    Warning() << "CVC4 threw an exception during cleanup." << std::endl
+              << e << std::endl;
+  }
 }
 
 const Options* ExprManager::getOptions() const {
@@ -697,6 +706,39 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name,
               new TypeNode(d_nodeManager->mkSortConstructor(name, arity))));
 }
 
+Type ExprManager::mkPredicateSubtype(Expr lambda)
+  throw(TypeCheckingException) {
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    return PredicateSubtype(Type(d_nodeManager,
+                new TypeNode(d_nodeManager->mkPredicateSubtype(lambda))));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Type ExprManager::mkPredicateSubtype(Expr lambda, Expr witness)
+  throw(TypeCheckingException) {
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    return PredicateSubtype(Type(d_nodeManager,
+                new TypeNode(d_nodeManager->mkPredicateSubtype(lambda, witness))));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
+Type ExprManager::mkSubrangeType(const SubrangeBounds& bounds)
+  throw(TypeCheckingException) {
+  NodeManagerScope nms(d_nodeManager);
+  try {
+    return SubrangeType(Type(d_nodeManager,
+                new TypeNode(d_nodeManager->mkSubrangeType(bounds))));
+  } catch (const TypeCheckingExceptionPrivate& e) {
+    throw TypeCheckingException(this, &e);
+  }
+}
+
 /**
  * Get the type for the given Expr and optionally do type checking.
  *