diff options
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 27 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 52 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 34 |
3 files changed, 36 insertions, 77 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index fdbb0750b..0119f44aa 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -70,7 +70,6 @@ SynthConjecture::SynthConjecture(Env& env, d_ceg_cegisUnif(new CegisUnif(env, qs, qim, d_tds, this)), d_sygus_ccore(new CegisCoreConnective(env, qs, qim, d_tds, this)), d_master(nullptr), - d_setInnerSksModel(false), d_repair_index(0), d_guarded_stream_exc(false) { @@ -304,7 +303,6 @@ bool SynthConjecture::needsCheck() return true; } -bool SynthConjecture::needsRefinement() const { return d_setInnerSksModel; } bool SynthConjecture::doCheck() { if (isSingleInvocation()) @@ -515,7 +513,6 @@ bool SynthConjecture::doCheck() recordSolution(candidate_values); return true; } - Assert(!d_setInnerSksModel); // print the candidate solution for debugging if (constructed_cand && printDebug) @@ -534,8 +531,6 @@ bool SynthConjecture::doCheck() out << ")" << std::endl; } - d_setInnerSksModel = true; - if (query.isNull()) { // no lemma to check @@ -546,12 +541,13 @@ bool SynthConjecture::doCheck() // here since the result of the satisfiability test may be unknown. recordSolution(candidate_values); - Result r = d_verify.verify(query, d_innerSks, d_innerSksModel); + std::vector<Node> skModel; + Result r = d_verify.verify(query, d_innerSks, skModel); if (r.asSatisfiabilityResult().isSat() == Result::SAT) { // we have a counterexample - return false; + return processCounterexample(skModel); } else if (r.asSatisfiabilityResult().isSat() != Result::UNSAT) { @@ -607,22 +603,19 @@ bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const return true; } -bool SynthConjecture::doRefine() +bool SynthConjecture::processCounterexample(const std::vector<Node>& skModel) { - Assert(d_setInnerSksModel); Trace("cegqi-refine") << "doRefine : Construct refinement lemma..." << std::endl; Trace("cegqi-refine-debug") << " For counterexample skolems : " << d_innerSks << std::endl; Node base_lem = d_checkBody.negate(); - Assert(d_innerSks.size() == d_innerSksModel.size()); + Assert(d_innerSks.size() == skModel.size()); Trace("cegqi-refine") << "doRefine : substitute..." << std::endl; - base_lem = base_lem.substitute(d_innerSks.begin(), - d_innerSks.end(), - d_innerSksModel.begin(), - d_innerSksModel.end()); + base_lem = base_lem.substitute( + d_innerSks.begin(), d_innerSks.end(), skModel.begin(), skModel.end()); Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl; base_lem = d_tds->rewriteNode(base_lem); Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem @@ -630,8 +623,6 @@ bool SynthConjecture::doRefine() size_t prevPending = d_qim.numPendingLemmas(); d_master->registerRefinementLemma(d_innerSks, base_lem); Trace("cegqi-refine") << "doRefine : finished" << std::endl; - d_setInnerSksModel = false; - d_innerSksModel.clear(); // check if we added a lemma bool addedLemma = d_qim.numPendingLemmas() > prevPending; @@ -753,10 +744,6 @@ void SynthConjecture::excludeCurrentSolution(const std::vector<Node>& enums, { Trace("cegqi-debug") << "Exclude current solution: " << enums << " / " << values << std::endl; - // We will not refine the current candidate solution since it is a solution - // thus, we clear information regarding the current refinement - d_setInnerSksModel = false; - d_innerSksModel.clear(); // However, we need to exclude the current solution using an explicit // blocking clause, so that we proceed to the next solution. We do this only // for passively-generated enumerators (TermDbSygus::isPassiveEnumerator). diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index a146c3b15..005ae4361 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -71,8 +71,6 @@ class SynthConjecture : protected EnvObj //-------------------------------for counterexample-guided check/refine /** whether the conjecture is waiting for a call to doCheck below */ bool needsCheck(); - /** whether the conjecture is waiting for a call to doRefine below */ - bool needsRefinement() const; /** do syntax-guided enumerative check * * This is step 2(a) of Figure 3 of Reynolds et al CAV 2015. @@ -87,25 +85,6 @@ class SynthConjecture : protected EnvObj * when each of t1, ..., tn fails to satisfy the current refinement lemmas. */ bool doCheck(); - /** do refinement - * - * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. - * - * This method is run when needsRefinement() returns true, indicating that - * the last call to doCheck found a counterexample to the last candidate. - * - * This method adds a refinement lemma on the output channel of quantifiers - * engine. If the refinement lemma is a duplicate, then we manually - * exclude the current candidate via excludeCurrentSolution. This should - * only occur when the synthesis conjecture for the current candidate fails - * to evaluate to false for a given counterexample point, but regardless its - * negation is satisfiable for the current candidate and that point. This is - * exclusive to theories with partial functions, e.g. (non-linear) division. - * - * This method returns true if a lemma was added on the output channel, and - * false otherwise. - */ - bool doRefine(); //-------------------------------end for counterexample-guided check/refine /** * Prints the current synthesis solution to output stream out. This is @@ -178,6 +157,25 @@ class SynthConjecture : protected EnvObj SygusStatistics& getSygusStatistics() { return d_stats; }; private: + /** do refinement + * + * This is step 2(b) of Figure 3 of Reynolds et al CAV 2015. + * + * This method is run when skModel is corresponds to a counterexample to the + * last candidate in the doCheck method. + * + * This method adds a refinement lemma on the output channel of quantifiers + * engine. If the refinement lemma is a duplicate, then we manually + * exclude the current candidate via excludeCurrentSolution. This should + * only occur when the synthesis conjecture for the current candidate fails + * to evaluate to false for a given counterexample point, but regardless its + * negation is satisfiable for the current candidate and that point. This is + * exclusive to theories with partial functions, e.g. (non-linear) division. + * + * This method returns true if a lemma was added on the output channel, and + * false otherwise. + */ + bool processCounterexample(const std::vector<Node>& skModel); /** Reference to the quantifiers state */ QuantifiersState& d_qstate; /** Reference to the quantifiers inference manager */ @@ -274,18 +272,6 @@ class SynthConjecture : protected EnvObj std::vector<Node> d_innerVars; /** list of skolems on inner quantification */ std::vector<Node> d_innerSks; - /** - * If we have already tested the satisfiability of the current verification - * lemma, this stores the model values of d_innerSks in the current - * (satisfiable, failed) verification lemma. - */ - std::vector<Node> d_innerSksModel; - /** - * Whether the above vector has been set. We have this flag since the above - * vector may be set to empty (e.g. for ground synthesis conjectures). - */ - bool d_setInnerSksModel; - /** the asserted (negated) conjecture */ Node d_quant; /** diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 454442351..4bee80ab8 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -122,10 +122,7 @@ void SynthEngine::check(Theory::Effort e, QEffort quant_e) SynthConjecture* sc = activeCheckConj[i]; if (!checkConjecture(sc)) { - if (!sc->needsRefinement()) - { - acnext.push_back(sc); - } + acnext.push_back(sc); } } activeCheckConj.clear(); @@ -208,29 +205,18 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) conj->debugPrint("sygus-engine-debug"); Trace("sygus-engine-debug") << std::endl; } - - if (!conj->needsRefinement()) + Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl; + Trace("sygus-engine-debug") << " *** Check candidate phase..." << std::endl; + size_t prevPending = d_qim.numPendingLemmas(); + bool ret = conj->doCheck(); + // if we added a lemma, return true + if (d_qim.numPendingLemmas() > prevPending) { - Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl; Trace("sygus-engine-debug") - << " *** Check candidate phase..." << std::endl; - size_t prevPending = d_qim.numPendingLemmas(); - bool ret = conj->doCheck(); - // if we added a lemma, return true - if (d_qim.numPendingLemmas() > prevPending) - { - Trace("sygus-engine-debug") - << " ...check for counterexample." << std::endl; - return true; - } - if (!conj->needsRefinement()) - { - return ret; - } - // otherwise, immediately go to refine candidate + << " ...check for counterexample." << std::endl; + return true; } - Trace("sygus-engine-debug") << " *** Refine candidate phase..." << std::endl; - return conj->doRefine(); + return ret; } bool SynthEngine::getSynthSolutions( |