diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-09-27 13:57:17 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-09-27 13:57:17 -0500 |
commit | a6cc1d8ebff497392533bbb16782bda6351648df (patch) | |
tree | 221f27e8b528d317fa75b2af8084cc4ad520c739 /src/theory/quantifiers/sygus/cegis.cpp | |
parent | 23f51f715f625a1275a7cb14a3a96e85e1290a89 (diff) |
Infrastructure for using active enumerators in sygus modules (#2547)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 71 |
1 files changed, 57 insertions, 14 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index fbe0da7a8..db9af10b4 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -13,6 +13,7 @@ **/ #include "theory/quantifiers/sygus/cegis.h" +#include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/quantifiers_options.h" #include "printer/printer.h" @@ -100,15 +101,47 @@ void Cegis::getTermList(const std::vector<Node>& candidates, bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, const std::vector<Node>& candidate_values) { + // First, decide if this call will apply "conjecture-specific refinement". + // In other words, in some settings, the following method will identify and + // block a class of solutions {candidates -> S} that generalizes the current + // one (given by {candidates -> candidate_values}), such that for each + // candidate_values' in S, we have that {candidates -> candidate_values'} is + // also not a solution for the given conjecture. We may not + // apply this form of refinement if any (relevant) enumerator in candidates is + // "actively generated" (see TermDbSygs::isPassiveEnumerator), since its + // model values are themselves interpreted as classes of solutions. + bool doGen = true; + for (const Node& v : candidates) + { + // if it is relevant to refinement + if (d_refinement_lemma_vars.find(v) != d_refinement_lemma_vars.end()) + { + if (!d_tds->isPassiveEnumerator(v)) + { + doGen = false; + break; + } + } + } NodeManager* nm = NodeManager::currentNM(); bool addedEvalLemmas = false; if (options::sygusRefEval()) { - Trace("cegqi-engine") << " *** Do refinement lemma evaluation..." - << std::endl; + Trace("cegqi-engine") << " *** Do refinement lemma evaluation" + << (doGen ? " with conjecture-specific refinement" + : "") + << "..." << std::endl; // see if any refinement lemma is refuted by evaluation std::vector<Node> cre_lems; - getRefinementEvalLemmas(candidates, candidate_values, cre_lems); + bool ret = + getRefinementEvalLemmas(candidates, candidate_values, cre_lems, doGen); + if (ret && !doGen) + { + Trace("cegqi-engine") << "...(actively enumerated) candidate failed " + "refinement lemma evaluation." + << std::endl; + return true; + } if (!cre_lems.empty()) { for (const Node& lem : cre_lems) @@ -124,7 +157,8 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, add the lemmas below as well, in parallel. */ } } - if (d_eval_unfold != nullptr) + // we only do evaluation unfolding for passive enumerators + if (doGen && d_eval_unfold != nullptr) { Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl; std::vector<Node> eager_terms, eager_vals, eager_exps; @@ -281,6 +315,8 @@ void Cegis::addRefinementLemma(Node lem) } // rewrite with extended rewriter slem = d_tds->getExtRewriter()->extendedRewrite(slem); + // collect all variables in slem + expr::getSymbols(slem, d_refinement_lemma_vars); std::vector<Node> waiting; waiting.push_back(lem); unsigned wcounter = 0; @@ -408,10 +444,10 @@ void Cegis::registerRefinementLemma(const std::vector<Node>& vars, } bool Cegis::usingRepairConst() { return true; } - -void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, +bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, const std::vector<Node>& ms, - std::vector<Node>& lems) + std::vector<Node>& lems, + bool doGen) { Trace("sygus-cref-eval") << "Cref eval : conjecture has " << d_refinement_lemma_unit.size() << " unit and " @@ -424,6 +460,7 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, Node nfalse = nm->mkConst(false); Node neg_guard = d_parent->getGuard().negate(); + bool ret = false; for (unsigned r = 0; r < 2; r++) { std::unordered_set<Node, NodeHashFunction>& rlemmas = @@ -447,6 +484,12 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, << "...after unfolding is : " << lemcsu << std::endl; if (lemcsu.isConst() && !lemcsu.getConst<bool>()) { + if (!doGen) + { + // we are not generating the lemmas, instead just return + return true; + } + ret = true; std::vector<Node> msu; std::vector<Node> mexp; msu.insert(msu.end(), ms.begin(), ms.end()); @@ -480,13 +523,12 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, { cre_lem = neg_guard; } - } - if (!cre_lem.isNull() - && std::find(lems.begin(), lems.end(), cre_lem) == lems.end()) - { - Trace("sygus-cref-eval") - << "...produced lemma : " << cre_lem << std::endl; - lems.push_back(cre_lem); + if (std::find(lems.begin(), lems.end(), cre_lem) == lems.end()) + { + Trace("sygus-cref-eval") << "...produced lemma : " << cre_lem + << std::endl; + lems.push_back(cre_lem); + } } } if (!lems.empty()) @@ -494,6 +536,7 @@ void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, break; } } + return ret; } bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, |