From b25c979f6db06a4aad82f0e18fc8432f85707347 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 25 May 2018 16:19:58 -0500 Subject: [PATCH] Reenable repair const (#1983) --- src/options/quantifiers_options.toml | 2 +- .../sygus/ce_guided_conjecture.cpp | 27 +++++++++++++++++++ src/theory/quantifiers/sygus/cegis.cpp | 2 ++ src/theory/quantifiers/sygus/cegis.h | 2 ++ src/theory/quantifiers/sygus/sygus_module.h | 6 +++++ test/regress/regress0/expect/scrub.08.sy | 2 +- .../regress1/quantifiers/horn-simple.smt2 | 2 +- test/regress/regress2/sygus/vcb.sy | 2 +- 8 files changed, 41 insertions(+), 4 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& lems) std::vector 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 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 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& vars, lems.push_back(rlem); } +bool Cegis::usingRepairConst() { return d_using_gr_repair; } + void Cegis::getRefinementEvalLemmas(const std::vector& vs, const std::vector& ms, std::vector& 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& vars, Node lem, std::vector& 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 */ diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy index 360474f84..24a0aab2e 100644 --- a/test/regress/regress0/expect/scrub.08.sy +++ b/test/regress/regress0/expect/scrub.08.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-sygus-repair-const ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. ; EXPECT: The fact in question: TERM diff --git a/test/regress/regress1/quantifiers/horn-simple.smt2 b/test/regress/regress1/quantifiers/horn-simple.smt2 index a27d8e0d6..6c5039c2b 100644 --- a/test/regress/regress1/quantifiers/horn-simple.smt2 +++ b/test/regress/regress1/quantifiers/horn-simple.smt2 @@ -6,7 +6,7 @@ (assert (forall ((x Int)) (=> (= x 0) (I x)))) -(assert (forall ((x Int)) (=> (and (I x) (< x 1)) (I (+ x 1))))) +(assert (forall ((x Int)) (=> (and (I x) (< x 6)) (I (+ x 1))))) (assert (forall ((x Int)) (=> (I x) (<= x 10)))) diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress2/sygus/vcb.sy index 7f895fae4..d8d4ff9bb 100644 --- a/test/regress/regress2/sygus/vcb.sy +++ b/test/regress/regress2/sygus/vcb.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --sygus-out=status --no-sygus-repair-const (set-logic LIA) (synth-fun f1 ((x1 Int) (x2 Int)) Int) -- 2.30.2