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/node_manager.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/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 37 |
1 files changed, 34 insertions, 3 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 704e930b5..da999cc82 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -38,6 +38,7 @@ #include "expr/metakind.h" #include "expr/node_value.h" #include "context/context.h" +#include "util/subrange_bound.h" #include "util/configuration_private.h" #include "util/tls.h" #include "util/options.h" @@ -662,6 +663,31 @@ public: inline TypeNode mkSortConstructor(const std::string& name, size_t arity); /** + * Make a predicate subtype type defined by the given LAMBDA + * expression. A TypeCheckingExceptionPrivate 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. + */ + TypeNode mkPredicateSubtype(Expr lambda) + throw(TypeCheckingExceptionPrivate); + + /** + * Make a predicate subtype type defined by the given LAMBDA + * expression and whose non-emptiness is witnessed by the given + * witness. A TypeCheckingExceptionPrivate can be thrown if lambda + * is not a LAMBDA, or is ill-typed, or if the witness is not a + * witness or ill-typed. + */ + TypeNode mkPredicateSubtype(Expr lambda, Expr witness) + throw(TypeCheckingExceptionPrivate); + + /** + * Make an integer subrange type as defined by the argument. + */ + TypeNode mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingExceptionPrivate); + + /** * Get the type for the given node and optionally do type checking. * * Initial type computation will be near-constant time if @@ -687,7 +713,7 @@ public: * (default: false) */ TypeNode getType(TNode n, bool check = false) - throw (TypeCheckingExceptionPrivate, AssertionException); + throw(TypeCheckingExceptionPrivate, AssertionException); /** * Convert a node to an expression. Uses the ExprManager @@ -944,10 +970,15 @@ inline TypeNode NodeManager::mkBitVectorType(unsigned size) { inline TypeNode NodeManager::mkArrayType(TypeNode indexType, TypeNode constituentType) { - CheckArgument(!indexType.isFunctionLike(), domain, + CheckArgument(!indexType.isNull(), indexType, + "unexpected NULL index type"); + CheckArgument(!constituentType.isNull(), constituentType, + "unexpected NULL constituent type"); + CheckArgument(!indexType.isFunctionLike(), indexType, "cannot index arrays by a function-like type"); - CheckArgument(!constituentType.isFunctionLike(), domain, + CheckArgument(!constituentType.isFunctionLike(), constituentType, "cannot store function-like types in arrays"); +Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl; return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType); } |