From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 31 Jan 2020 19:42:36 +0000 (-0600)
Subject: Allow PBE symmetry breaking with sygus stream (#3686)
X-Git-Tag: cvc5-1.0.0~3698
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c099abeb9c3a45019b18daac19c4b4cd43b4c6f0;p=cvc5.git

Allow PBE symmetry breaking with sygus stream (#3686)
---

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 95ec636ca..908846bea 100644
--- 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 d10678bf6..83d8fb612 100644
--- 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())
       {