From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 27 Mar 2018 19:37:01 +0000 (-0500)
Subject: Fix for --sygus-rr-synth (#1723)
X-Git-Tag: cvc5-1.0.0~5199
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d8c56098916be16ba80c79933c2e6fc7850024b7;p=cvc5.git

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

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index ad05aa5cd..28a9e58a7 100644
--- 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 99494657f..f9ae0b553 100644
--- 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()))