From 549060790c9e91d9fc37b882e137bb36e5b538ea Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 20 Apr 2018 14:45:26 -0500 Subject: [PATCH] Reenable filtering based on ordering in sygus sampler (#1784) --- src/options/quantifiers_options.toml | 22 +++- .../sygus/ce_guided_conjecture.cpp | 10 +- src/theory/quantifiers/sygus_sampler.cpp | 113 +++++++++++++----- src/theory/quantifiers/sygus_sampler.h | 7 +- 4 files changed, 118 insertions(+), 34 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 4a098f9fc..b8ddd6d31 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1132,12 +1132,28 @@ header = "options/quantifiers_options.h" help = "use sygus to enumerate candidate rewrite rules via sampling" [[option]] - name = "sygusRewSynthFilter" + name = "sygusRewSynthFilterOrder" category = "regular" - long = "sygus-rr-synth-filter" + long = "sygus-rr-synth-filter-order" type = "bool" default = "true" - help = "filter candidate rewrites based on techniques like matching" + help = "filter candidate rewrites based on variable ordering" + +[[option]] + name = "sygusRewSynthFilterMatch" + category = "regular" + long = "sygus-rr-synth-filter-match" + type = "bool" + default = "true" + help = "filter candidate rewrites based on matching" + +[[option]] + name = "sygusRewSynthFilterCong" + category = "regular" + long = "sygus-rr-synth-filter-cong" + type = "bool" + default = "true" + help = "filter candidate rewrites based on congruence" [[option]] name = "sygusRewVerify" diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 1e0f72817..ca1f92d89 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -748,7 +748,15 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation } } } - // we count this as a rewrite if we did not explicitly rule it out + // We count this as a rewrite if we did not explicitly rule it out. + // Notice that when --sygus-rr-synth-check is enabled, + // statistics on number of candidate rewrite rules is + // an accurate count of (#enumerated_terms-#unique_terms) only if + // the option sygus-rr-synth-filter-order is disabled. The reason + // is that the sygus sampler may reason that a candidate rewrite + // rule is not useful since its variables are unordered, whereby + // it discards it as a redundant candidate rewrite rule before + // checking its correctness. if (success) { ++(cei->d_statistics.d_candidate_rewrites); diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index f15c1199c..18e13fd59 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -91,7 +91,7 @@ void SygusSampler::initialize(TypeNode tn, for (const Node& sv : d_vars) { TypeNode svt = sv.getType(); - unsigned tnid; + unsigned tnid = 0; std::map::iterator itt = type_to_type_id.find(svt); if (itt == type_to_type_id.end()) { @@ -408,11 +408,12 @@ bool SygusSampler::isOrdered(Node n) return true; } -bool SygusSampler::containsFreeVariables(Node a, Node b) +bool SygusSampler::containsFreeVariables(Node a, Node b, bool strict) { // compute free variables in a std::vector fvs; computeFreeVariables(a, fvs); + std::vector fv_found; std::unordered_set visited; std::unordered_set::iterator it; @@ -432,6 +433,17 @@ bool SygusSampler::containsFreeVariables(Node a, Node b) { return false; } + else if (strict) + { + if (fv_found.size() + 1 == fvs.size()) + { + return false; + } + // cur should only be visited once + Assert(std::find(fv_found.begin(), fv_found.end(), cur) + == fv_found.end()); + fv_found.push_back(cur); + } } for (const Node& cn : cur) { @@ -693,8 +705,11 @@ void SygusSamplerExt::initializeSygusExt(QuantifiersEngine* qe, // initialize the dynamic rewriter std::stringstream ss; ss << f; - d_drewrite = - std::unique_ptr(new DynamicRewriter(ss.str(), qe)); + if (options::sygusRewSynthFilterCong()) + { + d_drewrite = + std::unique_ptr(new DynamicRewriter(ss.str(), qe)); + } d_pairs.clear(); d_match_trie.clear(); } @@ -707,8 +722,6 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) // this is a unique term return n; } - Trace("sygus-synth-rr") << "sygusSampleExt : " << n << "..." << eq_n - << std::endl; Node bn = n; Node beq_n = eq_n; if (d_use_sygus_type) @@ -716,27 +729,55 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) bn = d_tds->sygusToBuiltin(n); beq_n = d_tds->sygusToBuiltin(eq_n); } + Trace("sygus-synth-rr") << "sygusSampleExt : " << bn << "..." << beq_n + << std::endl; // whether we will keep this pair bool keep = true; - if( options::sygusRewSynthFilter() ) + // ----- check ordering redundancy + if (options::sygusRewSynthFilterOrder()) { - // ----- check matchable - // check whether the pair is matchable with a previous one - d_curr_pair_rhs = beq_n; - Trace("sse-match") << "SSE check matches : " << n << " [rhs = " << eq_n - << "]..." << std::endl; - if (!d_match_trie.getMatches(bn, &d_ssenm)) + bool nor = isOrdered(bn); + bool eqor = isOrdered(beq_n); + Trace("sygus-synth-rr-debug") << "Ordered? : " << nor << " " << eqor + << std::endl; + if (eqor || nor) + { + // if only one is ordered, then we require that the ordered one's + // variables cannot be a strict subset of the variables of the other. + if (!eqor) + { + if (containsFreeVariables(beq_n, bn, true)) + { + keep = false; + } + else + { + // if the previous value stored was unordered, but n is + // ordered, we prefer n. Thus, we force its addition to the + // sampler database. + SygusSampler::registerTerm(n, true); + } + } + else if (!nor) + { + keep = !containsFreeVariables(bn, beq_n, true); + } + } + else { keep = false; - Trace("sygus-synth-rr") << "...redundant (matchable)" << std::endl; + } + if (!keep) + { + Trace("sygus-synth-rr") << "...redundant (unordered)" << std::endl; } } // ----- check rewriting redundancy - if (d_drewrite != nullptr) + if (keep && d_drewrite != nullptr) { - Trace("sygus-synth-rr-debug") << "Add rewrite pair..." << std::endl; + Trace("sygus-synth-rr-debug") << "Check equal rewrite pair..." << std::endl; if (d_drewrite->areEqual(bn, beq_n)) { // must be unique according to the dynamic rewriter @@ -745,12 +786,26 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) } } + if (options::sygusRewSynthFilterMatch()) + { + // ----- check matchable + // check whether the pair is matchable with a previous one + d_curr_pair_rhs = beq_n; + Trace("sse-match") << "SSE check matches : " << bn << " [rhs = " << beq_n + << "]..." << std::endl; + if (!d_match_trie.getMatches(bn, &d_ssenm)) + { + keep = false; + Trace("sygus-synth-rr") << "...redundant (matchable)" << std::endl; + // regardless, would help to remember it + registerRelevantPair(n, eq_n); + } + } + if (keep) { return eq_n; } - Trace("sygus-synth-rr") << "Redundant pair : " << eq_n << " " << n; - Trace("sygus-synth-rr") << std::endl; if (Trace.isOn("sygus-rr-filter")) { Printer* p = Printer::getPrinter(options::outputLanguage()); @@ -759,6 +814,7 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep) p->toStreamSygus(ss, n); ss << " "; p->toStreamSygus(ss, eq_n); + ss << ")"; Trace("sygus-rr-filter") << ss.str() << std::endl; } return Node::null(); @@ -780,18 +836,21 @@ void SygusSamplerExt::registerRelevantPair(Node n, Node eq_n) Assert(!d_drewrite->areEqual(bn, beq_n)); d_drewrite->addRewrite(bn, beq_n); } - // add to match information - for (unsigned r = 0; r < 2; r++) + if (options::sygusRewSynthFilterMatch()) { - Node t = r == 0 ? bn : beq_n; - Node to = r == 0 ? beq_n : bn; - // insert in match trie if first time - if (d_pairs.find(t) == d_pairs.end()) + // add to match information + for (unsigned r = 0; r < 2; r++) { - Trace("sse-match") << "SSE add term : " << t << std::endl; - d_match_trie.addTerm(t); + Node t = r == 0 ? bn : beq_n; + Node to = r == 0 ? beq_n : bn; + // insert in match trie if first time + if (d_pairs.find(t) == d_pairs.end()) + { + Trace("sse-match") << "SSE add term : " << t << std::endl; + d_match_trie.addTerm(t); + } + d_pairs[t].insert(to); } - d_pairs[t].insert(to); } } diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 18b8f5511..a66e7ee21 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -207,10 +207,11 @@ class SygusSampler : public LazyTrieEvaluator bool isOrdered(Node n); /** contains free variables * - * Returns true if all free variables of a are contained in b. Free variables - * are those that occur in the range d_type_vars. + * Returns true if the free variables of b are a subset of those in a, where + * we require a strict subset if strict is true. Free variables are those that + * occur in the range d_type_vars. */ - bool containsFreeVariables(Node a, Node b); + bool containsFreeVariables(Node a, Node b, bool strict = false); protected: /** sygus term database of d_qe */ -- 2.30.2