From 04114df7dd58bd7391704a94fe98e2935b39130d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 12 Feb 2018 16:14:29 -0600 Subject: [PATCH] Minor improvements to sygus sampler (#1598) --- .../quantifiers/ce_guided_conjecture.cpp | 37 +++++++++++-------- .../quantifiers/ce_guided_instantiation.cpp | 3 ++ .../quantifiers/ce_guided_instantiation.h | 1 + src/theory/quantifiers/dynamic_rewrite.cpp | 9 ++++- src/theory/quantifiers/dynamic_rewrite.h | 5 +++ src/theory/quantifiers/sygus_sampler.cpp | 8 +++- src/theory/quantifiers/sygus_sampler.h | 22 ++++++++--- 7 files changed, 62 insertions(+), 23 deletions(-) diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp index b6ba792df..0ce9b7c72 100644 --- a/src/theory/quantifiers/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/ce_guided_conjecture.cpp @@ -623,7 +623,8 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol); } out << ")" << std::endl; - ++(d_qe->getCegInstantiation()->d_statistics.d_solutions); + CegInstantiation* cei = d_qe->getCegInstantiation(); + ++(cei->d_statistics.d_solutions); if (status != 0 && options::sygusRewSynth()) { @@ -640,22 +641,26 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation // eq_sol is a candidate solution that is equivalent to sol if (eq_sol != solb) { - // Terms solb and eq_sol are equivalent under sample points but do - // not rewrite to the same term. Hence, this indicates a candidate - // rewrite. - out << "(candidate-rewrite " << solb << " " << eq_sol << ")" - << std::endl; - ++(d_qe->getCegInstantiation()->d_statistics.d_candidate_rewrites); - // debugging information - if (Trace.isOn("sygus-rr-debug")) + ++(cei->d_statistics.d_candidate_rewrites); + if (!eq_sol.isNull()) { - ExtendedRewriter* er = sygusDb->getExtRewriter(); - Node solbr = er->extendedRewrite(solb); - Node eq_solr = er->extendedRewrite(eq_sol); - Trace("sygus-rr-debug") - << "; candidate #1 ext-rewrites to: " << solbr << std::endl; - Trace("sygus-rr-debug") - << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl; + // Terms solb and eq_sol are equivalent under sample points but do + // not rewrite to the same term. Hence, this indicates a candidate + // rewrite. + out << "(candidate-rewrite " << solb << " " << eq_sol << ")" + << std::endl; + ++(cei->d_statistics.d_candidate_rewrites_print); + // debugging information + if (Trace.isOn("sygus-rr-debug")) + { + ExtendedRewriter* er = sygusDb->getExtRewriter(); + Node solbr = er->extendedRewrite(solb); + Node eq_solr = er->extendedRewrite(eq_sol); + Trace("sygus-rr-debug") + << "; candidate #1 ext-rewrites to: " << solbr << std::endl; + Trace("sygus-rr-debug") + << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl; + } } } } diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp index fbafb8b8c..ea2a2d13a 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.cpp +++ b/src/theory/quantifiers/ce_guided_instantiation.cpp @@ -362,6 +362,7 @@ CegInstantiation::Statistics::Statistics() d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0), d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0), d_solutions("CegConjecture::solutions", 0), + d_candidate_rewrites_print("CegConjecture::candidate_rewrites_print", 0), d_candidate_rewrites("CegConjecture::candidate_rewrites", 0) { @@ -369,6 +370,7 @@ CegInstantiation::Statistics::Statistics() smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); smtStatisticsRegistry()->registerStat(&d_solutions); + smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print); smtStatisticsRegistry()->registerStat(&d_candidate_rewrites); } @@ -377,6 +379,7 @@ CegInstantiation::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); smtStatisticsRegistry()->unregisterStat(&d_solutions); + smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print); smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites); } diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h index 644e5b3ef..2dc74dc72 100644 --- a/src/theory/quantifiers/ce_guided_instantiation.h +++ b/src/theory/quantifiers/ce_guided_instantiation.h @@ -75,6 +75,7 @@ public: IntStat d_cegqi_lemmas_refine; IntStat d_cegqi_si_lemmas; IntStat d_solutions; + IntStat d_candidate_rewrites_print; IntStat d_candidate_rewrites; Statistics(); ~Statistics(); diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index a19695770..3462a4d10 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -25,7 +25,8 @@ namespace quantifiers { DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe) : d_qe(qe), - d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true) + d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true), + d_rewrites(qe->getUserContext()) { d_equalityEngine.addFunctionKind(kind::APPLY_UF); } @@ -42,20 +43,26 @@ bool DynamicRewriter::addRewrite(Node a, Node b) // add to the equality engine Node ai = toInternal(a); Node bi = toInternal(b); + Trace("dyn-rewrite-debug") << "Internal : " << ai << " " << bi << std::endl; d_equalityEngine.addTerm(ai); d_equalityEngine.addTerm(bi); + Trace("dyn-rewrite-debug") << "get reps..." << std::endl; // may already be equal by congruence Node air = d_equalityEngine.getRepresentative(ai); Node bir = d_equalityEngine.getRepresentative(bi); + Trace("dyn-rewrite-debug") << "Reps : " << air << " " << bir << std::endl; if (air == bir) { Trace("dyn-rewrite") << "...fail, congruent." << std::endl; return false; } + Trace("dyn-rewrite-debug") << "assert eq..." << std::endl; Node eq = ai.eqNode(bi); + d_rewrites.push_back(eq); d_equalityEngine.assertEquality(eq, true, eq); + Trace("dyn-rewrite-debug") << "Finished" << std::endl; return true; } diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index be2ff4c78..2b5464151 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -19,6 +19,7 @@ #include +#include "context/cdlist.h" #include "theory/quantifiers_engine.h" #include "theory/uf/equality_engine.h" @@ -51,6 +52,8 @@ namespace quantifiers { */ class DynamicRewriter { + typedef context::CDList NodeList; + public: DynamicRewriter(const std::string& name, QuantifiersEngine* qe); ~DynamicRewriter() {} @@ -105,6 +108,8 @@ class DynamicRewriter std::map d_term_to_internal; /** stores congruence closure over terms given to this class. */ eq::EqualityEngine d_equalityEngine; + /** list of all equalities asserted to equality engine */ + NodeList d_rewrites; }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 757b8e44f..aa0a4b778 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -430,6 +430,7 @@ Node SygusSampler::evaluate(Node n, unsigned index) // just a substitution std::vector& pt = d_samples[index]; Node ev = n.substitute(d_vars.begin(), d_vars.end(), pt.begin(), pt.end()); + Trace("sygus-sample-ev-debug") << "Rewrite : " << ev << std::endl; ev = Rewriter::rewrite(ev); Trace("sygus-sample-ev") << "( " << n << ", " << index << " ) -> " << ev << std::endl; @@ -656,6 +657,8 @@ void SygusSamplerExt::initializeSygusExt(QuantifiersEngine* qe, Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) { Node eq_n = SygusSampler::registerTerm(n, forceKeep); + Trace("sygus-synth-rr") << "sygusSampleExt : " << n << "..." << eq_n + << std::endl; if (eq_n == n) { return n; @@ -678,9 +681,11 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) isUnique = containsFreeVariables(eq_n, n); } } + Trace("sygus-synth-rr-debug") << "AlphaEq unique: " << isUnique << std::endl; bool rewRedundant = false; if (d_drewrite != nullptr) { + Trace("sygus-synth-rr-debug") << "Add rewrite..." << std::endl; if (!d_drewrite->addRewrite(n, eq_n)) { rewRedundant = isUnique; @@ -688,6 +693,7 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) isUnique = false; } } + Trace("sygus-synth-rr-debug") << "Rewrite unique: " << isUnique << std::endl; if (isUnique) { @@ -709,7 +715,7 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) } Trace("sygus-synth-rr") << std::endl; } - return n; + return Node::null(); } } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 48ddddbc6..60c2af22a 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -332,13 +332,25 @@ class SygusSamplerExt : public SygusSampler void initializeSygusExt(QuantifiersEngine* qe, Node f, unsigned nsamples); /** register term n with this sampler database * - * This returns a term ret with the same guarantees as - * SygusSampler::registerTerm, with the additional guarantee + * This returns either null, or a term ret with the same guarantees as + * SygusSampler::registerTerm with the additional guarantee * that for all ret' returned by a previous call to registerTerm( n' ), - * we have that ret = n is not alpha-equivalent to ret' = n, - * modulo symmetry of equality. For example, + * we have that n = ret is not alpha-equivalent to n' = ret' + * modulo symmetry of equality, nor is n = ret derivable from the set of + * all previous input/output pairs based on the d_drewrite utility. + * For example, * (t+0), t and (s+0), s - * will not be input/output pairs of this function. + * will not both be input/output pairs of this function since t+0=t is + * alpha-equivalent to s+0=s. + * s, t and s+0, t+0 + * will not both be input/output pairs of this function since s+0=t+0 is + * derivable from s=t. + * + * If this function returns null, then n is equivalent to a previously + * registered term ret, and the equality n = ret is either alpha-equivalent + * to a previous input/output pair n' = ret', or n = ret is derivable + * from the set of all previous input/output pairs based on the + * d_drewrite utility. */ virtual Node registerTerm(Node n, bool forceKeep = false) override; -- 2.30.2