Refactor options related to rewriting and symmetry breaking in sygus (#7949)

Note this also corrects a few inconsistencies in how the rewriter is invoked in fast / variable agnostic enumeration.

Notably, fast enumeration now leverages the term datatype sygus for rewriting, meaning it can evaluate recursive functions for enumerated terms.

diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 60cdcc3358d81670f885793953470e4507c5edf5..0bb0edba6639f781225121867791a7f299913e14 100644 (file)
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -86,28 +86,40 @@ name   = "Datatypes Theory"
   help       = "internally use shared selectors across multiple constructors"
 
 [[option]]
-  name       = "sygusSymBreak"
+  name       = "sygusSimpleSymBreak"
   category   = "regular"
-  long       = "sygus-sym-break"
-  type       = "bool"
-  default    = "true"
-  help       = "simple sygus symmetry breaking lemmas"
-
-[[option]]
-  name       = "sygusSymBreakAgg"
-  category   = "regular"
-  long       = "sygus-sym-break-agg"
-  type       = "bool"
-  default    = "true"
-  help       = "use aggressive checks for simple sygus symmetry breaking lemmas"
-
-[[option]]
-  name       = "sygusSymBreakDynamic"
-  category   = "regular"
-  long       = "sygus-sym-break-dynamic"
-  type       = "bool"
-  default    = "true"
-  help       = "dynamic sygus symmetry breaking lemmas"
+  long       = "sygus-simple-sym-break=MODE"
+  type       = "SygusSimpleSymBreakMode"
+  default    = "AGG"
+  help       = "if and how to apply simple symmetry breaking based on the grammar for smart enumeration"
+  help_mode  = "Modes for applying simple symmetry breaking based on the grammar for smart enumeration."
+[[option.mode.NONE]]
+  name = "none"
+  help = "Do not apply simple symmetry breaking."
+[[option.mode.BASIC]]
+  name = "basic"
+  help = "Apply basic simple symmetry breaking."
+[[option.mode.AGG]]
+  name = "agg"
+  help = "Apply aggressive simple symmetry breaking."
+  
+[[option]]
+  name       = "sygusRewriter"
+  category   = "regular"
+  long       = "sygus-rewriter=MODE"
+  type       = "SygusRewriterMode"
+  default    = "EXTENDED"
+  help       = "if and how to apply rewriting for sygus symmetry breaking"
+  help_mode  = "Modes for applying rewriting for sygus symmetry breaking."
+[[option.mode.NONE]]
+  name = "none"
+  help = "Do not use the rewriter."
+[[option.mode.BASIC]]
+  name = "basic"
+  help = "Use the basic rewriter."
+[[option.mode.EXTENDED]]
+  name = "extended"
+  help = "Use the extended rewriter."
 
 [[option]]
   name       = "sygusSymBreakPbe"

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index c284518c719803b1c65b6f62e2e5a9f3d8ec5f3a..312fc606b7be92de99c6e04d584953c439686349 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1260,14 +1260,6 @@ name   = "Quantifiers"
   default    = "false"
   help       = "enumerate a stream of solutions instead of terminating after the first one"
 
-[[option]]
-  name       = "sygusExtRew"
-  category   = "regular"
-  long       = "sygus-ext-rew"
-  type       = "bool"
-  default    = "true"
-  help       = "use extended rewriter for sygus"
-
 [[option]]
   name       = "cegisSample"
   category   = "regular"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index fea9d43985d3419209da131933d94eefa8a1a20a..1fd2c3dc5bcb081847b7c04eaa3fc1c06edffbde 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1580,9 +1580,9 @@ void SetDefaults::setDefaultsSygus(Options& opts) const
     opts.quantifiers.sygusRewSynth = true;
     // we should not use the extended rewriter, since we are interested
     // in rewrites that are not in the main rewriter
-    if (!opts.quantifiers.sygusExtRewWasSetByUser)
+    if (!opts.datatypes.sygusRewriterWasSetByUser)
     {
-      opts.quantifiers.sygusExtRew = false;
+      opts.datatypes.sygusRewriter = options::SygusRewriterMode::BASIC;
     }
   }
   // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm

diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 0318f7da943e3ef965753a2506a5beb9ca98bd8c..1134c0a5a12fc46b86bae301d86fdf59d91c27c3 100644 (file)
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -691,7 +691,8 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
 
   // if we are the "any constant" constructor, we do no symmetry breaking
   // only do simple symmetry breaking up to depth 2
-  bool doSymBreak = options().datatypes.sygusSymBreak;
+  bool doSymBreak = options().datatypes.sygusSimpleSymBreak
+                    != options::SygusSimpleSymBreakMode::NONE;
   if (isAnyConstant || depth > 2)
   {
     doSymBreak = false;
@@ -1047,7 +1048,7 @@ Node SygusExtension::registerSearchValue(Node a,
                             << ", type=" << tn << std::endl;
     Node bv = d_tds->sygusToBuiltin(cnv, tn);
     Trace("sygus-sb-debug") << "  ......builtin is " << bv << std::endl;
-    Node bvr = extendedRewrite(bv);
+    Node bvr = d_tds->rewriteNode(bv);
     Trace("sygus-sb-debug") << "  ......search value rewrites to " << bvr << std::endl;
     Trace("dt-sygus") << "  * DT builtin : " << n << " -> " << bvr << std::endl;
     unsigned sz = utils::getSygusTermSize(nv);
@@ -1624,7 +1625,9 @@ void SygusExtension::check()
 
         // register the search value ( prog -> progv ), this may invoke symmetry
         // breaking
-        if (!isExc && options().datatypes.sygusSymBreakDynamic)
+        if (!isExc
+            && options().datatypes.sygusRewriter
+                   != options::SygusRewriterMode::NONE)
         {
           bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog);
           // check that it is unique up to theory-specific rewriting and

diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 233d7f17b6d9095610f91f82c87a8bfd5848b262..a4b65ab300dafc37468f687f1f6d223eac9374f0 100644 (file)
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -125,7 +125,7 @@ Node EnumStreamPermutation::getNext()
   {
     d_first = false;
     Node bultin_value = d_tds->sygusToBuiltin(d_value, d_value.getType());
-    d_perm_values.insert(extendedRewrite(bultin_value));
+    d_perm_values.insert(d_tds->rewriteNode(bultin_value));
     return d_value;
   }
   unsigned n_classes = d_perm_state_class.size();
@@ -192,9 +192,9 @@ 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;
-    if (options().datatypes.sygusSymBreakDynamic)
+    if (options().datatypes.sygusRewriter != options::SygusRewriterMode::NONE)
     {
-      bultin_perm_value = extendedRewrite(bultin_perm_value);
+      bultin_perm_value = d_tds->rewriteNode(bultin_perm_value);
       Trace("synth-stream-concrete-debug")
           << " and rewrites to " << bultin_perm_value;
     }
@@ -512,9 +512,9 @@ Node EnumStreamSubstitution::getNext()
   // construction (unless it's equiv to a constant, e.g. true / false)
   Node builtin_comb_value =
       d_tds->sygusToBuiltin(comb_value, comb_value.getType());
-  if (options().datatypes.sygusSymBreakDynamic)
+  if (options().datatypes.sygusRewriter != options::SygusRewriterMode::NONE)
   {
-    builtin_comb_value = extendedRewrite(builtin_comb_value);
+    builtin_comb_value = d_tds->rewriteNode(builtin_comb_value);
   }
   if (Trace.isOn("synth-stream-concrete"))
   {

diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp
index fcbe3d42ed865ff17d7b489ce16f7cc775c4403c..d9078bfafb30dc2d816a270f5dc142fbf6cab965 100644 (file)
--- a/src/theory/quantifiers/sygus/enum_value_manager.cpp
+++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp
@@ -100,7 +100,8 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
                || options().quantifiers.sygusEnumMode
                       == options::SygusEnumMode::AUTO);
         // create the enumerator callback
-        if (options().datatypes.sygusSymBreakDynamic)
+        if (options().datatypes.sygusRewriter
+            != options::SygusRewriterMode::NONE)
         {
           std::ostream* out = nullptr;
           if (options().quantifiers.sygusRewVerify)
@@ -112,7 +113,7 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
             out = options().base.out;
           }
           d_secd = std::make_unique<SygusEnumeratorCallbackDefault>(
-              d_env, e, &d_stats, d_eec.get(), d_samplerRrV.get(), out);
+              d_env, e, d_tds, &d_stats, d_eec.get(), d_samplerRrV.get(), out);
         }
         // if sygus repair const is enabled, we enumerate terms with free
         // variables as arguments to any-constant constructors

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 52c1ef4a00a8be3ec39511557d6f3241f2d82b54..ba4496a7b4408139d2319e8491c39e8f02b2f327 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -55,10 +55,11 @@ void SygusEnumerator::initialize(Node e)
   Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl;
   d_enum = e;
   // allocate the default callback
