Reenable filtering based on ordering in sygus sampler (#1784)

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<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);
   }
 }
 
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 */