diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-29 15:35:44 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-29 17:35:44 -0500 |
commit | 19054b3b1d427e662d30d4322df2b2f2361353da (patch) | |
tree | 1ee878fd6c2c36b78ea33607a5668e6a6d8f7144 /src/theory/quantifiers | |
parent | 5cd6f0e5e910ad61ebc5045170842078818a3b80 (diff) |
Make ExprManager constructor private (#4669)
This commit makes the ExprManager constructor private and updates the
initialization of subsolvers, unit tests, and system tests accordingly.
This is a step towards making options part of SmtEngine instead of
NodeManager.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/expr_miner.h | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/query_generator.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_core_connective.cpp | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 76 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.h | 20 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 5 |
8 files changed, 86 insertions, 71 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 0454b6412..fc3474df4 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/candidate_rewrite_database.h" +#include "api/cvc4cpp.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -137,8 +138,15 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // options as the SmtEngine we belong to, where we ensure that // produce-models is set. bool needExport = false; - ExprManager em(nm->getOptions()); - std::unique_ptr<SmtEngine> rrChecker; + + // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! + // 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); Result r = rrChecker->checkSat(); @@ -175,7 +183,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE); if (needExport) { - Expr erefv = refv.toExpr().exportTo(&em, varMap); + Expr erefv = refv.toExpr().exportTo(em, varMap); val = Node::fromExpr(rrChecker->getValue(erefv).exportTo( nm->toExprManager(), varMap)); } diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 01a46d84a..b209fc6ff 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/expr_miner.h" +#include "api/cvc4cpp.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -68,8 +69,8 @@ Node ExprMiner::convertToSkolem(Node n) return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end()); } -void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, - ExprManager& em, +void ExprMiner::initializeChecker(SmtEngine* checker, + ExprManager* em, ExprManagerMapCollection& varMap, Node query, bool& needExport) @@ -110,10 +111,16 @@ 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; - ExprManager em(nm->getOptions()); - std::unique_ptr<SmtEngine> smte; + api::Solver slv(&nm->getOptions()); + ExprManager* em = slv.getExprManager(); + SmtEngine* smte = slv.getSmtEngine(); ExprManagerMapCollection varMap; initializeChecker(smte, em, varMap, queryr, needExport); return smte->checkSat(); diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index d69ef45b4..eebcebf88 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -89,8 +89,8 @@ class ExprMiner * (for instance, model values) must be exported to the current expression * manager. */ - void initializeChecker(std::unique_ptr<SmtEngine>& smte, - ExprManager& em, + void initializeChecker(SmtEngine* smte, + ExprManager* em, ExprManagerMapCollection& varMap, Node query, bool& needExport); diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 9f08ebec7..4cf65b24a 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -16,6 +16,8 @@ #include "theory/quantifiers/query_generator.h" #include <fstream> + +#include "api/cvc4cpp.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -157,9 +159,16 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) 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; - ExprManager em(nm->getOptions()); - std::unique_ptr<SmtEngine> queryChecker; + api::Solver slv(&nm->getOptions()); + ExprManager* em = slv.getExprManager(); + SmtEngine* queryChecker = slv.getSmtEngine(); ExprManagerMapCollection varMap; initializeChecker(queryChecker, em, varMap, qy, needExport); Result r = queryChecker->checkSat(); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index de75af083..5784e42c0 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -735,8 +735,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, { addSuccess = false; // try a new core - std::unique_ptr<SmtEngine> checkSol; - initializeSubsolver(checkSol); + std::unique_ptr<SmtEngine> checkSol( + new SmtEngine(NodeManager::currentNM()->toExprManager())); + initializeSubsolver(checkSol.get()); Trace("sygus-ccore") << "----- Check candidate " << an << std::endl; std::vector<Node> rasserts = asserts; rasserts.push_back(d_sc); @@ -775,8 +776,9 @@ 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; - initializeSubsolver(checkSc); + std::unique_ptr<SmtEngine> checkSc( + new SmtEngine(NodeManager::currentNM()->toExprManager())); + initializeSubsolver(checkSc.get()); 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 1c34bd73a..d34903805 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/sygus_repair_const.h" +#include "api/cvc4cpp.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -100,36 +101,6 @@ bool SygusRepairConst::isActive() const return !d_base_inst.isNull() && d_allow_constant_grammar; } -void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker, - ExprManager& em, - ExprManagerMapCollection& varMap, - Node query, - bool& needExport) -{ - 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. - initializeSubsolverWithExport(checker, - em, - varMap, - query.toExpr(), - true, - options::sygusRepairConstTimeout()); - // renable options disabled by sygus - checker->setOption("miniscope-quant", true); - checker->setOption("miniscope-quant-fv", true); - checker->setOption("quant-split", true); - } - else - { - needExport = false; - initializeSubsolver(checker, query.toExpr()); - } -} - bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates, const std::vector<Node>& candidate_values, std::vector<Node>& repair_cv, @@ -258,11 +229,48 @@ 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; - ExprManager em(nm->getOptions()); - std::unique_ptr<SmtEngine> repcChecker; - initializeChecker(repcChecker, em, varMap, fo_body, needExport); + + 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()); + } + Result r = repcChecker->checkSat(); Trace("sygus-repair-const") << "...got : " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::UNSAT @@ -279,7 +287,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody, Node fov_m; if (needExport) { - Expr e_fov = fov.toExpr().exportTo(&em, varMap); + Expr e_fov = fov.toExpr().exportTo(em, varMap); fov_m = Node::fromExpr( repcChecker->getValue(e_fov).exportTo(nm->toExprManager(), varMap)); } diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index dc721b42d..e02ca1f3e 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -209,26 +209,6 @@ class SygusRepairConst * If n is in the given logic, this method returns true. */ bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar); - /** initialize checker - * - * This function initializes the smt engine checker to check the - * satisfiability of the argument "query" - * - * The arguments em and varMap are used for supporting cases where we - * want checker 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 checker 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(std::unique_ptr<SmtEngine>& checker, - ExprManager& em, - ExprManagerMapCollection& varMap, - Node query, - bool& needExport); }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index f8349c834..590fdaa56 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -169,8 +169,9 @@ void SynthEngine::assignConjecture(Node q) if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation()) { // create new smt engine to do quantifier elimination - std::unique_ptr<SmtEngine> smt_qe; - initializeSubsolver(smt_qe); + std::unique_ptr<SmtEngine> smt_qe( + new SmtEngine(NodeManager::currentNM()->toExprManager())); + initializeSubsolver(smt_qe.get()); Trace("cegqi-qep") << "Property is non-ground single invocation, run " "QE to obtain single invocation." << std::endl; |