diff options
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 23 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.cpp | 9 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_engine.h | 2 |
4 files changed, 23 insertions, 13 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 06f041d93..79bec60ee 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -562,7 +562,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates, Assert(vals.size() == candidates.size()); Node sbody = d_base_body.substitute( candidates.begin(), candidates.end(), vals.begin(), vals.end()); - Trace("cegis-sample-debug") << "Sample " << sbody << std::endl; + Trace("cegis-sample-debug2") << "Sample " << sbody << std::endl; // do eager unfolding std::map<Node, Node> visited_n; sbody = d_qe->getTermDatabaseSygus()->getEagerUnfold(sbody, visited_n); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 7955d59a8..b95af719e 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -458,11 +458,11 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) Node lem; // introduce the skolem variables std::vector<Node> sks; + std::vector<Node> vars; if (constructed_cand) { if (inst.getKind() == NOT && inst[0].getKind() == FORALL) { - std::vector<Node> vars; for (const Node& v : inst[0][0]) { Node sk = nm->mkSkolem("rsk", v.getType()); @@ -527,10 +527,11 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) { Trace("cegqi-engine") << " * Verification lemma failed for:\n "; // do not send out - for (const Node& v : d_ce_sk_vars) + for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++) { + Node v = d_ce_sk_vars[i]; Node mv = Node::fromExpr(verifySmt.getValue(v.toExpr())); - Trace("cegqi-engine") << v << " -> " << mv << " "; + Trace("cegqi-engine") << vars[i] << " -> " << mv << " "; d_ce_sk_var_mvs.push_back(mv); } Trace("cegqi-engine") << std::endl; @@ -955,7 +956,7 @@ void SynthConjecture::printAndContinueStream() void SynthConjecture::printSynthSolution(std::ostream& out) { - Trace("cegqi-debug") << "Printing synth solution..." << std::endl; + Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl; Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren()); std::vector<Node> sols; std::vector<int> statuses; @@ -981,8 +982,10 @@ void SynthConjecture::printSynthSolution(std::ostream& out) bool is_unique_term = true; - if (status != 0 && options::sygusRewSynth()) + if (status != 0 && (options::sygusRewSynth() || options::sygusQueryGen() + || options::sygusSolFilterImplied())) { + Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl; std::map<Node, ExpressionMinerManager>::iterator its = d_exprm.find(prog); if (its == d_exprm.end()) @@ -993,6 +996,14 @@ void SynthConjecture::printSynthSolution(std::ostream& out) { d_exprm[prog].enableRewriteRuleSynth(); } + if (options::sygusQueryGen()) + { + d_exprm[prog].enableQueryGeneration(options::sygusQueryGenThresh()); + } + if (options::sygusSolFilterImplied()) + { + d_exprm[prog].enableFilterImpliedSolutions(); + } its = d_exprm.find(prog); } bool rew_print = false; @@ -1003,7 +1014,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out) } if (!is_unique_term) { - ++(cei->d_statistics.d_candidate_rewrites); + ++(cei->d_statistics.d_filtered_solutions); } } if (is_unique_term) diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index ba227bc8f..479cfa535 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -426,17 +426,16 @@ SynthEngine::Statistics::Statistics() d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0), d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0), d_solutions("SynthConjecture::solutions", 0), - d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", - 0), - d_candidate_rewrites("SynthConjecture::candidate_rewrites", 0) + d_filtered_solutions("SynthConjecture::filtered_solutions", 0), + d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", 0) { smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); smtStatisticsRegistry()->registerStat(&d_solutions); + smtStatisticsRegistry()->registerStat(&d_filtered_solutions); smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print); - smtStatisticsRegistry()->registerStat(&d_candidate_rewrites); } SynthEngine::Statistics::~Statistics() @@ -445,8 +444,8 @@ SynthEngine::Statistics::~Statistics() smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); smtStatisticsRegistry()->unregisterStat(&d_solutions); + smtStatisticsRegistry()->unregisterStat(&d_filtered_solutions); smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print); - smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites); } } // namespace quantifiers diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 8f0eea58f..a7346b888 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -100,8 +100,8 @@ class SynthEngine : public QuantifiersModule IntStat d_cegqi_lemmas_refine; IntStat d_cegqi_si_lemmas; IntStat d_solutions; + IntStat d_filtered_solutions; IntStat d_candidate_rewrites_print; - IntStat d_candidate_rewrites; Statistics(); ~Statistics(); }; /* class SynthEngine::Statistics */ |