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.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/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 70 |
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. * |