-  if (d_sec == nullptr && options().datatypes.sygusSymBreakDynamic)
+  if (d_sec == nullptr
+      && options().datatypes.sygusRewriter != options::SygusRewriterMode::NONE)
   {
-    d_secd =
-        std::make_unique<SygusEnumeratorCallbackDefault>(d_env, e, d_stats);
+    d_secd = std::make_unique<SygusEnumeratorCallbackDefault>(
+        d_env, e, d_tds, d_stats);
     d_sec = d_secd.get();
   }
   d_etype = d_enum.getType();

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
index bde1fdd67f59fc7a667141cd243576baac7aba41..d16b6d33e862f27078d58b899686fe0620a47da3 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp
@@ -18,6 +18,7 @@
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/example_eval_cache.h"
 #include "theory/quantifiers/sygus/sygus_stats.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/sygus_sampler.h"
 #include "theory/rewriter.h"
 
@@ -27,8 +28,9 @@ namespace quantifiers {
 
 SygusEnumeratorCallback::SygusEnumeratorCallback(Env& env,
                                                  Node e,
+                                                 TermDbSygus* tds,
                                                  SygusStatistics* s)
-    : EnvObj(env), d_enum(e), d_stats(s)
+    : EnvObj(env), d_enum(e), d_tds(tds), d_stats(s)
 {
   d_tn = e.getType();
 }
@@ -36,7 +38,7 @@ SygusEnumeratorCallback::SygusEnumeratorCallback(Env& env,
 bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
 {
   Node bn = datatypes::utils::sygusToBuiltin(n);
-  Node bnr = extendedRewrite(bn);
+  Node bnr = d_tds == nullptr ? extendedRewrite(bn) : d_tds->rewriteNode(bn);
   if (d_stats != nullptr)
   {
     ++(d_stats->d_enumTermsRewrite);
@@ -66,11 +68,12 @@ bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
 SygusEnumeratorCallbackDefault::SygusEnumeratorCallbackDefault(
     Env& env,
     Node e,
+    TermDbSygus* tds,
     SygusStatistics* s,
     ExampleEvalCache* eec,
     SygusSampler* ssrv,
     std::ostream* out)
-    : SygusEnumeratorCallback(env, e, s),
+    : SygusEnumeratorCallback(env, e, tds, s),
       d_eec(eec),
       d_samplerRrV(ssrv),
       d_out(out)

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
index 9b7c3fd98ba9cc57e7b5ccaaed4de09c829ab9fd..a83e1b0718b6fd8b38191c605c9d3c28f639f5b7 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_callback.h
@@ -31,6 +31,7 @@ namespace quantifiers {
 class ExampleEvalCache;
 class SygusStatistics;
 class SygusSampler;
+class TermDbSygus;
 
 /**
  * Base class for callbacks in the fast enumerator. This allows a user to
@@ -40,7 +41,10 @@ class SygusSampler;
 class SygusEnumeratorCallback : protected EnvObj
 {
  public:
-  SygusEnumeratorCallback(Env& env, Node e, SygusStatistics* s = nullptr);
+  SygusEnumeratorCallback(Env& env,
+                          Node e,
+                          TermDbSygus* tds = nullptr,
+                          SygusStatistics* s = nullptr);
   virtual ~SygusEnumeratorCallback() {}
   /**
    * Add term, return true if the term should be considered in the enumeration.
@@ -75,6 +79,8 @@ class SygusEnumeratorCallback : protected EnvObj
   Node d_enum;
   /** The type of enum */
   TypeNode d_tn;
+  /** Term database sygus */
+  TermDbSygus* d_tds;
   /** pointer to the statistics */
   SygusStatistics* d_stats;
 };
@@ -84,6 +90,7 @@ class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback
  public:
   SygusEnumeratorCallbackDefault(Env& env,
                                  Node e,
+                                 TermDbSygus* tds = nullptr,
                                  SygusStatistics* s = nullptr,
                                  ExampleEvalCache* eec = nullptr,
                                  SygusSampler* ssrv = nullptr,

diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 60170ceb4b465bc65f44df0fe5b486c48133cf3b..622aa2a6a88b8a65627a25b93296861a4888d45d 100644 (file)
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -739,7 +739,7 @@ SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn)
 Node TermDbSygus::rewriteNode(Node n) const
 {
   Node res;
-  if (options().quantifiers.sygusExtRew)
+  if (options().datatypes.sygusRewriter == options::SygusRewriterMode::EXTENDED)
   {
     res = extendedRewrite(n);
   }
@@ -855,7 +855,8 @@ bool TermDbSygus::canConstructKind(TypeNode tn,
     }
     return true;
   }
-  if (!options().datatypes.sygusSymBreakAgg)
+  if (options().datatypes.sygusSimpleSymBreak
+      != options::SygusSimpleSymBreakMode::AGG)
   {
     return false;
   }

diff --git a/test/regress/regress1/rr-verify/bool-crci.sy b/test/regress/regress1/rr-verify/bool-crci.sy
index 75837695dadf1c90ab2cb6b73ff827ca11ea7b9a..614a83f2b2d52479866ccf530b486ebc0c580e92 100644 (file)
--- a/test/regress/regress1/rr-verify/bool-crci.sy
+++ b/test/regress/regress1/rr-verify/bool-crci.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --sygus-simple-sym-break=none
 ; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1

diff --git a/test/regress/regress1/rr-verify/bv-term-32.sy b/test/regress/regress1/rr-verify/bv-term-32.sy
index 9dfb19451a87ba103a4cad2236c99c17a0ca9f73..95296463b80f15a933221f597231cbefb6c011e6 100644 (file)
--- a/test/regress/regress1/rr-verify/bv-term-32.sy
+++ b/test/regress/regress1/rr-verify/bv-term-32.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1

diff --git a/test/regress/regress1/rr-verify/bv-term.sy b/test/regress/regress1/rr-verify/bv-term.sy
index 9a11128d7b6fb5ce1f2502a87b3587fb0c39f93d..af954cbb1ade3914f1a2a8d12702866e19b458ab 100644 (file)
--- a/test/regress/regress1/rr-verify/bv-term.sy
+++ b/test/regress/regress1/rr-verify/bv-term.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-simple-sym-break=none
 ; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check
 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite|\(rewrite)'

diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy
index 2970fd0de53bb38726a13efb2c00f3787a613a3b..ad8635ca8851e6a48d6e8c955f1f4747ab6a53ea 100644 (file)
--- a/test/regress/regress1/rr-verify/fp-arith.sy
+++ b/test/regress/regress1/rr-verify/fp-arith.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
 ; EXIT: 1

diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy
index e4b3a0facf50c3770c7cd7e686b692a39768959b..33caed2e919ea9599cce73e988d89833ce2af156 100644 (file)
--- a/test/regress/regress1/rr-verify/fp-bool.sy
+++ b/test/regress/regress1/rr-verify/fp-bool.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
 ; EXIT: 1

diff --git a/test/regress/regress1/rr-verify/string-term.sy b/test/regress/regress1/rr-verify/string-term.sy
index 404719f6cb6521535a7259569ad30411699e9f53..815cb70a508430a91384b299f1f30b5201d74b45 100644 (file)
--- a/test/regress/regress1/rr-verify/string-term.sy
+++ b/test/regress/regress1/rr-verify/string-term.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --sygus-simple-sym-break=none
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1

diff --git a/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2
index a7c8645446aac6bcaaa5d5e03b2c8b3ab49dbcc4..cc0c329cde49111ec589560492e5734fff3f5514 100644 (file)
--- a/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2
+++ b/test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2
@@ -1,6 +1,6 @@
 (set-logic ALL)
 (set-option :sygus-inference true)
-(set-option :sygus-sym-break false)
+(set-option :sygus-simple-sym-break none)
 (set-option :sygus-sym-break-lazy false)
 (set-option :sygus-sym-break-rlv false)
 (set-info :status sat)