diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-20 22:34:18 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-20 22:34:18 +0200 |
commit | 7c26406e8f2952197037b152272988f2ec1e3ad1 (patch) | |
tree | 9a7d35eaa94caeed4a530250226905243ba8f3e4 /src/theory/quantifiers | |
parent | b417642a83d1c4ebf6d2ba4182a95cdeec39e4d8 (diff) |
sygusComp2018: minor changes to repair constant utility (#2110)
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 12 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.cpp | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_repair_const.h | 6 |
4 files changed, 25 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index bf973bd97..b2b00a31c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -121,7 +121,17 @@ void CegConjecture::assign( Node q ) { // initialize the sygus constant repair utility if (options::sygusRepairConst()) { - d_sygus_rconst->initialize(d_base_inst, d_candidates); + d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates); + if (options::sygusConstRepairAbort()) + { + if (!d_sygus_rconst->isActive()) + { + // no constant repair is possible: abort + std::stringstream ss; + ss << "Grammar does not allow repair constants." << std::endl; + throw LogicException(ss.str()); + } + } } // register this term with sygus database and other utilities that impact diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index a678f1e79..37ee01370 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -397,7 +397,7 @@ void Cegis::registerRefinementLemma(const std::vector<Node>& vars, lems.push_back(rlem); } -bool Cegis::usingRepairConst() { return d_using_gr_repair; } +bool Cegis::usingRepairConst() { return true; } void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, const std::vector<Node>& ms, diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 4aaccc71e..71449029b 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -92,6 +92,11 @@ void SygusRepairConst::registerSygusType(TypeNode tn, } } +bool SygusRepairConst::isActive() const +{ + return !d_base_inst.isNull() && d_allow_constant_grammar; +} + bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates, const std::vector<Node>& candidate_values, std::vector<Node>& repair_cv, @@ -100,7 +105,7 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates, Assert(candidates.size() == candidate_values.size()); // if no grammar type allows constants, no repair is possible - if (d_base_inst.isNull() || !d_allow_constant_grammar) + if (!isActive()) { return false; } @@ -415,7 +420,7 @@ Node SygusRepairConst::getFoQuery(const std::vector<Node>& candidates, const std::vector<Node>& sk_vars) { NodeManager* nm = NodeManager::currentNM(); - Node body = d_base_inst.negate(); + Node body = d_base_inst; Trace("sygus-repair-const") << " Substitute skeletons..." << std::endl; body = body.substitute(candidates.begin(), candidates.end(), diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index ba1295988..3e45f9210 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -77,6 +77,12 @@ class SygusRepairConst const std::vector<Node>& candidate_values, std::vector<Node>& repair_cv, bool useConstantsAsHoles = false); + /** + * Return whether this module has the possibility to repair solutions. This is + * true if this module has been initialized, and at least one candidate has + * an "any constant" constructor. + */ + bool isActive() const; /** must repair? * * This returns true if n must be repaired for it to be a valid solution. |