diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-22 20:27:32 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-22 20:27:32 -0500 |
commit | 2ac3d0bf2c00edbbd04033815f10ba0207010f77 (patch) | |
tree | 7a61979523714dfefa6ba8277b38b0b382706f28 /src/theory/quantifiers/sygus/cegis.cpp | |
parent | eab7fae2c02ce635500dbe7c743a5c0d7f39137d (diff) |
Repair constants using symbolic constructors (#1960)
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 69 |
1 files changed, 59 insertions, 10 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index fc41c7561..92ed41f3d 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -29,7 +29,7 @@ namespace theory { namespace quantifiers { Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p) - : SygusModule(qe, p), d_eval_unfold(nullptr) + : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false) { if (options::sygusEvalUnfold()) { @@ -66,10 +66,27 @@ bool Cegis::processInitialize(Node n, const std::vector<Node>& candidates, std::vector<Node>& lemmas) { + Trace("cegis") << "Initialize cegis..." << std::endl; // initialize an enumerator for each candidate for (unsigned i = 0; i < candidates.size(); i++) { - d_tds->registerEnumerator(candidates[i], candidates[i], d_parent); + Trace("cegis") << "...register enumerator " << candidates[i]; + bool do_repair_const = false; + if (options::sygusRepairConst()) + { + TypeNode ctn = candidates[i].getType(); + d_tds->registerSygusType(ctn); + if (d_tds->hasSubtermSymbolicCons(ctn)) + { + do_repair_const = true; + // remember that we are doing grammar-based repair + d_using_gr_repair = true; + Trace("cegis") << " (using repair)"; + } + } + Trace("cegis") << std::endl; + d_tds->registerEnumerator( + candidates[i], candidates[i], d_parent, false, do_repair_const); } return true; } @@ -156,6 +173,46 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums, Trace("cegis") << ss.str() << std::endl; } } + // if we are using grammar-based repair + if (d_using_gr_repair) + { + SygusRepairConst* src = d_parent->getRepairConst(); + Assert(src != nullptr); + // check if any enum_values have symbolic terms that must be repaired + bool mustRepair = false; + for (const Node& c : enum_values) + { + if (SygusRepairConst::mustRepair(c)) + { + mustRepair = true; + break; + } + } + Trace("cegis") << "...must repair is: " << mustRepair << std::endl; + // if the solution contains a subterm that must be repaired + if (mustRepair) + { + std::vector<Node> fail_cvs = enum_values; + Assert(candidates.size() == fail_cvs.size()); + if (src->repairSolution(candidates, fail_cvs, candidate_values)) + { + return true; + } + // repair solution didn't work, exclude this solution + std::vector<Node> exp; + for (unsigned i = 0, size = enums.size(); i < size; i++) + { + d_tds->getExplain()->getExplanationForEquality( + enums[i], enum_values[i], exp); + } + Assert(!exp.empty()); + Node expn = + exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp); + lems.push_back(expn.negate()); + return false; + } + } + // evaluate on refinement lemmas bool addedEvalLemmas = addEvalLemmas(enums, enum_values); @@ -197,14 +254,6 @@ bool Cegis::processConstructCandidates(const std::vector<Node>& enums, candidate_values.end(), enum_values.begin(), enum_values.end()); return true; } - SygusRepairConst* src = d_parent->getRepairConst(); - if (src != nullptr) - { - // it may be repairable - std::vector<Node> fail_cvs = enum_values; - Assert(candidates.size() == fail_cvs.size()); - return src->repairSolution(candidates, fail_cvs, candidate_values); - } return false; } |