diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-07 18:18:54 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-07 18:18:54 -0500 |
| commit | 6b673474218c300576cae43388b513c7fc8448f8 (patch) | |
| tree | 693a7b7ccbcb7a5a20b45df4c3564cf93dc0f2d3 | |
| parent | 55767b9620f18763b7b56ecefa954202d35fe2d3 (diff) | |
Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)
This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.
The changes that were required for this PR include:
The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.
61 files changed, 397 insertions, 903 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 49093acf5..a04b5cf85 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2670,12 +2670,11 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const Solver::Solver(Options* opts) { - Options* o = opts == nullptr ? new Options() : opts; - d_exprMgr.reset(new ExprManager(*o)); - d_smtEngine.reset(new SmtEngine(d_exprMgr.get())); + d_exprMgr.reset(new ExprManager); + d_smtEngine.reset(new SmtEngine(d_exprMgr.get(), opts)); d_smtEngine->setSolver(this); - d_rng.reset(new Random((*o)[options::seed])); - if (opts == nullptr) delete o; + Options& o = d_smtEngine->getOptions(); + d_rng.reset(new Random(o[options::seed])); } Solver::~Solver() {} @@ -4148,7 +4147,7 @@ Result Solver::checkEntailed(Term term) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); CVC4_API_CHECK(!d_smtEngine->isQueryMade() - || CVC4::options::incrementalSolving()) + || d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC4_API_ARG_CHECK_NOT_NULL(term); @@ -4165,7 +4164,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); CVC4_API_CHECK(!d_smtEngine->isQueryMade() - || CVC4::options::incrementalSolving()) + || d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; for (const Term& term : terms) @@ -4204,7 +4203,7 @@ Result Solver::checkSat(void) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); CVC4_API_CHECK(!d_smtEngine->isQueryMade() - || CVC4::options::incrementalSolving()) + || d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC4::Result r = d_smtEngine->checkSat(); @@ -4220,7 +4219,7 @@ Result Solver::checkSatAssuming(Term assumption) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); CVC4_API_CHECK(!d_smtEngine->isQueryMade() - || CVC4::options::incrementalSolving()) + || d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; CVC4_API_SOLVER_CHECK_TERM(assumption); @@ -4237,7 +4236,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); CVC4_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0 - || CVC4::options::incrementalSolving()) + || d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; for (const Term& term : assumptions) @@ -4641,7 +4640,7 @@ std::vector<std::pair<Term, Term>> Solver::getAssignment(void) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(CVC4::options::produceAssignments()) + CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceAssignments]) << "Cannot get assignment unless assignment generation is enabled " "(try --produce-assignments)"; std::vector<std::pair<Expr, Expr>> assignment = d_smtEngine->getAssignment(); @@ -4685,10 +4684,10 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(CVC4::options::incrementalSolving()) + CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot get unsat assumptions unless incremental solving is enabled " "(try --incremental)"; - CVC4_API_CHECK(CVC4::options::unsatAssumptions()) + CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions]) << "Cannot get unsat assumptions unless explicitly enabled " "(try --produce-unsat-assumptions)"; CVC4_API_CHECK(d_smtEngine->getSmtMode() @@ -4715,7 +4714,7 @@ std::vector<Term> Solver::getUnsatCore(void) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(CVC4::options::unsatCores()) + CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatCores]) << "Cannot get unsat core unless explicitly enabled " "(try --produce-unsat-cores)"; CVC4_API_CHECK(d_smtEngine->getSmtMode() @@ -4752,7 +4751,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(CVC4::options::produceModels()) + CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC4_API_CHECK(d_smtEngine->getSmtMode() @@ -4779,7 +4778,7 @@ Term Solver::getSeparationHeap() const << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(CVC4::options::produceModels()) + CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation heap term unless model generation is enabled " "(try --produce-models)"; CVC4_API_CHECK(d_smtEngine->getSmtMode() @@ -4804,7 +4803,7 @@ Term Solver::getSeparationNilTerm() const << "Cannot obtain separation logic expressions if not using the " "separation logic theory."; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(CVC4::options::produceModels()) + CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get separation nil term unless model generation is enabled " "(try --produce-models)"; CVC4_API_CHECK(d_smtEngine->getSmtMode() @@ -4828,7 +4827,7 @@ void Solver::pop(uint32_t nscopes) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(CVC4::options::incrementalSolving()) + CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot pop when not solving incrementally (use --incremental)"; CVC4_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels()) << "Cannot pop beyond first pushed context"; @@ -4870,7 +4869,7 @@ void Solver::printModel(std::ostream& out) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(CVC4::options::produceModels()) + CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels]) << "Cannot get value unless model generation is enabled " "(try --produce-models)"; CVC4_API_CHECK(d_smtEngine->getSmtMode() @@ -4887,7 +4886,7 @@ void Solver::push(uint32_t nscopes) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(CVC4::options::incrementalSolving()) + CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving]) << "Cannot push when not solving incrementally (use --incremental)"; for (uint32_t n = 0; n < nscopes; ++n) @@ -5285,6 +5284,12 @@ ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); } */ SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); } +/** + * !!! This is only temporarily available until the parser is fully migrated to + * the new API. !!! + */ +Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); } + /* -------------------------------------------------------------------------- */ /* Conversions */ /* -------------------------------------------------------------------------- */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 5223c9de6..91db4dd58 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2053,7 +2053,7 @@ class CVC4_PUBLIC Solver /** * Constructor. - * @param opts a pointer to a solver options object (for parser only) + * @param opts an optional pointer to a solver options object * @return the Solver */ Solver(Options* opts = nullptr); @@ -3263,6 +3263,10 @@ class CVC4_PUBLIC Solver // to the new API. !!! SmtEngine* getSmtEngine(void) const; + // !!! This is only temporarily available until options are refactored at + // the driver level. !!! + Options& getOptions(void); + private: /* Helper to convert a vector of internal types to sorts. */ std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const; diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index b042b9352..9222393c4 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -27,8 +27,6 @@ libcvc4_add_sources( node_manager.cpp node_manager.h node_manager_attributes.h - node_manager_listeners.cpp - node_manager_listeners.h node_self_iterator.h node_trie.cpp node_trie.h diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index d69dc73f9..7bec489a3 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -92,18 +92,6 @@ ExprManager::ExprManager() : #endif } -ExprManager::ExprManager(const Options& options) : - d_nodeManager(new NodeManager(this, options)) { -#ifdef CVC4_STATISTICS_ON - for (unsigned i = 0; i <= LAST_TYPE; ++ i) { - d_exprStatisticsVars[i] = NULL; - } - for (unsigned i = 0; i < kind::LAST_KIND; ++ i) { - d_exprStatistics[i] = NULL; - } -#endif -} - ExprManager::~ExprManager() { NodeManagerScope nms(d_nodeManager); @@ -137,15 +125,6 @@ ExprManager::~ExprManager() } } -const Options& ExprManager::getOptions() const { - return d_nodeManager->getOptions(); -} - -ResourceManager* ExprManager::getResourceManager() -{ - return d_nodeManager->getResourceManager(); -} - BooleanType ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()))); @@ -915,9 +894,6 @@ Type ExprManager::getType(Expr expr, bool check) } Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) { - Assert(NodeManager::currentNM() == NULL) - << "ExprManager::mkVar() should only be called externally, not from " - "within CVC4 code. Please use mkSkolem()."; NodeManagerScope nms(d_nodeManager); Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags); Debug("nm") << "set " << name << " on " << *n << std::endl; @@ -926,9 +902,6 @@ Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) { } Expr ExprManager::mkVar(Type type, uint32_t flags) { - Assert(NodeManager::currentNM() == NULL) - << "ExprManager::mkVar() should only be called externally, not from " - "within CVC4 code. Please use mkSkolem()."; NodeManagerScope nms(d_nodeManager); INC_STAT_VAR(type, false); return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags)); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 4dfd77686..db5d22fa8 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -88,19 +88,8 @@ class CVC4_PUBLIC ExprManager { /** A list of datatypes owned by this expr manager. */ std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes; - /** - * Creates an expression manager with default options. - */ + /** Creates an expression manager. */ ExprManager(); - - /** - * Creates an expression manager. - * - * @param options the earlyTypeChecking field is used to configure - * whether to do at Expr creation time. - */ - explicit ExprManager(const Options& options); - public: /** * Destroys the expression manager. No will be deallocated at this point, so @@ -109,12 +98,6 @@ class CVC4_PUBLIC ExprManager { */ ~ExprManager(); - /** Get this expr manager's options */ - const Options& getOptions() const; - - /** Get this expr manager's resource manager */ - ResourceManager* getResourceManager(); - /** Get the type for booleans */ BooleanType booleanType() const; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 88c4db778..c68b0df86 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -26,7 +26,6 @@ #include "expr/attribute.h" #include "expr/dtype.h" #include "expr/node_manager_attributes.h" -#include "expr/node_manager_listeners.h" #include "expr/skolem_manager.h" #include "expr/type_checker.h" #include "options/options.h" @@ -93,11 +92,8 @@ namespace attr { typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAttr; NodeManager::NodeManager(ExprManager* exprManager) - : d_options(new Options()), - d_statisticsRegistry(new StatisticsRegistry()), - d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)), + : d_statisticsRegistry(new StatisticsRegistry()), d_skManager(new SkolemManager), - d_registrations(new ListenerRegistrationList()), next_id(0), d_attrManager(new expr::attr::AttributeManager()), d_exprManager(exprManager), @@ -109,24 +105,6 @@ NodeManager::NodeManager(ExprManager* exprManager) init(); } -NodeManager::NodeManager(ExprManager* exprManager, const Options& options) - : d_options(new Options()), - d_statisticsRegistry(new StatisticsRegistry()), - d_resourceManager(new ResourceManager(*d_statisticsRegistry, *d_options)), - d_skManager(new SkolemManager), - d_registrations(new ListenerRegistrationList()), - next_id(0), - d_attrManager(new expr::attr::AttributeManager()), - d_exprManager(exprManager), - d_nodeUnderDeletion(NULL), - d_inReclaimZombies(false), - d_abstractValueCount(0), - d_skolemCounter(0) -{ - d_options->copyValues(options); - init(); -} - void NodeManager::init() { poolInsert( &expr::NodeValue::null() ); @@ -137,32 +115,6 @@ void NodeManager::init() { d_operators[i] = mkConst(Kind(k)); } } - d_resourceManager->setHardLimit((*d_options)[options::hardLimit]); - if((*d_options)[options::perCallResourceLimit] != 0) { - d_resourceManager->setResourceLimit((*d_options)[options::perCallResourceLimit], false); - } - if((*d_options)[options::cumulativeResourceLimit] != 0) { - d_resourceManager->setResourceLimit((*d_options)[options::cumulativeResourceLimit], true); - } - if((*d_options)[options::perCallMillisecondLimit] != 0) { - d_resourceManager->setTimeLimit((*d_options)[options::perCallMillisecondLimit], false); - } - if((*d_options)[options::cumulativeMillisecondLimit] != 0) { - d_resourceManager->setTimeLimit((*d_options)[options::cumulativeMillisecondLimit], true); - } - if((*d_options)[options::cpuTime]) { - d_resourceManager->useCPUTime(true); - } - - // Do not notify() upon registration as these were handled manually above. - d_registrations->add(d_options->registerTlimitListener( - new TlimitListener(d_resourceManager), false)); - d_registrations->add(d_options->registerTlimitPerListener( - new TlimitPerListener(d_resourceManager), false)); - d_registrations->add(d_options->registerRlimitListener( - new RlimitListener(d_resourceManager), false)); - d_registrations->add(d_options->registerRlimitPerListener( - new RlimitPerListener(d_resourceManager), false)); } NodeManager::~NodeManager() { @@ -234,16 +186,10 @@ NodeManager::~NodeManager() { } // defensive coding, in case destruction-order issues pop up (they often do) - delete d_resourceManager; - d_resourceManager = NULL; delete d_statisticsRegistry; d_statisticsRegistry = NULL; - delete d_registrations; - d_registrations = NULL; delete d_attrManager; d_attrManager = NULL; - delete d_options; - d_options = NULL; } size_t NodeManager::registerDatatype(std::shared_ptr<DType> dt) diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 098ff8eea..499cba457 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -109,20 +109,11 @@ class NodeManager { static thread_local NodeManager* s_current; - Options* d_options; StatisticsRegistry* d_statisticsRegistry; - ResourceManager* d_resourceManager; - /** The skolem manager */ std::shared_ptr<SkolemManager> d_skManager; - /** - * A list of registrations on d_options to that call into d_resourceManager. - * These must be garbage collected before d_options and d_resourceManager. - */ - ListenerRegistrationList* d_registrations; - NodeValuePool d_nodeValuePool; size_t next_id; @@ -389,26 +380,10 @@ class NodeManager { public: explicit NodeManager(ExprManager* exprManager); - explicit NodeManager(ExprManager* exprManager, const Options& options); ~NodeManager(); /** The node manager in the current public-facing CVC4 library context */ static NodeManager* currentNM() { return s_current; } - /** The resource manager associated with the current node manager */ - static ResourceManager* currentResourceManager() { return s_current->d_resourceManager; } - - /** Get this node manager's options (const version) */ - const Options& getOptions() const { - return *d_options; - } - - /** Get this node manager's options (non-const version) */ - Options& getOptions() { - return *d_options; - } - - /** Get this node manager's resource manager */ - ResourceManager* getResourceManager() { return d_resourceManager; } /** Get this node manager's skolem manager */ SkolemManager* getSkolemManager() { return d_skManager.get(); } @@ -1037,25 +1012,19 @@ public: class NodeManagerScope { /** The old NodeManager, to be restored on destruction. */ NodeManager* d_oldNodeManager; - Options::OptionsScope d_optionsScope; public: - - NodeManagerScope(NodeManager* nm) - : d_oldNodeManager(NodeManager::s_current) - , d_optionsScope(nm ? nm->d_options : NULL) { - // There are corner cases where nm can be NULL and it's ok. - // For example, if you write { Expr e; }, then when the null - // Expr is destructed, there's no active node manager. - //Assert(nm != NULL); - NodeManager::s_current = nm; - //Options::s_current = nm ? nm->d_options : NULL; - Debug("current") << "node manager scope: " - << NodeManager::s_current << "\n"; + NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) + { + // There are corner cases where nm can be NULL and it's ok. + // For example, if you write { Expr e; }, then when the null + // Expr is destructed, there's no active node manager. + // Assert(nm != NULL); + NodeManager::s_current = nm; + Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; } ~NodeManagerScope() { NodeManager::s_current = d_oldNodeManager; - //Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL; Debug("current") << "node manager scope: " << "returning to " << NodeManager::s_current << "\n"; } diff --git a/src/expr/node_manager_listeners.cpp b/src/expr/node_manager_listeners.cpp deleted file mode 100644 index 56a827deb..000000000 --- a/src/expr/node_manager_listeners.cpp +++ /dev/null @@ -1,44 +0,0 @@ -/********************* */ -/*! \file node_manager_listeners.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Listeners that NodeManager registers to its Options object. - ** - ** Listeners that NodeManager registers to its Options object. - **/ - -#include "node_manager_listeners.h" - -#include "base/listener.h" -#include "options/smt_options.h" -#include "util/resource_manager.h" - -namespace CVC4 { -namespace expr { - - -void TlimitListener::notify() { - d_rm->setTimeLimit(options::cumulativeMillisecondLimit(), true); -} - -void TlimitPerListener::notify() { - d_rm->setTimeLimit(options::perCallMillisecondLimit(), false); -} - -void RlimitListener::notify() { - d_rm->setTimeLimit(options::cumulativeResourceLimit(), true); -} - -void RlimitPerListener::notify() { - d_rm->setTimeLimit(options::perCallResourceLimit(), false); -} - -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ diff --git a/src/expr/node_manager_listeners.h b/src/expr/node_manager_listeners.h deleted file mode 100644 index e296b7ec6..000000000 --- a/src/expr/node_manager_listeners.h +++ /dev/null @@ -1,67 +0,0 @@ -/********************* */ -/*! \file node_manager_listeners.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Mathias Preiner - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Listeners that NodeManager registers to its Options object. - ** - ** Listeners that NodeManager registers to its Options object. - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__EXPR__NODE_MANAGER_LISTENERS_H -#define CVC4__EXPR__NODE_MANAGER_LISTENERS_H - -#include "base/listener.h" -#include "util/resource_manager.h" - -namespace CVC4 { -namespace expr { - -class TlimitListener : public Listener { - public: - TlimitListener(ResourceManager* rm) : d_rm(rm) {} - void notify() override; - - private: - ResourceManager* d_rm; -}; - -class TlimitPerListener : public Listener { - public: - TlimitPerListener(ResourceManager* rm) : d_rm(rm) {} - void notify() override; - - private: - ResourceManager* d_rm; -}; - -class RlimitListener : public Listener { - public: - RlimitListener(ResourceManager* rm) : d_rm(rm) {} - void notify() override; - - private: - ResourceManager* d_rm; -}; - -class RlimitPerListener : public Listener { - public: - RlimitPerListener(ResourceManager* rm) : d_rm(rm) {} - void notify() override; - - private: - ResourceManager* d_rm; -}; - -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ - -#endif /* CVC4__EXPR__NODE_MANAGER_LISTENERS_H */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 7a39f5fc2..374f68257 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -193,8 +193,8 @@ int runCvc4(int argc, char* argv[], Options& opts) { ReferenceStat<std::string> s_statFilename("filename", filenameStr); RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(), &s_statFilename); - // set filename in smt engine - pExecutor->getSmtEngine()->setFilename(filenameStr); + // notify SmtEngine that we are starting to parse + pExecutor->getSmtEngine()->notifyStartParsing(filenameStr); // Parse and execute commands until we are done Command* cmd; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index bb28c6dbc..17b792ab4 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -85,7 +85,7 @@ static set<string> s_declarations; #endif /* HAVE_LIBREADLINE */ InteractiveShell::InteractiveShell(api::Solver* solver) - : d_options(solver->getExprManager()->getOptions()), + : d_options(solver->getOptions()), d_in(*d_options.getIn()), d_out(*d_options.getOutConst()), d_quit(false) diff --git a/src/options/options.h b/src/options/options.h index b561b3426..e0f68a182 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -54,18 +54,6 @@ class CVC4_PUBLIC Options { /** Listeners for notifyBeforeSearch. */ ListenerCollection d_beforeSearchListeners; - /** Listeners for options::tlimit. */ - ListenerCollection d_tlimitListeners; - - /** Listeners for options::tlimit-per. */ - ListenerCollection d_tlimitPerListeners; - - /** Listeners for options::rlimit. */ - ListenerCollection d_rlimitListeners; - - /** Listeners for options::tlimit-per. */ - ListenerCollection d_rlimitPerListeners; - /** Listeners for options::defaultExprDepth. */ ListenerCollection d_setDefaultExprDepthListeners; @@ -324,55 +312,6 @@ public: Listener* listener); /** - * Registers a listener for options::tlimit being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerTlimitListener( - Listener* listener, bool notifyIfSet); - - /** - * Registers a listener for options::tlimit-per being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerTlimitPerListener( - Listener* listener, bool notifyIfSet); - - - /** - * Registers a listener for options::rlimit being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerRlimitListener( - Listener* listener, bool notifyIfSet); - - /** - * Registers a listener for options::rlimit-per being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerRlimitPerListener( - Listener* listener, bool notifyIfSet); - - /** * Registers a listener for options::defaultExprDepth being set. * * If notifyIfSet is true, this calls notify on the listener diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 500cd90c5..dd5265777 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -80,23 +80,6 @@ void OptionsHandler::notifyBeforeSearch(const std::string& option) } } - -void OptionsHandler::notifyTlimit(const std::string& option) { - d_options->d_tlimitListeners.notify(); -} - -void OptionsHandler::notifyTlimitPer(const std::string& option) { - d_options->d_tlimitPerListeners.notify(); -} - -void OptionsHandler::notifyRlimit(const std::string& option) { - d_options->d_rlimitListeners.notify(); -} - -void OptionsHandler::notifyRlimitPer(const std::string& option) { - d_options->d_rlimitPerListeners.notify(); -} - unsigned long OptionsHandler::limitHandler(std::string option, std::string optarg) { diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 9a5af8865..876edfad7 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -97,12 +97,6 @@ public: unsigned long limitHandler(std::string option, std::string optarg); - void notifyTlimit(const std::string& option); - void notifyTlimitPer(const std::string& option); - void notifyRlimit(const std::string& option); - void notifyRlimitPer(const std::string& option); - - /* expr/options_handlers.h */ void setDefaultExprDepthPredicate(std::string option, int depth); void setDefaultDagThreshPredicate(std::string option, int dag); diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 234ddd5b4..bf8926521 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -228,10 +228,6 @@ Options::Options() : d_holder(new options::OptionsHolder()) , d_handler(new options::OptionsHandler(this)) , d_beforeSearchListeners() - , d_tlimitListeners() - , d_tlimitPerListeners() - , d_rlimitListeners() - , d_rlimitPerListeners() {} Options::~Options() { @@ -284,35 +280,6 @@ ListenerCollection::Registration* Options::registerBeforeSearchListener( return d_beforeSearchListeners.registerListener(listener); } -ListenerCollection::Registration* Options::registerTlimitListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && - wasSetByUser(options::cumulativeMillisecondLimit); - return registerAndNotify(d_tlimitListeners, listener, notify); -} - -ListenerCollection::Registration* Options::registerTlimitPerListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::perCallMillisecondLimit); - return registerAndNotify(d_tlimitPerListeners, listener, notify); -} - -ListenerCollection::Registration* Options::registerRlimitListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::cumulativeResourceLimit); - return registerAndNotify(d_rlimitListeners, listener, notify); -} - -ListenerCollection::Registration* Options::registerRlimitPerListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::perCallResourceLimit); - return registerAndNotify(d_rlimitPerListeners, listener, notify); -} - ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener( Listener* listener, bool notifyIfSet) { @@ -373,13 +340,6 @@ Options::registerSetDiagnosticOutputChannelListener( ${custom_handlers}$ - -#ifdef CVC4_DEBUG -# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true -#else /* CVC4_DEBUG */ -# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false -#endif /* CVC4_DEBUG */ - #if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE) # define DO_SEMANTIC_CHECKS_BY_DEFAULT false #else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */ @@ -703,7 +663,7 @@ std::vector<std::vector<std::string> > Options::getOptions() const void Options::setOption(const std::string& key, const std::string& optionarg) { options::OptionsHandler* handler = d_handler; - Options *options = Options::current(); + Options* options = this; Trace("options") << "SMT setOption(" << key << ", " << optionarg << ")" << std::endl; diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 8ae6ea89a..2fb5dd0ba 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1608,15 +1608,6 @@ header = "options/quantifiers_options.h" default = "false" help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones" - -[[option]] - name = "sygusExprMinerCheckUseExport" - category = "expert" - long = "sygus-expr-miner-check-use-export" - type = "bool" - default = "true" - help = "export expressions to a different ExprManager with different options for satisfiability checks in expression miners" - # CEGQI applied to general quantified formulas [[option]] diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index c09f8bbf3..0a3d65167 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -280,7 +280,6 @@ header = "options/smt_options.h" long = "check-synth-sol" type = "bool" default = "false" - read_only = true help = "checks whether produced solutions to functions-to-synthesize satisfy the conjecture" [[option]] @@ -451,7 +450,6 @@ header = "options/smt_options.h" long = "tlimit=MS" type = "unsigned long" handler = "limitHandler" - notifies = ["notifyTlimit"] read_only = true help = "enable time limiting (give milliseconds)" @@ -462,7 +460,6 @@ header = "options/smt_options.h" long = "tlimit-per=MS" type = "unsigned long" handler = "limitHandler" - notifies = ["notifyTlimitPer"] read_only = true help = "enable time limiting per query (give milliseconds)" @@ -473,7 +470,6 @@ header = "options/smt_options.h" long = "rlimit=N" type = "unsigned long" handler = "limitHandler" - notifies = ["notifyRlimit"] read_only = true help = "enable resource limiting (currently, roughly the number of SAT conflicts)" @@ -484,7 +480,6 @@ header = "options/smt_options.h" long = "rlimit-per=N" type = "unsigned long" handler = "limitHandler" - notifies = ["notifyRlimitPer"] read_only = true help = "enable resource limiting per query" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index a5ce1bed0..bf12ee87d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -35,7 +35,6 @@ #include "parser/input.h" #include "parser/parser_exception.h" #include "smt/command.h" -#include "util/resource_manager.h" using namespace std; using namespace CVC4::kind; @@ -47,8 +46,7 @@ Parser::Parser(api::Solver* solver, Input* input, bool strictMode, bool parseOnly) - : d_resourceManager(solver->getExprManager()->getResourceManager()), - d_input(input), + : d_input(input), d_symtabAllocated(), d_symtab(&d_symtabAllocated), d_assertionLevel(0), @@ -743,19 +741,12 @@ Command* Parser::nextCommand() } } Debug("parser") << "nextCommand() => " << cmd << std::endl; - if (cmd != NULL && dynamic_cast<SetOptionCommand*>(cmd) == NULL && - dynamic_cast<QuitCommand*>(cmd) == NULL) { - // don't count set-option commands as to not get stuck in an infinite - // loop of resourcing out - d_resourceManager->spendResource(ResourceManager::Resource::ParseStep); - } return cmd; } api::Term Parser::nextExpression() { Debug("parser") << "nextExpression()" << std::endl; - d_resourceManager->spendResource(ResourceManager::Resource::ParseStep); api::Term result; if (!done()) { try { @@ -920,8 +911,7 @@ std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s) api::Term Parser::mkStringConstant(const std::string& s) { - ExprManager* em = d_solver->getExprManager(); - if (language::isInputLang_smt2_6(em->getOptions().getInputLanguage())) + if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage())) { return api::Term(d_solver, d_solver->mkString(s, true).getExpr()); } diff --git a/src/parser/parser.h b/src/parser/parser.h index 84dd4be0c..b993b08fb 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -135,8 +135,6 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) { class CVC4_PUBLIC Parser { friend class ParserBuilder; private: - /** The resource manager associated with this expr manager */ - ResourceManager* d_resourceManager; /** The input that we're parsing. */ Input* d_input; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index aba409109..46a2e2c59 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -332,8 +332,7 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const bool Smt2::isHoEnabled() const { - return getLogic().isHigherOrder() - && d_solver->getExprManager()->getOptions().getUfHo(); + return getLogic().isHigherOrder() && d_solver->getOptions().getUfHo(); } bool Smt2::logicIsSet() { @@ -999,7 +998,7 @@ void Smt2::addSygusConstructorVariables(api::DatatypeDecl& dt, InputLanguage Smt2::getLanguage() const { - return d_solver->getExprManager()->getOptions().getInputLanguage(); + return d_solver->getOptions().getInputLanguage(); } void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) @@ -1162,7 +1161,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args) } } // Second phase: apply the arguments to the parse op - const Options& opts = d_solver->getExprManager()->getOptions(); + const Options& opts = d_solver->getOptions(); // handle special cases if (p.d_kind == api::CONST_ARRAY && !p.d_type.isNull()) { diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 403cab42b..cb4d3fd9e 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -311,7 +311,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args) isBuiltinKind = true; } assert(kind != api::NULL_EXPR); - const Options& opts = d_solver->getExprManager()->getOptions(); + const Options& opts = d_solver->getOptions(); // Second phase: apply parse op to the arguments if (isBuiltinKind) { diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp index 314c34617..c15867a39 100644 --- a/src/preprocessing/passes/static_learning.cpp +++ b/src/preprocessing/passes/static_learning.cpp @@ -29,8 +29,7 @@ StaticLearning::StaticLearning(PreprocessingPassContext* preprocContext) PreprocessingPassResult StaticLearning::applyInternal( AssertionPipeline* assertionsToPreprocess) { - NodeManager::currentResourceManager()->spendResource( - ResourceManager::Resource::PreprocessStep); + d_preprocContext->spendResource(ResourceManager::Resource::PreprocessStep); for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i) { diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp index d8a587136..4500c7880 100644 --- a/src/preprocessing/passes/sygus_inference.cpp +++ b/src/preprocessing/passes/sygus_inference.cpp @@ -300,8 +300,9 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions, Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl; // make a separate smt call - SmtEngine rrSygus(nm->toExprManager()); - rrSygus.setLogic(smt::currentSmtEngine()->getLogicInfo()); + SmtEngine* currSmt = smt::currentSmtEngine(); + SmtEngine rrSygus(nm->toExprManager(), &currSmt->getOptions()); + rrSygus.setLogic(currSmt->getLogicInfo()); rrSygus.assertFormula(body.toExpr()); Trace("sygus-infer") << "*** Check sat..." << std::endl; Result r = rrSygus.checkSat(); diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index c7e7ae82c..2dfad99c2 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -23,11 +23,10 @@ namespace preprocessing { PreprocessingPassContext::PreprocessingPassContext( SmtEngine* smt, - ResourceManager* resourceManager, RemoveTermFormulas* iteRemover, theory::booleans::CircuitPropagator* circuitPropagator) : d_smt(smt), - d_resourceManager(resourceManager), + d_resourceManager(smt->getResourceManager()), d_iteRemover(iteRemover), d_topLevelSubstitutions(smt->getUserContext()), d_circuitPropagator(circuitPropagator), diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index deb600885..feed945d5 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -39,7 +39,6 @@ class PreprocessingPassContext public: PreprocessingPassContext( SmtEngine* smt, - ResourceManager* resourceManager, RemoveTermFormulas* iteRemover, theory::booleans::CircuitPropagator* circuitPropagator); diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index a7e8e6212..abd44dac7 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1401,24 +1401,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic) options::bvLazyRewriteExtf.set(false); } - if (!options::sygusExprMinerCheckUseExport()) - { - if (options::sygusExprMinerCheckTimeout.wasSetByUser()) - { - throw OptionException( - "--sygus-expr-miner-check-timeout=N requires " - "--sygus-expr-miner-check-use-export"); - } - if (options::sygusRewSynthInput() || options::produceAbducts()) - { - std::stringstream ss; - ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input" - : "--produce-abducts"); - ss << "requires --sygus-expr-miner-check-use-export"; - throw OptionException(ss.str()); - } - } - if (options::stringFMF() && !options::stringProcessLoopMode.wasSetByUser()) { Trace("smt") << "settting stringProcessLoopMode to 'simple' since " diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bb4d82fe0..0d8189aa4 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -273,11 +273,6 @@ class SmtEnginePrivate : public NodeManagerListener { typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap; typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap; - /** - * Manager for limiting time and abstract resource usage. - */ - ResourceManager* d_resourceManager; - /** Manager for the memory of regular-output-channel. */ ManagedRegularOutputChannel d_managedRegularChannel; @@ -373,7 +368,6 @@ class SmtEnginePrivate : public NodeManagerListener { public: SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), - d_resourceManager(NodeManager::currentResourceManager()), d_managedRegularChannel(), d_managedDiagnosticChannel(), d_managedDumpChannel(), @@ -384,7 +378,7 @@ class SmtEnginePrivate : public NodeManagerListener { d_fakeContext(), d_abstractValueMap(&d_fakeContext), d_abstractValues(), - d_processor(smt, *d_resourceManager), + d_processor(smt, *smt.getResourceManager()), // d_needsExpandDefs(true), //TODO? d_exprNames(smt.getUserContext()), d_iteRemover(smt.getUserContext()), @@ -392,17 +386,17 @@ class SmtEnginePrivate : public NodeManagerListener { { d_smt.d_nodeManager->subscribeEvents(this); d_true = NodeManager::currentNM()->mkConst(true); + ResourceManager* rm = d_smt.getResourceManager(); - d_listenerRegistrations->add(d_resourceManager->registerSoftListener( - new SoftResourceOutListener(d_smt))); + d_listenerRegistrations->add( + rm->registerSoftListener(new SoftResourceOutListener(d_smt))); - d_listenerRegistrations->add(d_resourceManager->registerHardListener( - new HardResourceOutListener(d_smt))); + d_listenerRegistrations->add( + rm->registerHardListener(new HardResourceOutListener(d_smt))); try { - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - + Options& opts = d_smt.getOptions(); // Multiple options reuse BeforeSearchListener so registration requires an // extra bit of care. // We can safely not call notify on this before search listener at @@ -410,35 +404,27 @@ class SmtEnginePrivate : public NodeManagerListener { // time. Therefore the BeforeSearchListener is a no-op. Therefore it does // not have to be called. d_listenerRegistrations->add( - nodeManagerOptions.registerBeforeSearchListener( - new BeforeSearchListener(d_smt))); + opts.registerBeforeSearchListener(new BeforeSearchListener(d_smt))); // These do need registration calls. + d_listenerRegistrations->add(opts.registerSetDefaultExprDepthListener( + new SetDefaultExprDepthListener(), true)); + d_listenerRegistrations->add(opts.registerSetDefaultExprDagListener( + new SetDefaultExprDagListener(), true)); + d_listenerRegistrations->add(opts.registerSetPrintExprTypesListener( + new SetPrintExprTypesListener(), true)); d_listenerRegistrations->add( - nodeManagerOptions.registerSetDefaultExprDepthListener( - new SetDefaultExprDepthListener(), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetDefaultExprDagListener( - new SetDefaultExprDagListener(), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetPrintExprTypesListener( - new SetPrintExprTypesListener(), true)); + opts.registerSetDumpModeListener(new DumpModeListener(), true)); + d_listenerRegistrations->add(opts.registerSetPrintSuccessListener( + new PrintSuccessListener(), true)); + d_listenerRegistrations->add(opts.registerSetRegularOutputChannelListener( + new SetToDefaultSourceListener(&d_managedRegularChannel), true)); d_listenerRegistrations->add( - nodeManagerOptions.registerSetDumpModeListener(new DumpModeListener(), - true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetPrintSuccessListener( - new PrintSuccessListener(), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetRegularOutputChannelListener( - new SetToDefaultSourceListener(&d_managedRegularChannel), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetDiagnosticOutputChannelListener( + opts.registerSetDiagnosticOutputChannelListener( new SetToDefaultSourceListener(&d_managedDiagnosticChannel), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerDumpToFileNameListener( - new SetToDefaultSourceListener(&d_managedDumpChannel), true)); + d_listenerRegistrations->add(opts.registerDumpToFileNameListener( + new SetToDefaultSourceListener(&d_managedDumpChannel), true)); } catch (OptionException& e) { @@ -467,11 +453,9 @@ class SmtEnginePrivate : public NodeManagerListener { d_smt.d_nodeManager->unsubscribeEvents(this); } - ResourceManager* getResourceManager() { return d_resourceManager; } - void spendResource(ResourceManager::Resource r) { - d_resourceManager->spendResource(r); + d_smt.getResourceManager()->spendResource(r); } ProcessAssertions* getProcessAssertions() { return &d_processor; } @@ -647,7 +631,7 @@ class SmtEnginePrivate : public NodeManagerListener { }/* namespace CVC4::smt */ -SmtEngine::SmtEngine(ExprManager* em) +SmtEngine::SmtEngine(ExprManager* em, Options* optr) : d_context(new Context()), d_userContext(new UserContext()), d_userLevels(), @@ -677,15 +661,35 @@ SmtEngine::SmtEngine(ExprManager* em) d_smtMode(SMT_MODE_START), d_private(nullptr), d_statisticsRegistry(nullptr), - d_stats(nullptr) -{ - SmtScope smts(this); - d_originalOptions.copyValues(em->getOptions()); - d_private.reset(new smt::SmtEnginePrivate(*this)); + d_stats(nullptr), + d_resourceManager(nullptr), + d_scope(nullptr) +{ + // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SmtEngine + // we are constructing the current SmtEngine in scope for the lifetime of + // this SmtEngine, or until another SmtEngine is constructed (that SmtEngine + // is then in scope during its lifetime). This is mostly to ensure that + // options are always in scope, for e.g. printing expressions, which rely + // on knowing the output language. + // Notice that the SmtEngine may spawn new SmtEngine "subsolvers" internally. + // These are created, used, and deleted in a modular fashion while not + // interleaving calls to the master SmtEngine. Thus the hack here does not + // break this use case. + // On the other hand, this hack breaks use cases where multiple SmtEngine + // objects are created by the user. + d_scope.reset(new SmtScope(this)); + if (optr != nullptr) + { + // if we provided a set of options, copy their values to the options + // owned by this SmtEngine. + d_options.copyValues(*optr); + } d_statisticsRegistry.reset(new StatisticsRegistry()); + d_resourceManager.reset( + new ResourceManager(*d_statisticsRegistry.get(), d_options)); + d_private.reset(new smt::SmtEnginePrivate(*this)); d_stats.reset(new SmtEngineStatistics()); - d_stats->d_resourceUnitsUsed.setData( - d_private->getResourceManager()->getResourceUsage()); + d_stats->d_resourceUnitsUsed.setData(d_resourceManager->getResourceUsage()); // The ProofManager is constructed before any other proof objects such as // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are @@ -705,6 +709,35 @@ SmtEngine::SmtEngine(ExprManager* em) void SmtEngine::finishInit() { + // Notice that finishInit is called when options are finalized. If we are + // parsing smt2, this occurs at the moment we enter "Assert mode", page 52 + // of SMT-LIB 2.6 standard. + + // Inialize the resource manager based on the options. + d_resourceManager->setHardLimit(options::hardLimit()); + if (options::perCallResourceLimit() != 0) + { + d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false); + } + if (options::cumulativeResourceLimit() != 0) + { + d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(), + true); + } + if (options::perCallMillisecondLimit() != 0) + { + d_resourceManager->setTimeLimit(options::perCallMillisecondLimit(), false); + } + if (options::cumulativeMillisecondLimit() != 0) + { + d_resourceManager->setTimeLimit(options::cumulativeMillisecondLimit(), + true); + } + if (options::cpuTime()) + { + d_resourceManager->useCPUTime(true); + } + // set the random seed Random::getRandom().setSeed(options::seed()); @@ -716,6 +749,7 @@ void SmtEngine::finishInit() // engine later (it is non-essential there) d_theoryEngine.reset(new TheoryEngine(getContext(), getUserContext(), + getResourceManager(), d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic))); @@ -735,10 +769,8 @@ void SmtEngine::finishInit() * are unregistered by the obsolete PropEngine object before registered * again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine(getTheoryEngine(), - getContext(), - getUserContext(), - d_private->getResourceManager())); + d_propEngine.reset(new PropEngine( + getTheoryEngine(), getContext(), getUserContext(), getResourceManager())); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -887,9 +919,11 @@ SmtEngine::~SmtEngine() d_propEngine.reset(nullptr); d_stats.reset(nullptr); + d_private.reset(nullptr); + // d_resourceManager must be destroyed before d_statisticsRegistry + d_resourceManager.reset(nullptr); d_statisticsRegistry.reset(nullptr); - d_private.reset(nullptr); d_userContext.reset(nullptr); d_context.reset(nullptr); @@ -934,6 +968,7 @@ void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); } LogicInfo SmtEngine::getLogicInfo() const { return d_logic; } + LogicInfo SmtEngine::getUserLogicInfo() const { // Lock the logic to make sure that this logic can be queried. We create a @@ -942,7 +977,17 @@ LogicInfo SmtEngine::getUserLogicInfo() const res.lock(); return res; } -void SmtEngine::setFilename(std::string filename) { d_filename = filename; } + +void SmtEngine::notifyStartParsing(std::string filename) +{ + d_filename = filename; + + // Copy the original options. This is called prior to beginning parsing. + // Hence reset should revert to these options, which note is after reading + // the command line. + d_originalOptions.copyValues(d_options); +} + std::string SmtEngine::getFilename() const { return d_filename; } void SmtEngine::setLogicInternal() { @@ -1367,8 +1412,8 @@ bool SmtEngine::isDefinedFunction( Expr func ){ void SmtEnginePrivate::finishInit() { - d_preprocessingPassContext.reset(new PreprocessingPassContext( - &d_smt, d_resourceManager, &d_iteRemover, &d_propagator)); + d_preprocessingPassContext.reset( + new PreprocessingPassContext(&d_smt, &d_iteRemover, &d_propagator)); // initialize the preprocessing passes d_processor.finishInit(d_preprocessingPassContext.get()); @@ -1380,15 +1425,14 @@ Result SmtEngine::check() { Trace("smt") << "SmtEngine::check()" << endl; - ResourceManager* resourceManager = d_private->getResourceManager(); - - resourceManager->beginCall(); + d_resourceManager->beginCall(); // Only way we can be out of resource is if cumulative budget is on - if (resourceManager->cumulativeLimitOn() && - resourceManager->out()) { - Result::UnknownExplanation why = resourceManager->outOfResources() ? - Result::RESOURCEOUT : Result::TIMEOUT; + if (d_resourceManager->cumulativeLimitOn() && d_resourceManager->out()) + { + Result::UnknownExplanation why = d_resourceManager->outOfResources() + ? Result::RESOURCEOUT + : Result::TIMEOUT; return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename); } @@ -1403,10 +1447,10 @@ Result SmtEngine::check() { Trace("smt") << "SmtEngine::check(): running check" << endl; Result result = d_propEngine->checkSat(); - resourceManager->endCall(); - Trace("limit") << "SmtEngine::check(): cumulative millis " << resourceManager->getTimeUsage() - << ", resources " << resourceManager->getResourceUsage() << endl; - + d_resourceManager->endCall(); + Trace("limit") << "SmtEngine::check(): cumulative millis " + << d_resourceManager->getTimeUsage() << ", resources " + << d_resourceManager->getResourceUsage() << endl; return Result(result, d_filename); } @@ -1795,9 +1839,10 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions, return r; } catch (UnsafeInterruptException& e) { - AlwaysAssert(d_private->getResourceManager()->out()); - Result::UnknownExplanation why = d_private->getResourceManager()->outOfResources() ? - Result::RESOURCEOUT : Result::TIMEOUT; + AlwaysAssert(d_resourceManager->out()); + Result::UnknownExplanation why = d_resourceManager->outOfResources() + ? Result::RESOURCEOUT + : Result::TIMEOUT; return Result(Result::SAT_UNKNOWN, why, d_filename); } } @@ -2535,8 +2580,11 @@ void SmtEngine::checkUnsatCore() { Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl; UnsatCore core = getUnsatCore(); - SmtEngine coreChecker(d_exprManager); + SmtEngine coreChecker(d_exprManager, &d_options); + coreChecker.setIsInternalSubsolver(); coreChecker.setLogic(getLogicInfo()); + coreChecker.getOptions().set(options::checkUnsatCores, false); + coreChecker.getOptions().set(options::checkProofs, false); PROOF( std::vector<Command*>::const_iterator itg = d_defineCommands.begin(); @@ -2550,14 +2598,10 @@ void SmtEngine::checkUnsatCore() { Notice() << "SmtEngine::checkUnsatCore(): pushing core member " << *i << endl; coreChecker.assertFormula(*i); } - const bool checkUnsatCores = options::checkUnsatCores(); Result r; try { - options::checkUnsatCores.set(false); - options::checkProofs.set(false); r = coreChecker.checkSat(); } catch(...) { - options::checkUnsatCores.set(checkUnsatCores); throw; } Notice() << "SmtEngine::checkUnsatCore(): result is " << r << endl; @@ -2832,10 +2876,11 @@ void SmtEngine::checkSynthSolution() } Trace("check-synth-sol") << "Starting new SMT Engine\n"; /* Start new SMT engine to check solutions */ - SmtEngine solChecker(d_exprManager); + SmtEngine solChecker(d_exprManager, &d_options); + solChecker.setIsInternalSubsolver(); solChecker.setLogic(getLogicInfo()); - setOption("check-synth-sol", SExpr("false")); - setOption("sygus-rec-fun", SExpr("false")); + solChecker.getOptions().set(options::checkSynthSol, false); + solChecker.getOptions().set(options::sygusRecFun, false); Trace("check-synth-sol") << "Retrieving assertions\n"; // Build conjecture from original assertions @@ -2956,7 +3001,8 @@ void SmtEngine::checkAbduct(Expr a) Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j << ": make new SMT engine" << std::endl; // Start new SMT engine to check solution - SmtEngine abdChecker(d_exprManager); + SmtEngine abdChecker(d_exprManager, &d_options); + abdChecker.setIsInternalSubsolver(); abdChecker.setLogic(getLogicInfo()); Trace("check-abduct") << "SmtEngine::checkAbduct: phase " << j << ": asserting formulas" << std::endl; @@ -3208,7 +3254,8 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd) Trace("sygus-abduct") << "SmtEngine::getAbduct: made conjecture : " << aconj << ", solving for " << d_sssf << std::endl; // we generate a new smt engine to do the abduction query - d_subsolver.reset(new SmtEngine(NodeManager::currentNM()->toExprManager())); + d_subsolver.reset( + new SmtEngine(NodeManager::currentNM()->toExprManager(), &d_options)); d_subsolver->setIsInternalSubsolver(); // get the logic LogicInfo l = d_logic.getUnlockedCopy(); @@ -3477,8 +3524,7 @@ void SmtEngine::reset() Options opts; opts.copyValues(d_originalOptions); this->~SmtEngine(); - NodeManager::fromExprManager(em)->getOptions().copyValues(opts); - new(this) SmtEngine(em); + new (this) SmtEngine(em, &opts); } void SmtEngine::resetAssertions() @@ -3522,10 +3568,8 @@ void SmtEngine::resetAssertions() * statistics are unregistered by the obsolete PropEngine object before * registered again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine(getTheoryEngine(), - getContext(), - getUserContext(), - d_private->getResourceManager())); + d_propEngine.reset(new PropEngine( + getTheoryEngine(), getContext(), getUserContext(), getResourceManager())); d_theoryEngine->setPropEngine(getPropEngine()); } @@ -3539,28 +3583,33 @@ void SmtEngine::interrupt() } void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) { - d_private->getResourceManager()->setResourceLimit(units, cumulative); + d_resourceManager->setResourceLimit(units, cumulative); } void SmtEngine::setTimeLimit(unsigned long milis, bool cumulative) { - d_private->getResourceManager()->setTimeLimit(milis, cumulative); + d_resourceManager->setTimeLimit(milis, cumulative); } unsigned long SmtEngine::getResourceUsage() const { - return d_private->getResourceManager()->getResourceUsage(); + return d_resourceManager->getResourceUsage(); } unsigned long SmtEngine::getTimeUsage() const { - return d_private->getResourceManager()->getTimeUsage(); + return d_resourceManager->getTimeUsage(); } unsigned long SmtEngine::getResourceRemaining() const { - return d_private->getResourceManager()->getResourceRemaining(); + return d_resourceManager->getResourceRemaining(); } unsigned long SmtEngine::getTimeRemaining() const { - return d_private->getResourceManager()->getTimeRemaining(); + return d_resourceManager->getTimeRemaining(); +} + +NodeManager* SmtEngine::getNodeManager() const +{ + return d_exprManager->getNodeManager(); } Statistics SmtEngine::getStatistics() const @@ -3654,8 +3703,7 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) } string optionarg = value.getValue(); - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - nodeManagerOptions.setOption(key, optionarg); + d_options.setOption(key, optionarg); } void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } @@ -3714,8 +3762,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const return SExpr(result); } - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - return SExpr::parseAtom(nodeManagerOptions.getOption(key)); + return SExpr::parseAtom(d_options.getOption(key)); } bool SmtEngine::getExpressionName(Expr e, std::string& name) const { @@ -3727,6 +3774,15 @@ void SmtEngine::setExpressionName(Expr e, const std::string& name) { d_private->setExpressionName(e,name); } +Options& SmtEngine::getOptions() { return d_options; } + +const Options& SmtEngine::getOptions() const { return d_options; } + +ResourceManager* SmtEngine::getResourceManager() +{ + return d_resourceManager.get(); +} + void SmtEngine::setSygusConjectureStale() { if (d_private->d_sygusConjectureStale) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index afb39b41b..8db8eadd5 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -171,8 +171,12 @@ class CVC4_PUBLIC SmtEngine SMT_MODE_INTERPOL }; - /** Construct an SmtEngine with the given expression manager. */ - SmtEngine(ExprManager* em); + /** + * Construct an SmtEngine with the given expression manager. + * If provided, optr is a pointer to a set of options that should initialize the values + * of the options object owned by this class. + */ + SmtEngine(ExprManager* em, Options* optr = nullptr); /** Destruct the SMT engine. */ ~SmtEngine(); @@ -248,8 +252,15 @@ class CVC4_PUBLIC SmtEngine /** Is this an internal subsolver? */ bool isInternalSubsolver() const; - /** set the input name */ - void setFilename(std::string filename); + /** + * Notify that we are now parsing the input with the given filename. + * This call sets the filename maintained by this SmtEngine for bookkeeping + * and also makes a copy of the current options of this SmtEngine. This + * is required so that the SMT-LIB command (reset) returns the SmtEngine + * to a state where its options were prior to parsing but after e.g. + * reading command line options. + */ + void notifyStartParsing(std::string filename); /** return the input name (if any) */ std::string getFilename() const; @@ -826,6 +837,9 @@ class CVC4_PUBLIC SmtEngine /** Permit access to the underlying ExprManager. */ ExprManager* getExprManager() const { return d_exprManager; } + /** Permit access to the underlying NodeManager. */ + NodeManager* getNodeManager() const; + /** Export statistics from this SmtEngine. */ Statistics getStatistics() const; @@ -878,6 +892,12 @@ class CVC4_PUBLIC SmtEngine */ void setExpressionName(Expr e, const std::string& name); + /** Get the options object (const and non-const versions) */ + Options& getOptions(); + const Options& getOptions() const; + + /** Get the resource manager of this SMT engine */ + ResourceManager* getResourceManager(); /* ....................................................................... */ private: /* ....................................................................... */ @@ -1321,6 +1341,18 @@ class CVC4_PUBLIC SmtEngine std::unique_ptr<smt::SmtEngineStatistics> d_stats; + /** The options object */ + Options d_options; + /** + * Manager for limiting time and abstract resource usage. + */ + std::unique_ptr<ResourceManager> d_resourceManager; + /** + * The global scope object. Upon creation of this SmtEngine, it becomes the + * SmtEngine in scope. It says the SmtEngine in scope until it is destructed, + * or another SmtEngine is created. + */ + std::unique_ptr<smt::SmtScope> d_scope; /*---------------------------- sygus commands ---------------------------*/ /** diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 7c438073a..1e9c91767 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -46,9 +46,16 @@ ProofManager* currentProofManager() { #endif /* IS_PROOFS_BUILD */ } +ResourceManager* currentResourceManager() +{ + return s_smtEngine_current->getResourceManager(); +} + SmtScope::SmtScope(const SmtEngine* smt) : NodeManagerScope(smt->d_nodeManager), - d_oldSmtEngine(s_smtEngine_current) { + d_oldSmtEngine(s_smtEngine_current), + d_optionsScope(smt ? &const_cast<SmtEngine*>(smt)->getOptions() : nullptr) +{ Assert(smt != NULL); s_smtEngine_current = const_cast<SmtEngine*>(smt); Debug("current") << "smt scope: " << s_smtEngine_current << std::endl; diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index 012c2ec31..5cccde9b8 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -22,6 +22,8 @@ #include "expr/node_manager.h" +#include "options/options.h" + namespace CVC4 { class ProofManager; @@ -36,20 +38,25 @@ bool smtEngineInScope(); // FIXME: Maybe move into SmtScope? ProofManager* currentProofManager(); -class SmtScope : public NodeManagerScope { - /** The old NodeManager, to be restored on destruction. */ - SmtEngine* d_oldSmtEngine; - -public: - SmtScope(const SmtEngine* smt); - ~SmtScope(); +/** get the current resource manager */ +ResourceManager* currentResourceManager(); - /** - * This returns the StatisticsRegistry attached to the currently in scope - * SmtEngine. - */ - static StatisticsRegistry* currentStatisticsRegistry(); +class SmtScope : public NodeManagerScope +{ + public: + SmtScope(const SmtEngine* smt); + ~SmtScope(); + /** + * This returns the StatisticsRegistry attached to the currently in scope + * SmtEngine. + */ + static StatisticsRegistry* currentStatisticsRegistry(); + private: + /** The old SmtEngine, to be restored on destruction. */ + SmtEngine* d_oldSmtEngine; + /** Options scope */ + Options::OptionsScope d_optionsScope; };/* class SmtScope */ diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index 82921b3a0..defc66b74 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -27,12 +27,12 @@ #include "proof/bitvector_proof.h" #include "prop/bv_sat_solver_notify.h" #include "prop/sat_solver_types.h" +#include "smt/smt_engine_scope.h" #include "theory/bv/bitblast/bitblast_strategies_template.h" #include "theory/theory_registrar.h" #include "theory/valuation.h" #include "util/resource_manager.h" - namespace CVC4 { namespace theory { namespace bv { @@ -111,7 +111,7 @@ class MinisatEmptyNotify : public prop::BVSatSolverNotify void notify(prop::SatClause& clause) override {} void spendResource(ResourceManager::Resource r) override { - NodeManager::currentResourceManager()->spendResource(r); + smt::currentResourceManager()->spendResource(r); } void safePoint(ResourceManager::Resource r) override {} diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index ef583cc13..4acd1d2f8 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -67,7 +67,7 @@ EagerBitblaster::EagerBitblaster(TheoryBV* theory_bv, context::Context* c) default: Unreachable() << "Unknown SAT solver type"; } d_satSolver.reset(solver); - ResourceManager* rm = NodeManager::currentResourceManager(); + ResourceManager* rm = smt::currentResourceManager(); d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), d_bitblastingRegistrar.get(), d_nullContext.get(), diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 9abeee65e..c3a305952 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -79,7 +79,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, d_satSolver.reset( prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name)); - ResourceManager* rm = NodeManager::currentResourceManager(); + ResourceManager* rm = smt::currentResourceManager(); d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), @@ -581,7 +581,7 @@ void TLazyBitblaster::clearSolver() { // recreate sat solver d_satSolver.reset( prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry())); - ResourceManager* rm = NodeManager::currentResourceManager(); + ResourceManager* rm = smt::currentResourceManager(); d_cnfStream.reset(new prop::TseitinCnfStream( d_satSolver.get(), d_nullRegistrar.get(), d_nullContext.get(), rm)); d_satSolverNotify.reset( diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index fc3474df4..cabd78643 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -129,26 +129,14 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // verify it if applicable if (options::sygusRewSynthCheck()) { - NodeManager* nm = NodeManager::currentNM(); - Node crr = solbr.eqNode(eq_solr).negate(); Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl; // Notice we don't set produce-models. rrChecker takes the same // options as the SmtEngine we belong to, where we ensure that // produce-models is set. - bool needExport = false; - - // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - // This is only temporarily until we have separate options for each - // SmtEngine instance. We should reuse the same ExprManager with - // a different SmtEngine (and different options) here, eventually. - // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - api::Solver slv(&nm->getOptions()); - ExprManager* em = slv.getExprManager(); - SmtEngine* rrChecker = slv.getSmtEngine(); - ExprManagerMapCollection varMap; - initializeChecker(rrChecker, em, varMap, crr, needExport); + std::unique_ptr<SmtEngine> rrChecker; + initializeChecker(rrChecker, crr); Result r = rrChecker->checkSat(); Trace("rr-check") << "...result : " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::SAT) @@ -181,16 +169,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, if (val.isNull()) { Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE); - if (needExport) - { - Expr erefv = refv.toExpr().exportTo(em, varMap); - val = Node::fromExpr(rrChecker->getValue(erefv).exportTo( - nm->toExprManager(), varMap)); - } - else - { - val = Node::fromExpr(rrChecker->getValue(refv.toExpr())); - } + val = Node::fromExpr(rrChecker->getValue(refv.toExpr())); } Trace("rr-check") << " " << v << " -> " << val << std::endl; pt.push_back(val); diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index b209fc6ff..6153242e7 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -69,32 +69,16 @@ Node ExprMiner::convertToSkolem(Node n) return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end()); } -void ExprMiner::initializeChecker(SmtEngine* checker, - ExprManager* em, - ExprManagerMapCollection& varMap, - Node query, - bool& needExport) +void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, + Node query) { // Convert bound variables to skolems. This ensures the satisfiability // check is ground. Node squery = convertToSkolem(query); - if (options::sygusExprMinerCheckUseExport()) - { - initializeSubsolverWithExport(checker, - em, - varMap, - squery.toExpr(), - true, - options::sygusExprMinerCheckTimeout()); - checker->setOption("sygus-rr-synth-input", false); - checker->setOption("input-language", "smt2"); - needExport = true; - } - else - { - initializeSubsolver(checker, squery.toExpr()); - needExport = false; - } + initializeSubsolver(checker, squery.toExpr()); + // also set the options + checker->setOption("sygus-rr-synth-input", false); + checker->setOption("input-language", "smt2"); } Result ExprMiner::doCheck(Node query) @@ -111,18 +95,8 @@ Result ExprMiner::doCheck(Node query) return Result(Result::SAT); } } - // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - // This is only temporarily until we have separate options for each - // SmtEngine instance. We should reuse the same ExprManager with - // a different SmtEngine (and different options) here, eventually. - // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - NodeManager* nm = NodeManager::currentNM(); - bool needExport = false; - api::Solver slv(&nm->getOptions()); - ExprManager* em = slv.getExprManager(); - SmtEngine* smte = slv.getSmtEngine(); - ExprManagerMapCollection varMap; - initializeChecker(smte, em, varMap, queryr, needExport); + std::unique_ptr<SmtEngine> smte; + initializeChecker(smte, query); return smte->checkSat(); } diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index eebcebf88..e603075c4 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -78,22 +78,8 @@ class ExprMiner * This function initializes the smt engine smte to check the satisfiability * of the argument "query", which is a formula whose free variables (of * kind BOUND_VARIABLE) are a subset of d_vars. - * - * The arguments em and varMap are used for supporting cases where we - * want smte to use a different expression manager instead of the current - * expression manager. The motivation for this so that different options can - * be set for the subcall. - * - * We update the flag needExport to true if smte is using the expression - * manager em. In this case, subsequent expressions extracted from smte - * (for instance, model values) must be exported to the current expression - * manager. */ - void initializeChecker(SmtEngine* smte, - ExprManager* em, - ExprManagerMapCollection& varMap, - Node query, - bool& needExport); + void initializeChecker(std::unique_ptr<SmtEngine>& smte, Node query); /** * Run the satisfiability check on query and return the result * (sat/unsat/unknown). diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 4cf65b24a..39d27373d 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -157,20 +157,9 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) if (options::sygusQueryGenCheck()) { Trace("sygus-qgen-check") << " query: check " << qy << "..." << std::endl; - NodeManager* nm = NodeManager::currentNM(); // make the satisfiability query - // - // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - // This is only temporarily until we have separate options for each - // SmtEngine instance. We should reuse the same ExprManager with - // a different SmtEngine (and different options) here, eventually. - // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - bool needExport = false; - api::Solver slv(&nm->getOptions()); - ExprManager* em = slv.getExprManager(); - SmtEngine* queryChecker = slv.getSmtEngine(); - ExprManagerMapCollection varMap; - initializeChecker(queryChecker, em, varMap, qy, needExport); + std::unique_ptr<SmtEngine> queryChecker; + initializeChecker(queryChecker, qy); Result r = queryChecker->checkSat(); Trace("sygus-qgen-check") << " query: ...got : " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index e98b875fd..d4637a636 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -88,10 +88,10 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out) } else { - Options& nodeManagerOptions = nm->getOptions(); - std::ostream* nodeManagerOut = nodeManagerOptions.getOut(); - (*nodeManagerOut) << "; (filtered " << (d_isStrong ? s : s.negate()) - << ")" << std::endl; + Options& opts = smt::currentSmtEngine()->getOptions(); + std::ostream* smtOut = opts.getOut(); + (*smtOut) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")" + << std::endl; } } d_curr_sols.clear(); diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index df21a06eb..d0cac6d58 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/smt_engine_subsolver.h" using namespace CVC4::kind; @@ -374,10 +375,9 @@ bool CegSingleInv::solve() siq = nm->mkNode(FORALL, siq[0], siq[1], n_attr); } // solve the single invocation conjecture using a fresh copy of SMT engine - SmtEngine siSmt(nm->toExprManager()); - siSmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); - siSmt.assertFormula(siq.toExpr()); - Result r = siSmt.checkSat(); + std::unique_ptr<SmtEngine> siSmt; + initializeSubsolver(siSmt, siq); + Result r = siSmt->checkSat(); Trace("sygus-si") << "Result: " << r << std::endl; if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) { @@ -386,7 +386,7 @@ bool CegSingleInv::solve() } // now, get the instantiations std::vector<Expr> qs; - siSmt.getInstantiatedQuantifiedFormulas(qs); + siSmt->getInstantiatedQuantifiedFormulas(qs); Assert(qs.size() <= 1); // track the instantiations, as solution construction is based on this Trace("sygus-si") << "#instantiated quantified formulas=" << qs.size() @@ -398,7 +398,7 @@ bool CegSingleInv::solve() TNode qn = Node::fromExpr(q); Assert(qn.getKind() == FORALL); std::vector<std::vector<Expr> > tvecs; - siSmt.getInstantiationTermVectors(q, tvecs); + siSmt->getInstantiationTermVectors(q, tvecs); Trace("sygus-si") << "#instantiations of " << q << "=" << tvecs.size() << std::endl; std::vector<Node> vars; diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 5784e42c0..de75af083 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -735,9 +735,8 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, { addSuccess = false; // try a new core - std::unique_ptr<SmtEngine> checkSol( - new SmtEngine(NodeManager::currentNM()->toExprManager())); - initializeSubsolver(checkSol.get()); + std::unique_ptr<SmtEngine> checkSol; + initializeSubsolver(checkSol); Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; std::vector<Node> rasserts = asserts; rasserts.push_back(d_sc); @@ -776,9 +775,8 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, { // In terms of Variant #2, this is the check "if S ^ U is unsat" Trace("sygus-ccore") << "----- Check side condition" << std::endl; - std::unique_ptr<SmtEngine> checkSc( - new SmtEngine(NodeManager::currentNM()->toExprManager())); - initializeSubsolver(checkSc.get()); + std::unique_ptr<SmtEngine> checkSc; + initializeSubsolver(checkSc); std::vector<Node> scasserts; scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end()); scasserts.push_back(d_sc); diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index d34903805..e411dcf2f 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -177,7 +177,6 @@ bool SygusRepairConst::repairSolution(Node sygusBody, return false; } - NodeManager* nm = NodeManager::currentNM(); Trace("sygus-repair-const") << "Get first-order query..." << std::endl; Node fo_body = getFoQuery(sygusBody, candidates, candidate_skeletons, sk_vars); @@ -229,48 +228,17 @@ bool SygusRepairConst::repairSolution(Node sygusBody, Trace("sygus-engine") << "Repairing previous solution..." << std::endl; // make the satisfiability query - // - // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - // This is only temporarily until we have separate options for each - // SmtEngine instance. We should reuse the same ExprManager with - // a different SmtEngine (and different options) here, eventually. - // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - bool needExport = true; - std::unique_ptr<SmtEngine> simpleSmte; - std::unique_ptr<api::Solver> slv; - ExprManager* em = nullptr; - SmtEngine* repcChecker = nullptr; - ExprManagerMapCollection varMap; - - if (options::sygusRepairConstTimeout.wasSetByUser()) - { - // To support a separate timeout for the subsolver, we need to create - // a separate ExprManager with its own options. This requires that - // the expressions sent to the subsolver can be exported from on - // ExprManager to another. - slv.reset(new api::Solver(&nm->getOptions())); - em = slv->getExprManager(); - repcChecker = slv->getSmtEngine(); - initializeSubsolverWithExport(repcChecker, - em, - varMap, - fo_body.toExpr(), - true, - options::sygusRepairConstTimeout()); - // renable options disabled by sygus - repcChecker->setOption("miniscope-quant", true); - repcChecker->setOption("miniscope-quant-fv", true); - repcChecker->setOption("quant-split", true); - } - else - { - needExport = false; - em = nm->toExprManager(); - simpleSmte.reset(new SmtEngine(em)); - repcChecker = simpleSmte.get(); - initializeSubsolver(repcChecker, fo_body.toExpr()); - } - + std::unique_ptr<SmtEngine> repcChecker; + // initialize the subsolver using the standard method + initializeSubsolver(repcChecker, + fo_body.toExpr(), + options::sygusRepairConstTimeout.wasSetByUser(), + options::sygusRepairConstTimeout()); + // renable options disabled by sygus + repcChecker->setOption("miniscope-quant", true); + repcChecker->setOption("miniscope-quant-fv", true); + repcChecker->setOption("quant-split", true); + // check satisfiability Result r = repcChecker->checkSat(); Trace("sygus-repair-const") << "...got : " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::UNSAT @@ -284,17 +252,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, { Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end()); Node fov = d_sk_to_fo[v]; - Node fov_m; - if (needExport) - { - Expr e_fov = fov.toExpr().exportTo(em, varMap); - fov_m = Node::fromExpr( - repcChecker->getValue(e_fov).exportTo(nm->toExprManager(), varMap)); - } - else - { - fov_m = Node::fromExpr(repcChecker->getValue(fov.toExpr())); - } + Node fov_m = Node::fromExpr(repcChecker->getValue(fov.toExpr())); Trace("sygus-repair-const") << " " << fov << " = " << fov_m << std::endl; // convert to sygus Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 7e6e74209..a28e76d90 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -20,6 +20,7 @@ #include "options/quantifiers_options.h" #include "printer/printer.h" #include "prop/prop_engine.h" +#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/first_order_model.h" @@ -1003,8 +1004,8 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums, // we have generated a solution, print it // get the current output stream // this output stream should coincide with wherever --dump-synth is output on - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - printSynthSolution(*nodeManagerOptions.getOut()); + Options& sopts = smt::currentSmtEngine()->getOptions(); + printSynthSolution(*sopts.getOut()); excludeCurrentSolution(enums, values); } diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 590fdaa56..f8349c834 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -169,9 +169,8 @@ void SynthEngine::assignConjecture(Node q) if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation()) { // create new smt engine to do quantifier elimination - std::unique_ptr<SmtEngine> smt_qe( - new SmtEngine(NodeManager::currentNM()->toExprManager())); - initializeSubsolver(smt_qe.get()); + std::unique_ptr<SmtEngine> smt_qe; + initializeSubsolver(smt_qe); Trace("cegqi-qep") << "Property is non-ground single invocation, run " "QE to obtain single invocation." << std::endl; diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 7ad2c54eb..7773b05d5 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -19,6 +19,8 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "theory/quantifiers/lazy_trie.h" #include "util/bitvector.h" #include "util/random.h" @@ -820,8 +822,8 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr) return; } // we have detected unsoundness in the rewriter - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - std::ostream* out = nodeManagerOptions.getOut(); + Options& sopts = smt::currentSmtEngine()->getOptions(); + std::ostream* out = sopts.getOut(); (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl; // debugging information (*out) << "Terms are not equivalent for : " << std::endl; diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 07bc695ec..0247a7277 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -162,7 +162,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) { ResourceManager* rm = NULL; bool hasSmtEngine = smt::smtEngineInScope(); if (hasSmtEngine) { - rm = NodeManager::currentResourceManager(); + rm = smt::currentResourceManager(); } // Rewrite until the stack is empty for (;;){ diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp index f529d3fea..45c115524 100644 --- a/src/theory/smt_engine_subsolver.cpp +++ b/src/theory/smt_engine_subsolver.cpp @@ -41,52 +41,32 @@ Result quickCheck(Node& query) return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK); } -void initializeSubsolver(SmtEngine* smte) +void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, + Node query, + bool needsTimeout, + unsigned long timeout) { + NodeManager* nm = NodeManager::currentNM(); + SmtEngine* smtCurr = smt::currentSmtEngine(); + // must copy the options + smte.reset(new SmtEngine(nm->toExprManager(), &smtCurr->getOptions())); smte->setIsInternalSubsolver(); - smte->setLogic(smt::currentSmtEngine()->getLogicInfo()); -} - -void initializeSubsolverWithExport(SmtEngine* smte, - ExprManager* em, - ExprManagerMapCollection& varMap, - Node query, - bool needsTimeout, - unsigned long timeout) -{ - // To support a separate timeout for the subsolver, we need to use - // a separate ExprManager with its own options. This requires that - // the expressions sent to the subsolver can be exported from on - // ExprManager to another. If the export fails, we throw an - // OptionException. - try + smte->setLogic(smtCurr->getLogicInfo()); + if (needsTimeout) { - smte->setIsInternalSubsolver(); - if (needsTimeout) - { - smte->setTimeLimit(timeout, true); - } - smte->setLogic(smt::currentSmtEngine()->getLogicInfo()); - Expr equery = query.toExpr().exportTo(em, varMap); - smte->assertFormula(equery); + smte->setTimeLimit(timeout, true); } - catch (const CVC4::ExportUnsupportedException& e) + smte->setLogic(smt::currentSmtEngine()->getLogicInfo()); + if (!query.isNull()) { - std::stringstream msg; - msg << "Unable to export " << query - << " but exporting expressions is " - "required for a subsolver."; - throw OptionException(msg.str()); + smte->assertFormula(query.toExpr()); } } -void initializeSubsolver(SmtEngine* smte, Node query) -{ - initializeSubsolver(smte); - smte->assertFormula(query.toExpr()); -} - -Result checkWithSubsolver(SmtEngine* smte, Node query) +Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, + Node query, + bool needsTimeout, + unsigned long timeout) { Assert(query.getType().isBoolean()); Result r = quickCheck(query); @@ -94,7 +74,7 @@ Result checkWithSubsolver(SmtEngine* smte, Node query) { return r; } - initializeSubsolver(smte, query); + initializeSubsolver(smte, query, needsTimeout, timeout); return smte->checkSat(); } @@ -128,50 +108,14 @@ Result checkWithSubsolver(Node query, } return r; } - - // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - // This is only temporarily until we have separate options for each - // SmtEngine instance. We should reuse the same ExprManager with - // a different SmtEngine (and different options) here, eventually. - // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! - std::unique_ptr<SmtEngine> simpleSmte; - std::unique_ptr<api::Solver> slv; - ExprManager* em = nullptr; - SmtEngine* smte = nullptr; - ExprManagerMapCollection varMap; - NodeManager* nm = NodeManager::currentNM(); - bool needsExport = false; - if (needsTimeout) - { - slv.reset(new api::Solver(&nm->getOptions())); - em = slv->getExprManager(); - smte = slv->getSmtEngine(); - needsExport = true; - initializeSubsolverWithExport( - smte, em, varMap, query, needsTimeout, timeout); - } - else - { - em = nm->toExprManager(); - simpleSmte.reset(new SmtEngine(em)); - smte = simpleSmte.get(); - initializeSubsolver(smte, query); - } + std::unique_ptr<SmtEngine> smte; + initializeSubsolver(smte, query, needsTimeout, timeout); r = smte->checkSat(); if (r.asSatisfiabilityResult().isSat() == Result::SAT) { for (const Node& v : vars) { - Expr val; - if (needsExport) - { - Expr ev = v.toExpr().exportTo(em, varMap); - val = smte->getValue(ev).exportTo(nm->toExprManager(), varMap); - } - else - { - val = smte->getValue(v.toExpr()); - } + Expr val = smte->getValue(v.toExpr()); modelVals.push_back(Node::fromExpr(val)); } } diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h index b606657bb..64646ac05 100644 --- a/src/theory/smt_engine_subsolver.h +++ b/src/theory/smt_engine_subsolver.h @@ -31,49 +31,18 @@ namespace CVC4 { namespace theory { /** - * This function initializes the smt engine smte as a subsolver, e.g. it - * creates a new SMT engine and sets the options of the current SMT engine. - */ -void initializeSubsolver(SmtEngine* smte); - -/** - * Initialize Smt subsolver with exporting - * * This function initializes the smt engine smte to check the satisfiability * of the argument "query". * - * The arguments em and varMap are used for supporting cases where we - * want smte to use a different expression manager instead of the current - * expression manager. The motivation for this so that different options can - * be set for the subcall. - * - * Notice that subsequent expressions extracted from smte (for instance, model - * values) must be exported to the current expression - * manager. - * * @param smte The smt engine pointer to initialize - * @param em Reference to the expression manager used by smte - * @param varMap Map used for exporting expressions - * @param query The query to check + * @param query The query to check (if provided) * @param needsTimeout Whether we would like to set a timeout * @param timeout The timeout (in milliseconds) */ -void initializeSubsolverWithExport(SmtEngine* smte, - ExprManager* em, - ExprManagerMapCollection& varMap, - Node query, - bool needsTimeout = false, - unsigned long timeout = 0); - -/** - * This function initializes the smt engine smte to check the satisfiability - * of the argument "query", without exporting expressions. - * - * Notice that is not possible to set a timeout value currently without - * exporting since the Options and ExprManager are tied together. - * TODO: eliminate this dependency (cvc4-projects #120). - */ -void initializeSubsolver(SmtEngine* smte, Node query); +void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, + Node query = Node::null(), + bool needsTimeout = false, + unsigned long timeout = 0); /** * This returns the result of checking the satisfiability of formula query. @@ -81,7 +50,10 @@ void initializeSubsolver(SmtEngine* smte, Node query); * If necessary, smte is initialized to the SMT engine that checked its * satisfiability. */ -Result checkWithSubsolver(SmtEngine* smte, Node query); +Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, + Node query, + bool needsTimeout = false, + unsigned long timeout = 0); /** * This returns the result of checking the satisfiability of formula query. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2472ae023..0b84893ae 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -173,6 +173,7 @@ void TheoryEngine::eqNotifyNewClass(TNode t){ TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, + ResourceManager* rm, RemoveTermFormulas& iteRemover, const LogicInfo& logicInfo) : d_propEngine(nullptr), @@ -205,7 +206,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_true(), d_false(), d_interrupted(false), - d_resourceManager(NodeManager::currentResourceManager()), + d_resourceManager(rm), d_inPreregister(false), d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index f2274b3da..c29ba1b4d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -363,6 +363,7 @@ class TheoryEngine { /** Constructs a theory engine */ TheoryEngine(context::Context* context, context::UserContext* userContext, + ResourceManager* rm, RemoveTermFormulas& iteRemover, const LogicInfo& logic); diff --git a/test/regress/regress1/sygus/issue4009-qep.smt2 b/test/regress/regress1/sygus/issue4009-qep.smt2 index 6f17a0c04..cc79954c4 100644 --- a/test/regress/regress1/sygus/issue4009-qep.smt2 +++ b/test/regress/regress1/sygus/issue4009-qep.smt2 @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-inference --sygus-qe-preproc +; COMMAND-LINE: --sygus-inference --sygus-qe-preproc --no-check-unsat-cores (set-logic ALL) (declare-fun a () Real) (declare-fun b () Real) diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp index 592144eaa..340326e40 100644 --- a/test/system/smt2_compliance.cpp +++ b/test/system/smt2_compliance.cpp @@ -61,8 +61,7 @@ int main() void testGetInfo(api::Solver* solver, const char* s) { - ParserBuilder pb( - solver, "<internal>", solver->getExprManager()->getOptions()); + ParserBuilder pb(solver, "<internal>", solver->getOptions()); Parser* p = pb.withStringInput(string("(get-info ") + s + ")").build(); assert(p != NULL); Command* c = p->nextCommand(); diff --git a/test/unit/api/grammar_black.h b/test/unit/api/grammar_black.h index f30f6b0ad..eee067ef2 100644 --- a/test/unit/api/grammar_black.h +++ b/test/unit/api/grammar_black.h @@ -37,7 +37,7 @@ class GrammarBlack : public CxxTest::TestSuite void GrammarBlack::setUp() { d_solver.reset(new Solver()); } -void GrammarBlack::tearDown() {} +void GrammarBlack::tearDown() { d_solver.reset(nullptr); } void GrammarBlack::testAddRule() { diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h index cbfc9cf23..f9f37a019 100644 --- a/test/unit/api/result_black.h +++ b/test/unit/api/result_black.h @@ -22,7 +22,7 @@ class ResultBlack : public CxxTest::TestSuite { public: void setUp() { d_solver.reset(new Solver()); } - void tearDown() override {} + void tearDown() override { d_solver.reset(nullptr); } void testIsNull(); void testEq(); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 4a7b74c8e..d10813f58 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -167,7 +167,7 @@ class SolverBlack : public CxxTest::TestSuite void SolverBlack::setUp() { d_solver.reset(new Solver()); } -void SolverBlack::tearDown() {} +void SolverBlack::tearDown() { d_solver.reset(nullptr); } void SolverBlack::testGetBooleanSort() { diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 1b8a7c92f..91242322a 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -22,6 +22,8 @@ #include <string> #include <vector> +#include "api/cvc4cpp.h" +#include "smt/smt_engine.h" #include "expr/expr_manager.h" #include "expr/node.h" #include "expr/node_builder.h" @@ -50,15 +52,13 @@ std::vector<Node> makeNSkolemNodes(NodeManager* nodeManager, int N, class NodeBlack : public CxxTest::TestSuite { private: - Options opts; NodeManager* d_nodeManager; - NodeManagerScope* d_scope; - TypeNode* d_booleanType; - TypeNode* d_realType; - + api::Solver* d_slv; public: void setUp() override { + // setup a SMT engine so that options are in scope + Options opts; char* argv[2]; argv[0] = strdup(""); argv[1] = strdup("--output-lang=ast"); @@ -66,18 +66,12 @@ class NodeBlack : public CxxTest::TestSuite { free(argv[0]); free(argv[1]); - d_nodeManager = new NodeManager(NULL, opts); - d_scope = new NodeManagerScope(d_nodeManager); - d_booleanType = new TypeNode(d_nodeManager->booleanType()); - d_realType = new TypeNode(d_nodeManager->realType()); + d_slv = new api::Solver(&opts); + d_nodeManager = d_slv->getSmtEngine()->getNodeManager(); } - void tearDown() override - { - delete d_realType; - delete d_booleanType; - delete d_scope; - delete d_nodeManager; + void tearDown() override { + delete d_slv; } bool imp(bool a, bool b) const { return (!a) || (b); } @@ -114,12 +108,12 @@ class NodeBlack : public CxxTest::TestSuite { void testOperatorEquals() { Node a, b, c; - b = d_nodeManager->mkSkolem("b", *d_booleanType); + b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); a = b; c = a; - Node d = d_nodeManager->mkSkolem("d", *d_booleanType); + Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); TS_ASSERT(a == a); TS_ASSERT(a == b); @@ -148,12 +142,12 @@ class NodeBlack : public CxxTest::TestSuite { void testOperatorNotEquals() { Node a, b, c; - b = d_nodeManager->mkSkolem("b", *d_booleanType); + b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); a = b; c = a; - Node d = d_nodeManager->mkSkolem("d", *d_booleanType); + Node d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); /*structed assuming operator == works */ TS_ASSERT(iff(a != a, !(a == a))); @@ -208,7 +202,7 @@ class NodeBlack : public CxxTest::TestSuite { void testOperatorAssign() { Node a, b; Node c = d_nodeManager->mkNode( - NOT, d_nodeManager->mkSkolem("c", *d_booleanType)); + NOT, d_nodeManager->mkSkolem("c", d_nodeManager->booleanType())); b = c; TS_ASSERT(b == c); @@ -324,8 +318,8 @@ class NodeBlack : public CxxTest::TestSuite { void testIteNode() { /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/ - Node a = d_nodeManager->mkSkolem("a", *d_booleanType); - Node b = d_nodeManager->mkSkolem("b", *d_booleanType); + Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); + Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); Node cnd = d_nodeManager->mkNode(OR, a, b); Node thenBranch = d_nodeManager->mkConst(true); @@ -383,8 +377,8 @@ class NodeBlack : public CxxTest::TestSuite { void testGetKind() { /*inline Kind getKind() const; */ - Node a = d_nodeManager->mkSkolem("a", *d_booleanType); - Node b = d_nodeManager->mkSkolem("b", *d_booleanType); + Node a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); + Node b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); Node n = d_nodeManager->mkNode(NOT, a); TS_ASSERT(NOT == n.getKind()); @@ -392,8 +386,8 @@ class NodeBlack : public CxxTest::TestSuite { n = d_nodeManager->mkNode(EQUAL, a, b); TS_ASSERT(EQUAL == n.getKind()); - Node x = d_nodeManager->mkSkolem("x", *d_realType); - Node y = d_nodeManager->mkSkolem("y", *d_realType); + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->realType()); + Node y = d_nodeManager->mkSkolem("y", d_nodeManager->realType()); n = d_nodeManager->mkNode(PLUS, x, y); TS_ASSERT(PLUS == n.getKind()); @@ -470,9 +464,9 @@ class NodeBlack : public CxxTest::TestSuite { // test iterators void testIterator() { NodeBuilder<> b; - Node x = d_nodeManager->mkSkolem("x", *d_booleanType); - Node y = d_nodeManager->mkSkolem("y", *d_booleanType); - Node z = d_nodeManager->mkSkolem("z", *d_booleanType); + Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); + Node y = d_nodeManager->mkSkolem("y", d_nodeManager->booleanType()); + Node z = d_nodeManager->mkSkolem("z", d_nodeManager->booleanType()); Node n = b << x << y << z << kind::AND; { // iterator @@ -717,7 +711,7 @@ class NodeBlack : public CxxTest::TestSuite { // This is for demonstrating what a certain type of user error looks like. // Node level0(){ // NodeBuilder<> nb(kind::AND); - // Node x = d_nodeManager->mkSkolem("x", *d_booleanType); + // Node x = d_nodeManager->mkSkolem("x", d_nodeManager->booleanType()); // nb << x; // nb << x; // return Node(nb.constructNode()); diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 9d5a0fc8d..8668f746b 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -209,8 +209,7 @@ class ParserBlack d_solver.reset(new api::Solver(&d_options)); } - void tearDown() { - } + void tearDown() { d_solver.reset(nullptr); } private: InputLanguage d_lang; diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index 4a30b4179..24dd5ae62 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -145,7 +145,7 @@ class CnfStreamWhite : public CxxTest::TestSuite { d_satSolver = new FakeSatSolver(); d_cnfContext = new context::Context(); d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine); - ResourceManager * rm = d_nodeManager->getResourceManager(); + ResourceManager* rm = d_smt->getResourceManager(); d_cnfStream = new CVC4::prop::TseitinCnfStream( d_satSolver, d_cnfRegistrar, d_cnfContext, rm); } diff --git a/test/unit/theory/evaluator_white.h b/test/unit/theory/evaluator_white.h index 3fc95b2a5..0a50bae2d 100644 --- a/test/unit/theory/evaluator_white.h +++ b/test/unit/theory/evaluator_white.h @@ -48,9 +48,9 @@ class TheoryEvaluatorWhite : public CxxTest::TestSuite { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager(opts); + d_em = new ExprManager; d_nm = NodeManager::fromExprManager(d_em); - d_smt = new SmtEngine(d_em); + d_smt = new SmtEngine(d_em, &opts); d_scope = new SmtScope(d_smt); d_smt->finalOptionsAreSet(); } diff --git a/test/unit/theory/sequences_rewriter_white.h b/test/unit/theory/sequences_rewriter_white.h index c9c897f5f..347289693 100644 --- a/test/unit/theory/sequences_rewriter_white.h +++ b/test/unit/theory/sequences_rewriter_white.h @@ -46,8 +46,8 @@ class SequencesRewriterWhite : public CxxTest::TestSuite { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager(opts); - d_smt = new SmtEngine(d_em); + d_em = new ExprManager; + d_smt = new SmtEngine(d_em, &opts); d_scope = new SmtScope(d_smt); d_smt->finalOptionsAreSet(); d_rewriter = new ExtendedRewriter(true); diff --git a/test/unit/theory/theory_bv_rewriter_white.h b/test/unit/theory/theory_bv_rewriter_white.h index d2284aa8f..e6110256a 100644 --- a/test/unit/theory/theory_bv_rewriter_white.h +++ b/test/unit/theory/theory_bv_rewriter_white.h @@ -40,8 +40,8 @@ class TheoryBvRewriterWhite : public CxxTest::TestSuite { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager(opts); - d_smt = new SmtEngine(d_em); + d_em = new ExprManager; + d_smt = new SmtEngine(d_em, &opts); d_scope = new SmtScope(d_smt); d_smt->finalOptionsAreSet(); diff --git a/test/unit/theory/theory_strings_word_white.h b/test/unit/theory/theory_strings_word_white.h index 2e29d50b8..048d1d707 100644 --- a/test/unit/theory/theory_strings_word_white.h +++ b/test/unit/theory/theory_strings_word_white.h @@ -37,8 +37,8 @@ class TheoryStringsWordWhite : public CxxTest::TestSuite { Options opts; opts.setOutputLanguage(language::output::LANG_SMTLIB_V2); - d_em = new ExprManager(opts); - d_smt = new SmtEngine(d_em); + d_em = new ExprManager; + d_smt = new SmtEngine(d_em, &opts); d_scope = new SmtScope(d_smt); d_nm = NodeManager::currentNM(); |