Fix for --sygus-rr-synth (#1723)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index ad05aa5cd2044c63281c5ebe442377acdb0fe416..28a9e58a7a8ae621569e6723118e081103f7613e 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1114,6 +1114,14 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "use sygus to enumerate candidate rewrite rules via sampling"
 
+[[option]]
+  name       = "sygusRewSynthFilter"
+  category   = "regular"
+  long       = "sygus-rr-synth-filter"
+  type       = "bool"
+  default    = "true"
+  help       = "filter candidate rewrites based on techniques like matching"
+
 [[option]]
   name       = "sygusRewVerify"
   category   = "regular"

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 99494657f2e1210a0256978887acfc4aad2e2784..f9ae0b553dd34957fa932cf53363fb8f38d544c5 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -717,15 +717,18 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
   // whether we will keep this pair
   bool keep = true;
 
-  // ----- 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))
+  if( options::sygusRewSynthFilter() )
   {
-    keep = false;
-    Trace("sygus-synth-rr-debug") << "...redundant (matchable)" << std::endl;
+    // ----- 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))
+    {
+      keep = false;
+      Trace("sygus-synth-rr-debug") << "...redundant (matchable)" << std::endl;
+    }
   }
 
   // ----- check rewriting redundancy
@@ -884,6 +887,7 @@ bool MatchTrie::getMatches(Node n, NotifyMatch* ntm)
           smap.erase(vars.back());
           vars.pop_back();
           subs.pop_back();
+          visit_bound_var[index] = false;
         }
 
         if (vindex == static_cast<int>(curr->d_vars.size()))