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, 30 insertions, 3 deletions

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 2abd05821..bf9bfbb38 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -26,6 +26,7 @@
 #include "expr/kind.h"
 #include "expr/type.h"
 #include "expr/expr.h"
+#include "util/subrange_bound.h"
 
 ${includes}
 
@@ -33,7 +34,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 37 "${template}"
+#line 38 "${template}"
 
 namespace CVC4 {
 
@@ -119,7 +120,7 @@ public:
    * any expression references that used to be managed by this expression
    * manager and are left-over are bad.
    */
-  ~ExprManager();
+  ~ExprManager() throw();
 
   /** Get this node manager's options */
   const Options* getOptions() const;
@@ -403,9 +404,34 @@ public:
   SortConstructorType mkSortConstructor(const std::string& name,
                                         size_t arity) const;
 
+  /**
+   * Make a predicate subtype type defined by the given LAMBDA
+   * expression.  A TypeCheckingException can be thrown if lambda is
+   * not a LAMBDA, or is ill-typed, or if CVC4 fails at proving that
+   * the resulting predicate subtype is inhabited.
+   */
+  Type mkPredicateSubtype(Expr lambda)
+    throw(TypeCheckingException);
+
+  /**
+   * Make a predicate subtype type defined by the given LAMBDA
+   * expression and whose non-emptiness is witnessed by the given
+   * witness.  A TypeCheckingException can be thrown if lambda is not
+   * a LAMBDA, or is ill-typed, or if the witness is not a witness or
+   * ill-typed.
+   */
+  Type mkPredicateSubtype(Expr lambda, Expr witness)
+    throw(TypeCheckingException);
+
+  /**
+   * Make an integer subrange type as defined by the argument.
+   */
+  Type mkSubrangeType(const SubrangeBounds& bounds)
+    throw(TypeCheckingException);
+
   /** Get the type of an expression */
   Type getType(Expr e, bool check = false)
-    throw (TypeCheckingException);
+    throw(TypeCheckingException);
 
   // variables are special, because duplicates are permitted
   Expr mkVar(const std::string& name, Type type);
@@ -421,6 +447,7 @@ public:
 
   /** Returns the maximum arity of the given kind. */
   static unsigned maxArity(Kind kind);
+
 };/* class ExprManager */
 
 ${mkConst_instantiations}