diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-01 14:48:04 +0000 |
commit | 45a138c326da72890bf889a3670aad503ef4aa1e (patch) | |
tree | fa0c9a8497d0b33f78a9f19212152a61392825cc /src/expr/expr_manager_template.h | |
parent | 8c0b2d6db32103268f84d89c0d0545c7eb504069 (diff) |
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!
Diffstat (limited to 'src/expr/expr_manager_template.h')
-rw-r--r-- | src/expr/expr_manager_template.h | 33 |
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} |