diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-03 15:28:34 -0500 |
---|---|---|
committer | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-10-03 15:28:34 -0500 |
commit | aecb70fd1ab7c8928d8a440278a8cf2a9a828984 (patch) | |
tree | 10973aa805b2ecf4948555b1703c7f39baf91e36 /src/theory/quantifiers/sygus/cegis.cpp | |
parent | ef1e8fd92dc24fc02754c9573c1dac6c473bf2ca (diff) |
Add actively generated sygus enumerators (#2552)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 43 |
1 files changed, 29 insertions, 14 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index db9af10b4..9706e3732 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -68,8 +68,19 @@ bool Cegis::processInitialize(Node n, std::vector<Node>& lemmas) { Trace("cegis") << "Initialize cegis..." << std::endl; + unsigned csize = candidates.size(); + // We only can use actively-generated enumerators if there is only one + // function-to-synthesize. Otherwise, we would have to generate a "product" of + // two actively-generated enumerators. That is, given a conjecture with two + // functions-to-synthesize with enumerators e_f and e_g, if: + // e_f -> t1, ..., tn + // e_g -> s1, ..., sm + // This module would expect constructCandidates calls (e_f,e_g) -> (ti, sj) + // for each i,j. We do not do this and revert to the default behavior of + // this module instead. + bool isVarAgnostic = options::sygusEnumVarAgnostic() && csize == 1; // initialize an enumerator for each candidate - for (unsigned i = 0; i < candidates.size(); i++) + for (unsigned i = 0; i < csize; i++) { Trace("cegis") << "...register enumerator " << candidates[i]; bool do_repair_const = false; @@ -86,8 +97,13 @@ bool Cegis::processInitialize(Node n, } } Trace("cegis") << std::endl; - d_tds->registerEnumerator( - candidates[i], candidates[i], d_parent, false, do_repair_const); + // variable agnostic enumerators require an active guard + d_tds->registerEnumerator(candidates[i], + candidates[i], + d_parent, + isVarAgnostic, + do_repair_const, + isVarAgnostic); } return true; } @@ -99,7 +115,8 @@ void Cegis::getTermList(const std::vector<Node>& candidates, } bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, - const std::vector<Node>& candidate_values) + const std::vector<Node>& candidate_values, + std::vector<Node>& lems) { // First, decide if this call will apply "conjecture-specific refinement". // In other words, in some settings, the following method will identify and @@ -144,13 +161,14 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, } if (!cre_lems.empty()) { - for (const Node& lem : cre_lems) + lems.insert(lems.end(), cre_lems.begin(), cre_lems.end()); + addedEvalLemmas = true; + if (Trace.isOn("cegqi-lemma")) { - if (d_qe->addLemma(lem)) + for (const Node& lem : cre_lems) { Trace("cegqi-lemma") << "Cegqi::Lemma : ref evaluation : " << lem << std::endl; - addedEvalLemmas = true; } } /* we could, but do not return here. experimentally, it is better to @@ -178,12 +196,9 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates, { Node lem = nm->mkNode( OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i])); - if (d_qe->addLemma(lem)) - { - Trace("cegqi-lemma") - << "Cegqi::Lemma : evaluation unfold : " << lem << std::endl; - addedEvalLemmas = true; - } + lems.push_back(lem); + Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation unfold : " << lem + << std::endl; } } return addedEvalLemmas; @@ -258,7 +273,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, } // evaluate on refinement lemmas - bool addedEvalLemmas = addEvalLemmas(enums, enum_values); + bool addedEvalLemmas = addEvalLemmas(enums, enum_values, lems); // try to construct candidates if (!processConstructCandidates(enums, |