diff options
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. * |