From 3115a76e3675ab1da3f111f33688b2ed2c5f8b53 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 31 Aug 2018 18:10:57 -0500 Subject: [PATCH] Allows SAT checks of repair const to have different options (#2412) --- src/options/quantifiers_options.toml | 7 + .../quantifiers/sygus/sygus_repair_const.cpp | 149 +++++++++++------- .../quantifiers/sygus/sygus_repair_const.h | 20 +++ 3 files changed, 123 insertions(+), 53 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 6e1c7f6b6..c9d1aefa1 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1000,6 +1000,13 @@ header = "options/quantifiers_options.h" default = "true" help = "use approach to repair constants in sygus candidate solutions" +[[option]] + name = "sygusRepairConstTimeout" + category = "regular" + long = "sygus-repair-const-timeout=N" + type = "unsigned long" + help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions" + [[option]] name = "sygusMinGrammar" category = "regular" diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 75d595a39..89f04ffb6 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_repair_const.h" #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" @@ -97,6 +98,50 @@ bool SygusRepairConst::isActive() const return !d_base_inst.isNull() && d_allow_constant_grammar; } +void SygusRepairConst::initializeChecker(std::unique_ptr& checker, + ExprManager& em, + ExprManagerMapCollection& varMap, + Node query, + bool& needExport) +{ + NodeManager* nm = NodeManager::currentNM(); + 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. If the export fails, we throw an + // OptionException. + try + { + checker.reset(new SmtEngine(&em)); + checker->setTimeLimit(options::sygusRepairConstTimeout(), true); + checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); + // renable options disabled by sygus + checker->setOption("miniscope-quant", true); + checker->setOption("miniscope-quant-fv", true); + checker->setOption("quant-split", true); + // export + Expr e_query = query.toExpr().exportTo(&em, varMap); + checker->assertFormula(e_query); + } + catch (const CVC4::ExportUnsupportedException& e) + { + std::stringstream msg; + msg << "Unable to export " << query + << " but exporting expressions is required for " + "--sygus-repair-const-timeout."; + throw OptionException(msg.str()); + } + } + else + { + needExport = false; + checker.reset(new SmtEngine(nm->toExprManager())); + checker->assertFormula(query.toExpr()); + } +} + bool SygusRepairConst::repairSolution(const std::vector& candidates, const std::vector& candidate_values, std::vector& repair_cv, @@ -130,8 +175,8 @@ bool SygusRepairConst::repairSolution(const std::vector& candidates, for (unsigned i = 0, size = candidates.size(); i < size; i++) { Node cv = candidate_values[i]; - Node skeleton = - getSkeleton(cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles); + Node skeleton = getSkeleton( + cv, free_var_count, sk_vars, sk_vars_to_subs, useConstantsAsHoles); if (Trace.isOn("sygus-repair-const")) { Printer* p = Printer::getPrinter(options::outputLanguage()); @@ -206,68 +251,66 @@ bool SygusRepairConst::repairSolution(const std::vector& candidates, << std::endl; return false; } - - // do miniscoping explicitly - if (fo_body[1].getKind() == AND) - { - Node bvl = fo_body[0]; - std::vector children; - for (const Node& conj : fo_body[1]) - { - children.push_back(nm->mkNode(FORALL, bvl, conj)); - } - fo_body = nm->mkNode(AND, children); - } } Trace("cegqi-engine") << "Repairing previous solution..." << std::endl; // make the satisfiability query - SmtEngine repcChecker(nm->toExprManager()); - repcChecker.setLogic(smt::currentSmtEngine()->getLogicInfo()); - repcChecker.assertFormula(fo_body.toExpr()); - Result r = repcChecker.checkSat(); + bool needExport = false; + ExprManagerMapCollection varMap; + ExprManager em(nm->getOptions()); + std::unique_ptr repcChecker; + initializeChecker(repcChecker, em, varMap, fo_body, needExport); + Result r = repcChecker->checkSat(); Trace("sygus-repair-const") << "...got : " << r << std::endl; - if (r.asSatisfiabilityResult().isSat() != Result::UNSAT - && !r.asSatisfiabilityResult().isUnknown()) + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT + || r.asSatisfiabilityResult().isUnknown()) { - std::vector sk_sygus_m; - for (const Node& v : sk_vars) + Trace("cegqi-engine") << "...failed" << std::endl; + return false; + } + std::vector sk_sygus_m; + for (const Node& v : sk_vars) + { + Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end()); + Node fov = d_sk_to_fo[v]; + Node fov_m; + if (needExport) { - Assert(d_sk_to_fo.find(v) != d_sk_to_fo.end()); - Node fov = d_sk_to_fo[v]; - 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); - sk_sygus_m.push_back(fov_m_to_sygus); + Expr e_fov = fov.toExpr().exportTo(&em, varMap); + fov_m = Node::fromExpr( + repcChecker->getValue(e_fov).exportTo(nm->toExprManager(), varMap)); } - std::stringstream ss; - // convert back to sygus - for (unsigned i = 0, size = candidates.size(); i < size; i++) + else { - Node csk = candidate_skeletons[i]; - Node scsk = csk.substitute( - sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end()); - repair_cv.push_back(scsk); - if (Trace.isOn("sygus-repair-const") || Trace.isOn("cegqi-engine")) - { - std::stringstream sss; - Printer::getPrinter(options::outputLanguage()) - ->toStreamSygus(sss, repair_cv[i]); - ss << " * " << candidates[i] << " -> " << sss.str() << std::endl; - } + fov_m = Node::fromExpr(repcChecker->getValue(fov.toExpr())); } - Trace("cegqi-engine") << "...success:" << std::endl; - Trace("cegqi-engine") << ss.str(); - Trace("sygus-repair-const") - << "Repaired constants in solution : " << std::endl; - Trace("sygus-repair-const") << ss.str(); - return true; + Trace("sygus-repair-const") << " " << fov << " = " << fov_m << std::endl; + // convert to sygus + Node fov_m_to_sygus = d_tds->getProxyVariable(v.getType(), fov_m); + sk_sygus_m.push_back(fov_m_to_sygus); } - - Trace("cegqi-engine") << "...failed" << std::endl; - - return false; + std::stringstream ss; + // convert back to sygus + for (unsigned i = 0, size = candidates.size(); i < size; i++) + { + Node csk = candidate_skeletons[i]; + Node scsk = csk.substitute( + sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end()); + repair_cv.push_back(scsk); + if (Trace.isOn("sygus-repair-const") || Trace.isOn("cegqi-engine")) + { + std::stringstream sss; + Printer::getPrinter(options::outputLanguage()) + ->toStreamSygus(sss, repair_cv[i]); + ss << " * " << candidates[i] << " -> " << sss.str() << std::endl; + } + } + Trace("cegqi-engine") << "...success:" << std::endl; + Trace("cegqi-engine") << ss.str(); + Trace("sygus-repair-const") << "Repaired constants in solution : " + << std::endl; + Trace("sygus-repair-const") << ss.str(); + return true; } bool SygusRepairConst::mustRepair(Node n) diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index 3e45f9210..c6bfd2806 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -189,6 +189,26 @@ 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& checker, + ExprManager& em, + ExprManagerMapCollection& varMap, + Node query, + bool& needExport); }; } /* CVC4::theory::quantifiers namespace */ -- 2.30.2