From 6b673474218c300576cae43388b513c7fc8448f8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 7 Jul 2020 18:18:54 -0500 Subject: Transfer ownership of internal Options from NodeManager to SmtEngine (#4682) This PR decouples Options from NodeManager. Instead, options now live in SmtEngine. The changes that were required for this PR include: The main internal options object is now owned by SmtEngine instead of ExprManager. The ownership resource manager is moved from NodeManager to SmtEngine. Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit. A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created. The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore. Resource manager was removed from the smt2 parser. Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset. Updates to unit tests to ensure conformance to new options scoping. --- src/theory/quantifiers/expr_miner.cpp | 42 +++++++---------------------------- 1 file changed, 8 insertions(+), 34 deletions(-) (limited to 'src/theory/quantifiers/expr_miner.cpp') 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& 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 smte; + initializeChecker(smte, query); return smte->checkSat(); } -- cgit v1.2.3