From 093d5ffdfa5c1656309da6b9cbdfbbf28574a8a0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 12 Mar 2019 15:18:30 -0500 Subject: [PATCH] Add option --sygus-rr-synth-rec for considering all grammar types recursively (#2270) --- src/options/quantifiers_options.toml | 12 ++++- .../candidate_rewrite_database.cpp | 31 +++++++++++-- .../quantifiers/candidate_rewrite_database.h | 18 ++++++-- .../quantifiers/candidate_rewrite_filter.cpp | 14 +++++- .../quantifiers/candidate_rewrite_filter.h | 6 ++- src/theory/quantifiers/expr_miner_manager.cpp | 4 +- src/theory/quantifiers/sygus_sampler.cpp | 44 +++++++++---------- src/theory/quantifiers/sygus_sampler.h | 29 +++++++++--- 8 files changed, 116 insertions(+), 42 deletions(-) diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index d9d3e0d38..4deb5565d 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1240,7 +1240,7 @@ header = "options/quantifiers_options.h" type = "bool" default = "false" read_only = true - help = "use sygus to enumerate and verify correctness of rewrite rules via sampling" + help = "use sygus to enumerate and verify correctness of rewrite rules" [[option]] name = "sygusRewSynth" @@ -1248,7 +1248,7 @@ header = "options/quantifiers_options.h" long = "sygus-rr-synth" type = "bool" default = "false" - help = "use sygus to enumerate candidate rewrite rules via sampling" + help = "use sygus to enumerate candidate rewrite rules" [[option]] name = "sygusRewSynthFilterOrder" @@ -1369,6 +1369,14 @@ header = "options/quantifiers_options.h" long = "sygus-expr-miner-check-timeout=N" type = "unsigned long" help = "timeout (in milliseconds) for satisfiability checks in expression miners" + +[[option]] + name = "sygusRewSynthRec" + category = "regular" + long = "sygus-rr-synth-rec" + type = "bool" + default = "false" + help = "synthesize rewrite rules over all sygus grammar types recursively" [[option]] name = "sygusQueryGen" diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 2d2e9ce30..3e613cde5 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -69,9 +69,29 @@ void CandidateRewriteDatabase::initializeSygus(const std::vector& vars, } bool CandidateRewriteDatabase::addTerm(Node sol, + bool rec, std::ostream& out, bool& rew_print) { + // have we added this term before? + std::unordered_map::iterator itac = + d_add_term_cache.find(sol); + if (itac != d_add_term_cache.end()) + { + return itac->second; + } + + if (rec) + { + // if recursive, we first add all subterms + for (const Node& solc : sol) + { + // whether a candidate rewrite is printed for any subterm is irrelevant + bool rew_printc = false; + addTerm(solc, rec, out, rew_printc); + } + } + // register the term bool is_unique_term = true; Node eq_sol = d_sampler->registerTerm(sol); // eq_sol is a candidate solution that is equivalent to sol @@ -252,13 +272,18 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // it discards it as a redundant candidate rewrite rule before // checking its correctness. } + d_add_term_cache[sol] = is_unique_term; return is_unique_term; } -bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) +bool CandidateRewriteDatabase::addTerm(Node sol, bool rec, std::ostream& out) { bool rew_print = false; - return addTerm(sol, out, rew_print); + return addTerm(sol, rec, out, rew_print); +} +bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) +{ + return addTerm(sol, false, out); } void CandidateRewriteDatabase::setSilent(bool flag) { d_silent = flag; } @@ -298,7 +323,7 @@ bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out) Trace("synth-rr-dbg") << "...finish." << std::endl; } Trace("synth-rr-dbg") << "Add term " << nr << " for " << tn << std::endl; - return itc->second.addTerm(nr, out); + return itc->second.addTerm(nr, false, out); } } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 5b8ffbd94..3fa9d989a 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -71,9 +71,13 @@ class CandidateRewriteDatabase : public ExprMiner * cause a candidate-rewrite to be printed on the output stream out. * We return true if the term sol is distinct (up to equivalence) with * all previous terms added to this class. The argument rew_print is set to - * true if this class printed a rewrite. + * true if this class printed a rewrite involving sol. + * + * If the flag rec is true, then we also recursively add all subterms of sol + * to this class as well. */ - bool addTerm(Node sol, std::ostream& out, bool& rew_print); + bool addTerm(Node sol, bool rec, std::ostream& out, bool& rew_print); + bool addTerm(Node sol, bool rec, std::ostream& out); bool addTerm(Node sol, std::ostream& out) override; /** sets whether this class should output candidate rewrites it finds */ void setSilent(bool flag); @@ -93,6 +97,13 @@ class CandidateRewriteDatabase : public ExprMiner bool d_using_sygus; /** candidate rewrite filter */ CandidateRewriteFilter d_crewrite_filter; + /** + * Cache of skolems for each free variable that appears in a synthesis check + * (for --sygus-rr-synth-check). + */ + std::map d_fv_to_skolem; + /** the cache for results of addTerm */ + std::unordered_map d_add_term_cache; /** if true, we silence the output of candidate rewrites */ bool d_silent; }; @@ -115,7 +126,8 @@ class CandidateRewriteDatabaseGen * This registers term n with this class. We generate the candidate rewrite * database of the appropriate type (if not allocated already), and register * n with this database. This may result in "candidate-rewrite" being - * printed on the output stream out. + * printed on the output stream out. We return true if the term sol is + * distinct (up to equivalence) with all previous terms added to this class. */ bool addTerm(Node n, std::ostream& out); diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index 0d3878149..2638872fb 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -290,6 +290,12 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) // ----- check rewriting redundancy if (keep && options::sygusRewSynthFilterCong()) { + // When using sygus types, this filtering applies to the builtin versions + // of n and eq_n. This means that we may filter out a rewrite rule for one + // sygus type based on another, e.g. we won't report x=x+0 for both A and B + // in: + // A -> x | 0 | A+A + // B -> x | 0 | B+B Trace("cr-filter-debug") << "Check equal rewrite pair..." << std::endl; if (d_drewrite->areEqual(bn, beq_n)) { @@ -309,7 +315,9 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) Node bni = d_drewrite->toInternal(bn); if (!bni.isNull()) { - if (!d_match_trie.getMatches(bni, &d_ssenm)) + // as with congruence filtering, we cache based on the builtin type + TypeNode tn = bn.getType(); + if (!d_match_trie[tn].getMatches(bni, &d_ssenm)) { keep = false; Trace("cr-filter") << "...redundant (matchable)" << std::endl; @@ -357,6 +365,8 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n) } if (options::sygusRewSynthFilterMatch()) { + // cache based on the builtin type + TypeNode tn = bn.getType(); // add to match information for (unsigned r = 0; r < 2; r++) { @@ -369,7 +379,7 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n) Node ti = d_drewrite->toInternal(t); if (!ti.isNull()) { - d_match_trie.addTerm(ti); + d_match_trie[tn].addTerm(ti); } } d_pairs[t].insert(to); diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h index ca071faa4..f8ebe298f 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -165,14 +165,16 @@ class CandidateRewriteFilter * detail, if (t,s) is a relevant pair, then t in d_pairs[s]. */ std::map > d_pairs; - /** Match trie storing all terms in the domain of d_pairs. + /** + * For each (builtin) type, a match trie storing all terms in the domain of + * d_pairs. * * Notice that we store d_drewrite->toInternal(t) instead of t, for each * term t, so that polymorphism is handled properly. In particular, this * prevents matches between terms select( x, y ) and select( z, y ) where * the type of x and z are different. */ - MatchTrie d_match_trie; + std::map d_match_trie; /** Notify class */ class CandidateRewriteFilterNotifyMatch : public NotifyMatch { diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index a808d386c..4de95e3a1 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -15,6 +15,8 @@ #include "theory/quantifiers/expr_miner_manager.h" #include "theory/quantifiers_engine.h" +#include "options/quantifiers_options.h" + namespace CVC4 { namespace theory { namespace quantifiers { @@ -140,7 +142,7 @@ bool ExpressionMinerManager::addTerm(Node sol, bool ret = true; if (d_doRewSynth) { - ret = d_crd.addTerm(sol, out, rew_print); + ret = d_crd.addTerm(sol, options::sygusRewSynthRec(), out, rew_print); } // a unique term, let's try the query generator diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 8834fe751..27ca270cc 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -40,7 +40,6 @@ void SygusSampler::initialize(TypeNode tn, d_tds = nullptr; d_use_sygus_type = false; d_is_valid = true; - d_tn = tn; d_ftn = TypeNode::null(); d_type_vars.clear(); d_vars.clear(); @@ -95,7 +94,6 @@ void SygusSampler::initializeSygus(TermDbSygus* tds, Assert(d_ftn.isDatatype()); const Datatype& dt = static_cast(d_ftn.toType()).getDatatype(); Assert(dt.isSygus()); - d_tn = TypeNode::fromType(dt.getSygusType()); Trace("sygus-sample") << "Register sampler for " << f << std::endl; @@ -264,28 +262,30 @@ bool SygusSampler::PtTrie::add(std::vector& pt) Node SygusSampler::registerTerm(Node n, bool forceKeep) { - if (d_is_valid) + if (!d_is_valid) { - Node bn = n; - // if this is a sygus type, get its builtin analog - if (d_use_sygus_type) - { - Assert(!d_ftn.isNull()); - bn = d_tds->sygusToBuiltin(n); - Assert(d_builtin_to_sygus.find(bn) == d_builtin_to_sygus.end() - || d_builtin_to_sygus[bn] == n); - d_builtin_to_sygus[bn] = n; - } - Assert(bn.getType() == d_tn); - Node res = d_trie.add(bn, this, 0, d_samples.size(), forceKeep); - if (d_use_sygus_type) - { - Assert(d_builtin_to_sygus.find(res) != d_builtin_to_sygus.end()); - res = res != bn ? d_builtin_to_sygus[res] : n; - } - return res; + // do nothing + return n; + } + Node bn = n; + TypeNode tn = n.getType(); + // If we are using sygus types, get the builtin analog of n. + if (d_use_sygus_type) + { + bn = d_tds->sygusToBuiltin(n); + d_builtin_to_sygus[tn][bn] = n; + } + // cache based on the (original) type of n + Node res = d_trie[tn].add(bn, this, 0, d_samples.size(), forceKeep); + // If we are using sygus types, map back to an original. + // Notice that d_builtin_to_sygus is not necessarily bijective. + if (d_use_sygus_type) + { + std::map& bts = d_builtin_to_sygus[tn]; + Assert(bts.find(res) != bts.end()); + res = res != bn ? bts[res] : n; } - return n; + return res; } bool SygusSampler::isContiguous(Node n) diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 98f52992b..526a9e4b1 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -188,14 +188,15 @@ class SygusSampler : public LazyTrieEvaluator }; /** a trie for samples */ PtTrie d_samples_trie; - /** type of nodes we will be registering with this class */ - TypeNode d_tn; /** the sygus type for this sampler (if applicable). */ TypeNode d_ftn; - /** whether we are registering terms of type d_ftn */ + /** whether we are registering terms of sygus types with this sampler */ bool d_use_sygus_type; - /** map from builtin terms to the sygus term they correspond to */ - std::map d_builtin_to_sygus; + /** + * For each (sygus) type, a map from builtin terms to the sygus term they + * correspond to. + */ + std::map > d_builtin_to_sygus; /** all variables we are sampling values for */ std::vector d_vars; /** type variables @@ -229,8 +230,22 @@ class SygusSampler : public LazyTrieEvaluator * that type. */ std::map > d_type_consts; - /** the lazy trie */ - LazyTrie d_trie; + /** a lazy trie for each type + * + * This stores the evaluation of all terms registered to this class. + * + * Notice if we are registering sygus terms with this class, then terms + * are grouped into this trie according to their sygus type, and not their + * builtin type. For example, for grammar: + * A -> x | B+1 + * B -> x | 0 | 1 | B+B + * If we register C^B_+( C^B_x(), C^B_0() ) and C^A_x() with this class, + * then x+0 is registered to d_trie[B] and x is registered to d_trie[A], + * and no rewrite rule is reported. The reason for this is that otherwise + * we would end up reporting many useless rewrites since the same builtin + * term can be generated by multiple sygus types (e.g. C^B_x() and C^A_x()). + */ + std::map d_trie; /** is this sampler valid? * * A sampler can be invalid if sample points cannot be generated for a type -- 2.30.2