diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-20 14:45:26 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-20 14:45:26 -0500 |
commit | 549060790c9e91d9fc37b882e137bb36e5b538ea (patch) | |
tree | 146d966b1188d3e134b1bb700ab6a08262fb07e0 /src/theory/quantifiers/sygus_sampler.cpp | |
parent | 5f1cdd91a5e03dd29b660c841032d5b2a31ea634 (diff) |
Reenable filtering based on ordering in sygus sampler (#1784)
Diffstat (limited to 'src/theory/quantifiers/sygus_sampler.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus_sampler.cpp | 113 |
1 files changed, 86 insertions, 27 deletions
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<TypeNode, unsigned>::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<Node> fvs; computeFreeVariables(a, fvs); + std::vector<Node> fv_found; std::unordered_set<TNode, TNodeHashFunction> visited; std::unordered_set<TNode, TNodeHashFunction>::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<DynamicRewriter>(new DynamicRewriter(ss.str(), qe)); + if (options::sygusRewSynthFilterCong()) + { + d_drewrite = + std::unique_ptr<DynamicRewriter>(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); } } |