diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-16 15:53:22 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-16 15:53:22 +0000 |
commit | 36615c5e7332e26645b33ce9b6bab25439a5108e (patch) | |
tree | 166efefced107009f4a68ff3d0c6623540dfa435 | |
parent | 25396f93b7df85c80a39ed207483e28a8c86ff26 (diff) |
Support for having two SmtEngines with the same ExprManager.
Basically, this involves creating a separate StatisticsRegistry for the
ExprManager and for the SmtEngine. Otherwise, theories register the
same statistic twice. This is a larger problem, though, for creating
multiple instances of theories, and that is unaddressed. Still,
separating out the expr statistics into a separate registry is probably
a good idea, since the expr package is somewhat separate anyway (and in
the short term it allows two SmtEngines to co-exist).
-rw-r--r-- | src/expr/expr_manager_template.cpp | 18 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 8 | ||||
-rw-r--r-- | src/expr/node_manager.h | 4 | ||||
-rw-r--r-- | src/main/driver.cpp | 1 | ||||
-rw-r--r-- | src/main/driver_portfolio.cpp | 7 | ||||
-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 | ||||
-rw-r--r-- | src/util/stats.cpp | 24 | ||||
-rw-r--r-- | src/util/stats.h | 3 | ||||
-rw-r--r-- | test/system/Makefile.am | 3 | ||||
-rw-r--r-- | test/system/boilerplate.cpp | 1 | ||||
-rw-r--r-- | test/system/two_smt_engines.cpp | 37 | ||||
-rw-r--r-- | test/unit/Makefile.am | 4 | ||||
-rw-r--r-- | test/unit/prop/cnf_stream_white.h (renamed from test/unit/prop/cnf_stream_black.h) | 52 | ||||
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 35 | ||||
-rw-r--r-- | test/unit/theory/theory_engine_white.h | 41 | ||||
-rw-r--r-- | test/unit/theory/theory_white.h (renamed from test/unit/theory/theory_black.h) | 30 |
20 files changed, 264 insertions, 128 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 1db534dc4..25578399f 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -40,7 +40,7 @@ ${includes} stringstream statName; \ statName << "expr::ExprManager::" << kind; \ d_exprStatistics[kind] = new IntStat(statName.str(), 0); \ - StatisticsRegistry::registerStat(d_exprStatistics[kind]); \ + d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatistics[kind]); \ } \ ++ *(d_exprStatistics[kind]); \ } @@ -56,7 +56,7 @@ ${includes} statName << "expr::ExprManager::VARIABLE:" << type; \ } \ d_exprStatisticsVars[type] = new IntStat(statName.str(), 0); \ - StatisticsRegistry::registerStat(d_exprStatisticsVars[type]); \ + d_nodeManager->getStatisticsRegistry()->registerStat_(d_exprStatisticsVars[type]); \ } \ ++ *(d_exprStatisticsVars[type]); \ } @@ -78,7 +78,7 @@ ExprManager::ExprManager() : for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { d_exprStatistics[i] = NULL; } - for (unsigned i = 0; i <= LAST_TYPE; ++ i) { + for (unsigned i = 0; i < LAST_TYPE; ++ i) { d_exprStatisticsVars[i] = NULL; } #endif @@ -88,7 +88,7 @@ ExprManager::ExprManager(const Options& options) : d_ctxt(new Context()), d_nodeManager(new NodeManager(d_ctxt, this, options)) { #ifdef CVC4_STATISTICS_ON - for (unsigned i = 0; i <= LAST_TYPE; ++ i) { + for (unsigned i = 0; i < LAST_TYPE; ++ i) { d_exprStatisticsVars[i] = NULL; } for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { @@ -105,13 +105,13 @@ ExprManager::~ExprManager() throw() { #ifdef CVC4_STATISTICS_ON for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { if (d_exprStatistics[i] != NULL) { - StatisticsRegistry::unregisterStat(d_exprStatistics[i]); + d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatistics[i]); delete d_exprStatistics[i]; } } - for (unsigned i = 0; i <= LAST_TYPE; ++ i) { + for (unsigned i = 0; i < LAST_TYPE; ++ i) { if (d_exprStatisticsVars[i] != NULL) { - StatisticsRegistry::unregisterStat(d_exprStatisticsVars[i]); + d_nodeManager->getStatisticsRegistry()->unregisterStat_(d_exprStatisticsVars[i]); delete d_exprStatisticsVars[i]; } } @@ -886,6 +886,10 @@ Context* ExprManager::getContext() const { return d_ctxt; } +StatisticsRegistry* ExprManager::getStatisticsRegistry() const throw() { + return d_nodeManager->getStatisticsRegistry(); +} + namespace expr { Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 9d0b8d34a..fdc1e1159 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -27,6 +27,7 @@ #include "expr/type.h" #include "expr/expr.h" #include "util/subrange_bound.h" +#include "util/stats.h" ${includes} @@ -34,7 +35,7 @@ ${includes} // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 38 "${template}" +#line 39 "${template}" namespace CVC4 { @@ -64,7 +65,7 @@ private: NodeManager* d_nodeManager; /** Counts of expressions and variables created of a given kind */ - IntStat* d_exprStatisticsVars[LAST_TYPE + 1]; + IntStat* d_exprStatisticsVars[LAST_TYPE]; IntStat* d_exprStatistics[kind::LAST_KIND]; /** @@ -450,6 +451,9 @@ public: Expr mkVar(const std::string& name, Type type); Expr mkVar(Type type); + /** Get a reference to the statistics registry for this ExprManager */ + StatisticsRegistry* getStatisticsRegistry() const throw(); + /** Export an expr to a different ExprManager */ //static Expr exportExpr(const Expr& e, ExprManager* em); /** Export a type to a different ExprManager */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 6ce96e70a..6c34eb4a3 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -277,7 +277,7 @@ public: } /** Get this node manager's statistics registry */ - StatisticsRegistry* getStatisticsRegistry() const { + StatisticsRegistry* getStatisticsRegistry() const throw() { return d_statisticsRegistry; } @@ -802,7 +802,7 @@ public: Debug("current") << "node manager scope: " << "returning to " << NodeManager::s_current << "\n"; } -}; +};/* class NodeManagerScope */ template <class AttrKind> diff --git a/src/main/driver.cpp b/src/main/driver.cpp index eda5df2ca..f24526e6c 100644 --- a/src/main/driver.cpp +++ b/src/main/driver.cpp @@ -240,6 +240,7 @@ int runCvc4(int argc, char* argv[], Options& options) { // signal handlers need access pStatistics = smt.getStatisticsRegistry(); + pStatistics->registerStat_(exprMgr.getStatisticsRegistry()); // Timer statistic RegisterStatistic statTotalTime(exprMgr, &s_totalTime); diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp index 0698d5157..d93e9f872 100644 --- a/src/main/driver_portfolio.cpp +++ b/src/main/driver_portfolio.cpp @@ -409,7 +409,7 @@ int runCvc4(int argc, char *argv[], Options& options) { theStatisticsRegistry.registerStat_((&driverStatisticsRegistry)); // Timer statistic - RegisterStatistic* statTotatTime = + RegisterStatistic* statTotalTime = new RegisterStatistic(&driverStatisticsRegistry, &s_totalTime); RegisterStatistic* statBeforePortfolioTime = new RegisterStatistic(&driverStatisticsRegistry, &s_beforePortfolioTime); @@ -521,7 +521,8 @@ int runCvc4(int argc, char *argv[], Options& options) { // Register the statistics registry of the thread string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id); smts[i]->getStatisticsRegistry()->setName(tag); - theStatisticsRegistry.registerStat_( (Stat*)smts[i]->getStatisticsRegistry() ); + theStatisticsRegistry.registerStat_( smts[i]->getStatisticsRegistry() ); + theStatisticsRegistry.registerStat_( exprMgrs[i]->getStatisticsRegistry() ); } /************************* Lemma sharing init ************************/ @@ -635,7 +636,7 @@ int runCvc4(int argc, char *argv[], Options& options) { //delete vmaps; - delete statTotatTime; + delete statTotalTime; delete statBeforePortfolioTime; delete statFilenameReg; 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 */ + +} +} diff --git a/src/util/stats.cpp b/src/util/stats.cpp index b030495c5..96e300197 100644 --- a/src/util/stats.cpp +++ b/src/util/stats.cpp @@ -20,7 +20,10 @@ #include "util/stats.h" #include "expr/node_manager.h" #include "expr/expr_manager_scope.h" +#include "expr/expr_manager.h" #include "lib/clock_gettime.h" +#include "smt/smt_engine_scope.h" +#include "smt/smt_engine.h" #ifdef CVC4_STATISTICS_ON # define __CVC4_USE_STATISTICS true @@ -34,12 +37,12 @@ std::string Stat::s_delim(","); std::string StatisticsRegistry::s_regDelim("::"); StatisticsRegistry* StatisticsRegistry::current() { - return NodeManager::currentNM()->getStatisticsRegistry(); + return smt::currentSmtEngine()->getStatisticsRegistry(); } void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; + StatSet& registeredStats = current()->d_registeredStats; AlwaysAssert(registeredStats.find(s) == registeredStats.end(), "Statistic `%s' was already registered with this registry.", s->getName().c_str()); registeredStats.insert(s); @@ -55,7 +58,7 @@ void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) { void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { #ifdef CVC4_STATISTICS_ON - StatSet& registeredStats = NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats; + StatSet& registeredStats = current()->d_registeredStats; AlwaysAssert(registeredStats.find(s) != registeredStats.end(), "Statistic `%s' was not registered with this registry.", s->getName().c_str()); registeredStats.erase(s); @@ -91,11 +94,11 @@ void StatisticsRegistry::flushStat(std::ostream &out) const {; } StatisticsRegistry::const_iterator StatisticsRegistry::begin() { - return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.begin(); + return current()->d_registeredStats.begin(); }/* StatisticsRegistry::begin() */ StatisticsRegistry::const_iterator StatisticsRegistry::end() { - return NodeManager::currentNM()->getStatisticsRegistry()->d_registeredStats.end(); + return current()->d_registeredStats.end(); }/* StatisticsRegistry::end() */ void TimerStat::start() { @@ -117,9 +120,14 @@ void TimerStat::stop() { }/* TimerStat::stop() */ RegisterStatistic::RegisterStatistic(ExprManager& em, Stat* stat) : - d_reg(NULL), + d_reg(em.getStatisticsRegistry()), d_stat(stat) { - ExprManagerScope ems(em); - d_reg = StatisticsRegistry::current(); d_reg->registerStat_(d_stat); } + +RegisterStatistic::RegisterStatistic(SmtEngine& smt, Stat* stat) : + d_reg(smt.getStatisticsRegistry()), + d_stat(stat) { + d_reg->registerStat_(d_stat); +} + diff --git a/src/util/stats.h b/src/util/stats.h index 63e732305..aabf04dc0 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -43,6 +43,7 @@ namespace CVC4 { #endif class ExprManager; +class SmtEngine; class CVC4_PUBLIC Stat; @@ -803,6 +804,8 @@ public: RegisterStatistic(ExprManager& em, Stat* stat); + RegisterStatistic(SmtEngine& smt, Stat* stat); + ~RegisterStatistic() { d_reg->unregisterStat_(d_stat); } diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 7fa7b4a68..070f69639 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -2,7 +2,8 @@ TESTS_ENVIRONMENT = TEST_EXTENSIONS = .class CPLUSPLUS_TESTS = \ boilerplate \ - ouroborous + ouroborous \ + two_smt_engines # cvc3_main TESTS = $(CPLUSPLUS_TESTS) diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp index c64c1463e..18a560c0e 100644 --- a/test/system/boilerplate.cpp +++ b/test/system/boilerplate.cpp @@ -30,6 +30,7 @@ using namespace std; int main() { ExprManager em; Options opts; + cout << "foo: " << opts.threadArgv.size() << endl; SmtEngine smt(&em); Result r = smt.query(em.mkConst(true)); diff --git a/test/system/two_smt_engines.cpp b/test/system/two_smt_engines.cpp new file mode 100644 index 000000000..35d6c92cf --- /dev/null +++ b/test/system/two_smt_engines.cpp @@ -0,0 +1,37 @@ +/********************* */ +/*! \file two_smt_engines.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A simple test of multiple SmtEngines + ** + ** A simple test of multiple SmtEngines. + **/ + +#include <iostream> +#include <sstream> + +#include "expr/expr.h" +#include "smt/smt_engine.h" + +using namespace CVC4; +using namespace std; + +int main() { + ExprManager em; + Options opts; + SmtEngine smt(&em); + SmtEngine smt2(&em); + Result r = smt.query(em.mkConst(true)); + + return r == Result::VALID ? 0 : 1; +} + diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index bb8cdf7fe..dc53bff61 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -2,7 +2,7 @@ UNIT_TESTS = \ theory/logic_info_white \ theory/theory_engine_white \ - theory/theory_black \ + theory/theory_white \ theory/theory_arith_white \ theory/union_find_black \ theory/theory_bv_white \ @@ -24,7 +24,7 @@ UNIT_TESTS = \ expr/type_node_white \ parser/parser_black \ parser/parser_builder_black \ - prop/cnf_stream_black \ + prop/cnf_stream_white \ context/context_black \ context/context_white \ context/context_mm_black \ diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_white.h index 70c306a6d..cc7ea9bf6 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_white.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file cnf_stream_black.h +/*! \file cnf_stream_white.h ** \verbatim ** Original author: cconway ** Major contributors: mdeters @@ -22,7 +22,6 @@ #include "util/Assert.h" - #include "expr/expr_manager.h" #include "expr/node_manager.h" #include "context/context.h" @@ -30,6 +29,7 @@ #include "prop/prop_engine.h" #include "prop/theory_proxy.h" #include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "theory/theory.h" #include "theory/theory_engine.h" @@ -42,6 +42,8 @@ using namespace CVC4; using namespace CVC4::context; using namespace CVC4::prop; +using namespace CVC4::smt; +using namespace CVC4::theory; using namespace std; /* This fake class relies on the face that a MiniSat variable is just an int. */ @@ -118,19 +120,13 @@ public: };/* class FakeSatSolver */ -class CnfStreamBlack : public CxxTest::TestSuite { +class CnfStreamWhite : public CxxTest::TestSuite { /** The SAT solver proxy */ FakeSatSolver* d_satSolver; - /** The logic info */ - LogicInfo* d_logicInfo; - /** The theory engine */ TheoryEngine* d_theoryEngine; - /** The output channel */ - theory::OutputChannel* d_outputChannel; - /** The CNF converter in use */ CnfStream* d_cnfStream; @@ -143,31 +139,32 @@ class CnfStreamBlack : public CxxTest::TestSuite { /** The node manager */ NodeManager* d_nodeManager; + ExprManager* d_exprManager; + SmtScope* d_scope; + SmtEngine* d_smt; + void setUp() { - d_context = new Context(); - d_userContext = new UserContext(); - d_nodeManager = new NodeManager(d_context, NULL); - NodeManagerScope nms(d_nodeManager); + d_exprManager = new ExprManager(); + d_smt = new SmtEngine(d_exprManager); + d_smt->d_logic.lock(); + d_nodeManager = NodeManager::fromExprManager(d_exprManager); + d_scope = new SmtScope(d_smt); + + d_context = d_smt->d_context; + d_userContext = d_smt->d_userContext; + + d_theoryEngine = d_smt->d_theoryEngine; + d_satSolver = new FakeSatSolver(); - d_logicInfo = new LogicInfo(); - d_logicInfo->lock(); - d_theoryEngine = new TheoryEngine(d_context, d_userContext, *d_logicInfo); - d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN); - d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL); - d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH); d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine)); } void tearDown() { - NodeManagerScope nms(d_nodeManager); delete d_cnfStream; - d_theoryEngine->shutdown(); - delete d_theoryEngine; - delete d_logicInfo; delete d_satSolver; - delete d_nodeManager; - delete d_userContext; - delete d_context; + delete d_scope; + delete d_smt; + delete d_exprManager; } public: @@ -291,8 +288,7 @@ public: Node b = d_nodeManager->mkVar(d_nodeManager->booleanType()); Node a_and_b = d_nodeManager->mkNode(kind::AND, a, b); d_cnfStream->ensureLiteral(a_and_b); - // Clauses are necessary to "literal-ize" a_and_b; this perhaps - // doesn't belong in a black-box test though... + // Clauses are necessary to "literal-ize" a_and_b TS_ASSERT( d_satSolver->addClauseCalled() ); TS_ASSERT( d_cnfStream->hasLiteral(a_and_b) ); } diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 48b9b2d35..fe922a6e1 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -21,12 +21,15 @@ #include <cxxtest/TestSuite.h> #include "theory/theory.h" +#include "theory/theory_engine.h" #include "theory/arith/theory_arith.h" #include "theory/quantifiers_engine.h" #include "expr/node.h" #include "expr/node_manager.h" #include "context/context.h" #include "util/rational.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "theory/theory_test_utils.h" @@ -38,6 +41,7 @@ using namespace CVC4::theory::arith; using namespace CVC4::expr; using namespace CVC4::context; using namespace CVC4::kind; +using namespace CVC4::smt; using namespace std; @@ -45,14 +49,15 @@ class TheoryArithWhite : public CxxTest::TestSuite { Context* d_ctxt; UserContext* d_uctxt; + ExprManager* d_em; NodeManager* d_nm; - NodeManagerScope* d_scope; + SmtScope* d_scope; + SmtEngine* d_smt; TestOutputChannel d_outputChannel; LogicInfo d_logicInfo; Theory::Effort d_level; - QuantifiersEngine* d_quantifiersEngine; TheoryArith* d_arith; TypeNode* d_booleanType; @@ -96,14 +101,22 @@ public: } void setUp() { - d_ctxt = new Context(); - d_uctxt = new UserContext(); - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); + d_em = new ExprManager(); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_em); + d_ctxt = d_smt->d_context; + d_uctxt = d_smt->d_userContext; + d_scope = new SmtScope(d_smt); d_outputChannel.clear(); d_logicInfo.lock(); - d_quantifiersEngine = new QuantifiersEngine(d_ctxt, NULL); - d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_quantifiersEngine); + + // guard against duplicate statistics assertion errors + delete d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]; + delete d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH]; + d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL; + d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL; + + d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_smt->d_theoryEngine->d_quantEngine); preregistered = new std::set<Node>(); @@ -119,12 +132,10 @@ public: delete preregistered; delete d_arith; - delete d_quantifiersEngine; d_outputChannel.clear(); delete d_scope; - delete d_nm; - delete d_uctxt; - delete d_ctxt; + delete d_smt; + delete d_em; } void testAssert() { diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index ae61bd0d3..ee637daac 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -34,6 +34,8 @@ #include "expr/node_manager.h" #include "expr/kind.h" #include "context/context.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "util/rational.h" #include "util/integer.h" #include "util/options.h" @@ -44,6 +46,7 @@ using namespace CVC4::theory; using namespace CVC4::expr; using namespace CVC4::context; using namespace CVC4::kind; +using namespace CVC4::smt; using namespace std; @@ -233,49 +236,47 @@ class TheoryEngineWhite : public CxxTest::TestSuite { Context* d_ctxt; UserContext* d_uctxt; + ExprManager* d_em; NodeManager* d_nm; - NodeManagerScope* d_scope; + SmtEngine* d_smt; + SmtScope* d_scope; FakeOutputChannel *d_nullChannel; TheoryEngine* d_theoryEngine; - LogicInfo* d_logicInfo; public: void setUp() { - d_ctxt = new Context(); - d_uctxt = new UserContext(); + d_em = new ExprManager(); + d_smt = new SmtEngine(d_em); + d_nm = NodeManager::fromExprManager(d_em); + d_scope = new SmtScope(d_smt); - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); + d_ctxt = d_smt->d_context; + d_uctxt = d_smt->d_userContext; d_nullChannel = new FakeOutputChannel(); - // create the TheoryEngine - d_logicInfo = new LogicInfo(); - d_theoryEngine = new TheoryEngine(d_ctxt, d_uctxt, *d_logicInfo); - + d_theoryEngine = d_smt->d_theoryEngine; + for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) { + delete d_theoryEngine->d_theoryOut[id]; + delete d_theoryEngine->d_theoryTable[id]; + d_theoryEngine->d_theoryOut[id] = NULL; + d_theoryEngine->d_theoryTable[id] = NULL; + } d_theoryEngine->addTheory< FakeTheory<THEORY_BUILTIN> >(THEORY_BUILTIN); d_theoryEngine->addTheory< FakeTheory<THEORY_BOOL> >(THEORY_BOOL); d_theoryEngine->addTheory< FakeTheory<THEORY_UF> >(THEORY_UF); d_theoryEngine->addTheory< FakeTheory<THEORY_ARITH> >(THEORY_ARITH); d_theoryEngine->addTheory< FakeTheory<THEORY_ARRAY> >(THEORY_ARRAY); d_theoryEngine->addTheory< FakeTheory<THEORY_BV> >(THEORY_BV); - - //Debug.on("theory-rewrite"); } void tearDown() { - d_theoryEngine->shutdown(); - delete d_theoryEngine; - delete d_logicInfo; - delete d_nullChannel; delete d_scope; - delete d_nm; - - delete d_uctxt; - delete d_ctxt; + delete d_smt; + delete d_em; } void testRewriterSimple() { diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_white.h index 74f5870a3..5b46aee4f 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_white.h @@ -19,9 +19,12 @@ #include <cxxtest/TestSuite.h> #include "theory/theory.h" +#include "theory/theory_engine.h" #include "expr/node.h" #include "expr/node_manager.h" #include "context/context.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include <vector> @@ -29,6 +32,7 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::expr; using namespace CVC4::context; +using namespace CVC4::smt; using namespace std; @@ -159,7 +163,9 @@ class TheoryBlack : public CxxTest::TestSuite { Context* d_ctxt; UserContext* d_uctxt; NodeManager* d_nm; - NodeManagerScope* d_scope; + ExprManager* d_em; + SmtScope* d_scope; + SmtEngine* d_smt; LogicInfo* d_logicInfo; TestOutputChannel d_outputChannel; @@ -172,12 +178,21 @@ class TheoryBlack : public CxxTest::TestSuite { public: void setUp() { - d_ctxt = new Context(); - d_uctxt = new UserContext(); - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); + d_em = new ExprManager(); + d_nm = NodeManager::fromExprManager(d_em); + d_smt = new SmtEngine(d_em); + d_ctxt = d_smt->d_context; + d_uctxt = d_smt->d_userContext; + d_scope = new SmtScope(d_smt); d_logicInfo = new LogicInfo(); d_logicInfo->lock(); + + // guard against duplicate statistics assertion errors + delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN]; + delete d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN]; + d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN] = NULL; + d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN] = NULL; + d_dummy = new DummyTheory(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), *d_logicInfo, NULL); d_outputChannel.clear(); atom0 = d_nm->mkConst(true); @@ -190,9 +205,8 @@ public: delete d_dummy; delete d_logicInfo; delete d_scope; - delete d_nm; - delete d_uctxt; - delete d_ctxt; + delete d_smt; + delete d_em; } void testEffort(){ |