Add option --sygus-rr-synth-rec for considering all grammar types recursively (#2270)

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<Node>& vars,
 }
 
 bool CandidateRewriteDatabase::addTerm(Node sol,
+                                       bool rec,
                                        std::ostream& out,
                                        bool& rew_print)
 {
+  // have we added this term before?
+  std::unordered_map<Node, bool, NodeHashFunction>::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<Node, Node> d_fv_to_skolem;
+  /** the cache for results of addTerm */
+  std::unordered_map<Node, bool, NodeHashFunction> 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<Node, std::unordered_set<Node, NodeHashFunction> > 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<TypeNode, MatchTrie> 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<DatatypeType>(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<Node>& 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<Node, Node>& 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<Node, Node> d_builtin_to_sygus;
+  /**
+   * For each (sygus) type, a map from builtin terms to the sygus term they
+   * correspond to.
+   */
+  std::map<TypeNode, std::map<Node, Node> > d_builtin_to_sygus;
   /** all variables we are sampling values for */
   std::vector<Node> d_vars;
   /** type variables
@@ -229,8 +230,22 @@ class SygusSampler : public LazyTrieEvaluator
    * that type.
    */
   std::map<TypeNode, std::vector<Node> > 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<TypeNode, LazyTrie> d_trie;
   /** is this sampler valid?
    *
    * A sampler can be invalid if sample points cannot be generated for a type