diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/Makefile.am | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 68 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 4 | ||||
-rw-r--r-- | src/smt/smt_engine_scope.cpp | 10 | ||||
-rw-r--r-- | src/smt/smt_engine_scope.h | 40 |
5 files changed, 89 insertions, 35 deletions
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index 3e777ec89..5cc0cedd1 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -8,6 +8,8 @@ noinst_LTLIBRARIES = libsmt.la libsmt_la_SOURCES = \ smt_engine.cpp \ smt_engine.h \ + smt_engine_scope.cpp \ + smt_engine_scope.h \ modal_exception.h \ bad_option_exception.h \ no_such_function_exception.h diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4cccb8d10..01ce73be1 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -38,6 +38,7 @@ #include "smt/modal_exception.h" #include "smt/no_such_function_exception.h" #include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "theory/theory_engine.h" #include "proof/proof_manager.h" #include "util/proof.h" @@ -48,16 +49,9 @@ #include "util/output.h" #include "util/hash.h" #include "theory/substitutions.h" -#include "theory/builtin/theory_builtin.h" -#include "theory/booleans/theory_bool.h" -#include "theory/booleans/circuit_propagator.h" -#include "theory/uf/theory_uf.h" -#include "theory/arith/theory_arith.h" -#include "theory/arrays/theory_arrays.h" -#include "theory/bv/theory_bv.h" -#include "theory/datatypes/theory_datatypes.h" #include "theory/theory_traits.h" #include "theory/logic_info.h" +#include "theory/booleans/circuit_propagator.h" #include "util/ite_removal.h" #include "theory/model.h" @@ -265,6 +259,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_cumulativeResourceUsed(0), d_status(), d_private(new smt::SmtEnginePrivate(*this)), + d_statisticsRegistry(new StatisticsRegistry()), d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"), d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"), d_numConstantProps("smt::SmtEngine::numConstantProps", 0), @@ -277,7 +272,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0) { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); StatisticsRegistry::registerStat(&d_definitionExpansionTime); StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime); @@ -382,7 +377,7 @@ void SmtEngine::shutdown() { } SmtEngine::~SmtEngine() throw() { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); try { while(Options::current()->incrementalSolving && d_userContext->getLevel() > 1) { @@ -424,6 +419,9 @@ SmtEngine::~SmtEngine() throw() { delete d_theoryEngine; delete d_propEngine; //delete d_decisionEngine; + + delete d_statisticsRegistry; + } catch(Exception& e) { Warning() << "CVC4 threw an exception during cleanup." << endl << e << endl; @@ -431,7 +429,7 @@ SmtEngine::~SmtEngine() throw() { } void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); if(Dump.isOn("benchmark")) { Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString()); @@ -442,7 +440,7 @@ void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { } void SmtEngine::setLogic(const std::string& s) throw(ModalException) { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); setLogic(LogicInfo(s)); } @@ -605,7 +603,7 @@ void SmtEngine::setLogicInternal() throw(AssertionException) { void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOptionException, ModalException) { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; if(Dump.isOn("benchmark")) { @@ -629,7 +627,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value) if(! value.isAtom()) { throw BadOptionException("argument to (set-info :cvc4-logic ..) must be a string"); } - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); d_logic = value.getValue(); setLogicInternal(); return; @@ -664,7 +662,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value) SExpr SmtEngine::getInfo(const std::string& key) const throw(BadOptionException) { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); Trace("smt") << "SMT getInfo(" << key << ")" << endl; if(key == ":all-statistics") { @@ -705,7 +703,7 @@ SExpr SmtEngine::getInfo(const std::string& key) const void SmtEngine::setOption(const std::string& key, const SExpr& value) throw(BadOptionException, ModalException) { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; if(Dump.isOn("benchmark")) { @@ -757,7 +755,7 @@ void SmtEngine::setOption(const std::string& key, const SExpr& value) SExpr SmtEngine::getOption(const std::string& key) const throw(BadOptionException) { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); Trace("smt") << "SMT getOption(" << key << ")" << endl; if(Dump.isOn("benchmark")) { @@ -804,7 +802,7 @@ void SmtEngine::defineFunction(Expr func, << func; Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula); } - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); // type check body Type formulaType = formula.getType(Options::current()->typeChecking); @@ -1606,7 +1604,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) { Assert(e.isNull() || e.getExprManager() == d_exprManager); - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); finalOptionsAreSet(); @@ -1669,7 +1667,7 @@ Result SmtEngine::query(const BoolExpr& e) { Assert(!e.isNull()); Assert(e.getExprManager() == d_exprManager); - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); finalOptionsAreSet(); @@ -1725,7 +1723,7 @@ Result SmtEngine::query(const BoolExpr& e) { Result SmtEngine::assertFormula(const BoolExpr& e) { Assert(e.getExprManager() == d_exprManager); - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); finalOptionsAreSet(); Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl; ensureBoolean(e); @@ -1738,7 +1736,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) { Expr SmtEngine::simplify(const Expr& e) { Assert(e.getExprManager() == d_exprManager); - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); finalOptionsAreSet(); if( Options::current()->typeChecking ) { e.getType(true);// ensure expr is type-checked at this point @@ -1753,7 +1751,7 @@ Expr SmtEngine::simplify(const Expr& e) { Expr SmtEngine::getValue(const Expr& e) throw(ModalException, AssertionException) { Assert(e.getExprManager() == d_exprManager); - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); // ensure expr is type-checked at this point Type type = e.getType(Options::current()->typeChecking); @@ -1799,7 +1797,7 @@ Expr SmtEngine::getValue(const Expr& e) } bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); finalOptionsAreSet(); Type type = e.getType(Options::current()->typeChecking); // must be Boolean @@ -1828,7 +1826,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) { SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { Trace("smt") << "SMT getAssignment()" << endl; - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); finalOptionsAreSet(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetAssignmentCommand(); @@ -1890,7 +1888,7 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) { void SmtEngine::addToModelType( Type& t ){ Trace("smt") << "SMT addToModelType(" << t << ")" << endl; - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); if( Options::current()->produceModels ) { d_theoryEngine->getModel()->addDefineType( TypeNode::fromType( t ) ); } @@ -1898,7 +1896,7 @@ void SmtEngine::addToModelType( Type& t ){ void SmtEngine::addToModelFunction( Expr& e ){ Trace("smt") << "SMT addToModelFunction(" << e << ")" << endl; - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); if( Options::current()->produceModels ) { d_theoryEngine->getModel()->addDefineFunction( e.getNode() ); } @@ -1907,7 +1905,7 @@ void SmtEngine::addToModelFunction( Expr& e ){ Model* SmtEngine::getModel() throw(ModalException, AssertionException){ Trace("smt") << "SMT getModel()" << endl; - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); if(!Options::current()->produceModels) { const char* msg = @@ -1928,7 +1926,7 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) { Trace("smt") << "SMT getProof()" << endl; - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); finalOptionsAreSet(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetProofCommand(); @@ -1958,7 +1956,7 @@ vector<Expr> SmtEngine::getAssertions() if(Dump.isOn("benchmark")) { Dump("benchmark") << GetAssertionsCommand(); } - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); Trace("smt") << "SMT getAssertions()" << endl; if(!Options::current()->interactive) { const char* msg = @@ -1970,13 +1968,13 @@ vector<Expr> SmtEngine::getAssertions() } size_t SmtEngine::getStackLevel() const { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); Trace("smt") << "SMT getStackLevel()" << endl; return d_context->getLevel(); } void SmtEngine::push() { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); finalOptionsAreSet(); Trace("smt") << "SMT push()" << endl; d_private->processAssertions(); @@ -2000,7 +1998,7 @@ void SmtEngine::push() { } void SmtEngine::pop() { - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); finalOptionsAreSet(); Trace("smt") << "SMT pop()" << endl; if(Dump.isOn("benchmark")) { @@ -2108,11 +2106,11 @@ unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) { } StatisticsRegistry* SmtEngine::getStatisticsRegistry() const { - return d_exprManager->d_nodeManager->getStatisticsRegistry(); + return d_statisticsRegistry; } void SmtEngine::printModel( std::ostream& out, Model* m ){ - NodeManagerScope nms(d_nodeManager); + SmtScope smts(this); m->toStream(out); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index aef98d75b..4df9054a7 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -76,6 +76,7 @@ namespace smt { class DefinedFunction; class SmtEnginePrivate; + class SmtScope; }/* CVC4::smt namespace */ // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the @@ -248,6 +249,9 @@ class CVC4_PUBLIC SmtEngine { void setLogicInternal() throw(AssertionException); friend class ::CVC4::smt::SmtEnginePrivate; + friend class ::CVC4::smt::SmtScope; + + StatisticsRegistry* d_statisticsRegistry; // === STATISTICS === /** time spent in definition-expansion */ diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp new file mode 100644 index 000000000..03298e99a --- /dev/null +++ b/src/smt/smt_engine_scope.cpp @@ -0,0 +1,10 @@ +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" + +namespace CVC4 { +namespace smt { + +CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current = NULL; + +} +} diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h new file mode 100644 index 000000000..bcdaefd9f --- /dev/null +++ b/src/smt/smt_engine_scope.h @@ -0,0 +1,40 @@ +#include "smt/smt_engine.h" +#include "util/tls.h" +#include "util/Assert.h" +#include "expr/node_manager.h" +#include "util/output.h" + +#pragma once + +namespace CVC4 { +namespace smt { + +extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current; + +inline SmtEngine* currentSmtEngine() { + Assert(s_smtEngine_current != NULL); + return s_smtEngine_current; +} + +class SmtScope : public NodeManagerScope { + /** The old NodeManager, to be restored on destruction. */ + SmtEngine* d_oldSmtEngine; + +public: + + SmtScope(const SmtEngine* smt) : + NodeManagerScope(smt->d_nodeManager), + d_oldSmtEngine(s_smtEngine_current) { + Assert(smt != NULL); + s_smtEngine_current = const_cast<SmtEngine*>(smt); + Debug("current") << "smt scope: " << s_smtEngine_current << std::endl; + } + + ~SmtScope() { + s_smtEngine_current = d_oldSmtEngine; + Debug("current") << "smt scope: returning to " << s_smtEngine_current << std::endl; + } +};/* class SmtScope */ + +} +} |