From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 8 Oct 2018 20:00:23 +0000 (-0500)
Subject:  Disable extended rewriter when applicable with var agnostic enumeration (#2594)
X-Git-Tag: cvc5-1.0.0~4451
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=697c624dec0c292beb0ecb9aae0b01ba54c89473;p=cvc5.git

 Disable extended rewriter when applicable with var agnostic enumeration (#2594)
---

diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index bf939e0fe..24770ade0 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -16,6 +16,7 @@
 #include "theory/quantifiers/sygus/enum_stream_substitution.h"
 
 #include "options/base_options.h"
+#include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -187,10 +188,14 @@ Node EnumStreamPermutation::getNext()
     bultin_perm_value = d_tds->sygusToBuiltin(perm_value, perm_value.getType());
     Trace("synth-stream-concrete-debug")
         << " ......perm builtin is " << bultin_perm_value;
-    bultin_perm_value =
-        d_tds->getExtRewriter()->extendedRewrite(bultin_perm_value);
-    Trace("synth-stream-concrete-debug")
-        << " and rewrites to " << bultin_perm_value << "\n";
+    if (options::sygusSymBreakDynamic())
+    {
+      bultin_perm_value =
+          d_tds->getExtRewriter()->extendedRewrite(bultin_perm_value);
+      Trace("synth-stream-concrete-debug")
+          << " and rewrites to " << bultin_perm_value;
+    }
+    Trace("synth-stream-concrete-debug") << "\n";
     // if permuted value is equivalent modulo rewriting to a previous one, look
     // for another
   } while (!d_perm_values.insert(bultin_perm_value).second);
@@ -504,8 +509,13 @@ Node EnumStreamSubstitution::getNext()
       domain_sub.begin(), domain_sub.end(), range_sub.begin(), range_sub.end());
   // the new combination value should be fresh, modulo rewriting, by
   // construction (unless it's equiv to a constant, e.g. true / false)
-  Node builtin_comb_value = d_tds->getExtRewriter()->extendedRewrite(
-      d_tds->sygusToBuiltin(comb_value, comb_value.getType()));
+  Node builtin_comb_value =
+      d_tds->sygusToBuiltin(comb_value, comb_value.getType());
+  if (options::sygusSymBreakDynamic())
+  {
+    builtin_comb_value =
+        d_tds->getExtRewriter()->extendedRewrite(builtin_comb_value);
+  }
   if (Trace.isOn("synth-stream-concrete"))
   {
     std::stringstream ss;