Allow PBE symmetry breaking with sygus stream (#3686)

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 95ec636cad73f10e3037cd4bb8defff88b8ea77f..908846bea22b62256d5a1e7094370e15282931f8 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1138,7 +1138,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-unif-pi=MODE"
   type       = "SygusUnifPiMode"
   default    = "NONE"
-  read_only  = true
   help       = "mode for synthesis via piecewise-indepedent unification"
   help_mode  = "Modes for piecewise-independent unification."
 [[option.mode.NONE]]

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d10678bf653cfc615b4fbd36d913547d8aafd246..83d8fb612250e6c105d8e56132a3fad96b46fd6b 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2003,8 +2003,9 @@ void SmtEngine::setDefaults() {
     }
     // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
     // is one that is specialized for returning a single solution. Non-basic
-    // sygus algorithms currently include the PBE solver, static template
-    // inference for invariant synthesis, and single invocation techniques.
+    // sygus algorithms currently include the PBE solver, UNIF+PI, static
+    // template inference for invariant synthesis, and single invocation
+    // techniques.
     bool reqBasicSygus = false;
     if (options::produceAbducts())
     {
@@ -2035,11 +2036,10 @@ void SmtEngine::setDefaults() {
       if (!options::sygusUnifPbe.wasSetByUser())
       {
         options::sygusUnifPbe.set(false);
-        // also disable PBE-specific symmetry breaking unless PBE was enabled
-        if (!options::sygusSymBreakPbe.wasSetByUser())
-        {
-          options::sygusSymBreakPbe.set(false);
-        }
+      }
+      if (options::sygusUnifPi.wasSetByUser())
+      {
+        options::sygusUnifPi.set(options::SygusUnifPiMode::NONE);
       }
       if (!options::sygusInvTemplMode.wasSetByUser())
       {