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.cpp | |
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.cpp')
-rw-r--r-- | src/expr/node_manager.cpp | 65 |
1 files changed, 57 insertions, 8 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index c647e128c..a2fddadfc 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -29,6 +29,7 @@ #include <algorithm> #include <stack> +#include <utility> #include <ext/hash_set> using namespace std; @@ -235,14 +236,15 @@ void NodeManager::reclaimZombies() { }/* NodeManager::reclaimZombies() */ TypeNode NodeManager::getType(TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - // Many theories' type checkers call Node::getType() directly. - // This is incorrect, since "this" might not be the caller's - // curent node manager. Rather than force the individual typecheckers - // not to do this (by policy, which would be imperfect and lead - // to hard-to-find bugs, which it has in the past), we just - // set this node manager to be current for the duration of this - // check. + throw(TypeCheckingExceptionPrivate, AssertionException) { + + // Many theories' type checkers call Node::getType() directly. This + // is incorrect, since "this" might not be the caller's curent node + // manager. Rather than force the individual typecheckers not to do + // this (by policy, which would be imperfect and lead to + // hard-to-find bugs, which it has in the past), we just set this + // node manager to be current for the duration of this check. + // NodeManagerScope nms(this); TypeNode typeNode; @@ -321,4 +323,51 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor, return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); } +TypeNode NodeManager::mkPredicateSubtype(Expr lambda) + throw(TypeCheckingExceptionPrivate) { + + Node lambdan = Node::fromExpr(lambda); + + if(lambda.isNull()) { + throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression"); + } + + TypeNode tn = lambdan.getType(); + if(! tn.isPredicateLike() || + tn.getArgTypes().size() != 1) { + std::stringstream ss; + ss << Expr::setlanguage(Options::current()->outputLanguage) + << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; + throw TypeCheckingExceptionPrivate(lambdan, ss.str()); + } + + return TypeNode(mkTypeConst(Predicate(lambda))); +} + +TypeNode NodeManager::mkPredicateSubtype(Expr lambda, Expr witness) + throw(TypeCheckingExceptionPrivate) { + + Node lambdan = Node::fromExpr(lambda); + + if(lambda.isNull()) { + throw TypeCheckingExceptionPrivate(lambdan, "cannot make a predicate subtype based on null expression"); + } + + TypeNode tn = lambdan.getType(); + if(! tn.isPredicateLike() || + tn.getArgTypes().size() != 1) { + std::stringstream ss; + ss << Expr::setlanguage(Options::current()->outputLanguage) + << "expected a predicate of one argument to define predicate subtype, but got type `" << tn << "'"; + throw TypeCheckingExceptionPrivate(lambdan, ss.str()); + } + + return TypeNode(mkTypeConst(Predicate(lambda, witness))); +} + +TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) + throw(TypeCheckingExceptionPrivate) { + return TypeNode(mkTypeConst(bounds)); +} + }/* CVC4 namespace */ |