diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-25 16:19:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-25 16:19:58 -0500 |
commit | b25c979f6db06a4aad82f0e18fc8432f85707347 (patch) | |
tree | bc83f304cab407e76828f37ec3fc8a0296c1c267 /src | |
parent | 9fc8a7885c89e488daeeaf73c9f099b9d906f3ca (diff) |
Reenable repair const (#1983)
Diffstat (limited to 'src')
-rw-r--r-- | src/options/quantifiers_options.toml | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 27 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_module.h | 6 |
5 files changed, 38 insertions, 1 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 4a7004821..107f3896f 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -989,7 +989,7 @@ header = "options/quantifiers_options.h" category = "regular" long = "sygus-repair-const" type = "bool" - default = "false" + default = "true" help = "use approach to repair constants in sygus candidate solutions" [[option]] diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index f66a97ce8..ecb6db2fb 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -258,6 +258,33 @@ void CegConjecture::doCheck(std::vector<Node>& lems) std::vector<Node> candidate_values; bool constructed_cand = false; + // If a module is not trying to repair constants in solutions and the option + // sygusRepairConst is true, we use a default scheme for trying to repair + // constants here. + if (options::sygusRepairConst() && !d_master->usingRepairConst()) + { + Trace("cegqi-check") << "CegConjuncture : repair previous solution..." + << std::endl; + // have we tried to repair the previous solution? + // if not, call the repair constant utility + unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size(); + if (d_repair_index < ninst) + { + std::vector<Node> fail_cvs; + for (const Node& cprog : d_candidates) + { + Assert(d_repair_index < d_cinfo[cprog].d_inst.size()); + fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]); + } + d_repair_index++; + if (d_sygus_rconst->repairSolution( + d_candidates, fail_cvs, candidate_values)) + { + constructed_cand = true; + } + } + } + // get the model value of the relevant terms from the master module std::vector<Node> enum_values; getModelValues(terms, enum_values); diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 92ed41f3d..ee54c3296 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -397,6 +397,8 @@ void Cegis::registerRefinementLemma(const std::vector<Node>& vars, lems.push_back(rlem); } +bool Cegis::usingRepairConst() { return d_using_gr_repair; } + void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, const std::vector<Node>& ms, std::vector<Node>& lems) diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index ca27a2281..856219b73 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -63,6 +63,8 @@ class Cegis : public SygusModule virtual void registerRefinementLemma(const std::vector<Node>& vars, Node lem, std::vector<Node>& lems) override; + /** using repair const */ + virtual bool usingRepairConst() override; protected: /** the evaluation unfold utility of d_tds */ diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index 75be570e6..b01f8e1d0 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -122,6 +122,12 @@ class SygusModule { return Node::null(); } + /** + * Are we trying to repair constants in candidate solutions? + * If we return true for usingRepairConst is true, then this module has + * attmepted to repair any solutions returned by constructCandidates. + */ + virtual bool usingRepairConst() { return false; } protected: /** reference to quantifier engine */ |