diff options
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(); |