From: Andrew Reynolds Date: Fri, 20 Jul 2018 20:34:18 +0000 (+0200) Subject: sygusComp2018: minor changes to repair constant utility (#2110) X-Git-Tag: cvc5-1.0.0~4884 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7c26406e8f2952197037b152272988f2ec1e3ad1;p=cvc5.git sygusComp2018: minor changes to repair constant utility (#2110) --- diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index fa8f07dac..8e954ddc0 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -969,6 +969,15 @@ header = "options/quantifiers_options.h" read_only = true help = "abort if synthesis conjecture is not single invocation" +[[option]] + name = "sygusConstRepairAbort" + category = "regular" + long = "sygus-crepair-abort" + type = "bool" + default = "false" + read_only = true + help = "abort if constant repair techniques are not applicable" + [[option]] name = "sygusUnif" category = "regular" 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& vars, lems.push_back(rlem); } -bool Cegis::usingRepairConst() { return d_using_gr_repair; } +bool Cegis::usingRepairConst() { return true; } void Cegis::getRefinementEvalLemmas(const std::vector& vs, const std::vector& 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& candidates, const std::vector& candidate_values, std::vector& repair_cv, @@ -100,7 +105,7 @@ bool SygusRepairConst::repairSolution(const std::vector& 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& candidates, const std::vector& 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& candidate_values, std::vector& 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.