Better option names for PBE (#1891)

6 files changed, 26 insertions, 18 deletions

diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index ef736e913..8d6f0baf3 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -113,6 +113,14 @@ header = "options/datatypes_options.h"
   help       = "dynamic sygus sym break lemmas"
 
 [[option]]
+  name       = "sygusSymBreakPbe"
+  category   = "regular"
+  long       = "sygus-sym-break-pbe"
+  type       = "bool"
+  default    = "true"
+  help       = "sygus sym break lemmas based on pbe conjectures"
+  
+[[option]]
   name       = "sygusOpt1"
   category   = "regular"
   long       = "sygus-opt1"
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 2f911bdd1..4c771c143 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -960,14 +960,6 @@ header = "options/quantifiers_options.h"
   help       = "abort if synthesis conjecture is not single invocation"
 
 [[option]]
-  name       = "sygusPbe"
-  category   = "regular"
-  long       = "sygus-pbe"
-  type       = "bool"
-  default    = "true"
-  help       = "sygus advanced pruning based on examples"
-
-[[option]]
   name       = "sygusUnif"
   category   = "regular"
   long       = "sygus-unif"
@@ -1050,13 +1042,12 @@ header = "options/quantifiers_options.h"
   help       = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems"
 
 [[option]]
-  name       = "sygusUnifCondSol"
+  name       = "sygusUnifPbe"
   category   = "regular"
-  long       = "sygus-unif-csol"
+  long       = "sygus-pbe"
   type       = "bool"
   default    = "true"
-  read_only  = true
-  help       = "enable new approach which unifies conditional solutions"
+  help       = "enable approach which unifies conditional solutions, specialized for programming-by-examples (pbe) conjectures"
 
 [[option]]
   name       = "sygusDirectEval"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c750b8a12..aeec5298a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1949,9 +1949,13 @@ void SmtEngine::setDefaults() {
     if (options::sygusStream())
     {
       // PBE and streaming modes are incompatible
-      if (!options::sygusPbe.wasSetByUser())
+      if (!options::sygusSymBreakPbe.wasSetByUser())
       {
-        options::sygusPbe.set(false);
+        options::sygusSymBreakPbe.set(false);
+      }
+      if (!options::sygusUnifPbe.wasSetByUser())
+      {
+        options::sygusUnifPbe.set(false);
       }
     }
     //do not allow partial functions
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 6f660642e..757f4d040 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -662,8 +662,12 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
         // class
         // is it equivalent under examples?
         Node bvr_equiv;
-        if (aconj->getPbe()->hasExamples(a)) {
-          bvr_equiv = aconj->getPbe()->addSearchVal(tn, a, bvr);
+        if (options::sygusSymBreakPbe())
+        {
+          if (aconj->getPbe()->hasExamples(a))
+          {
+            bvr_equiv = aconj->getPbe()->addSearchVal(tn, a, bvr);
+          }
         }
         if( !bvr_equiv.isNull() ){
           if( bvr_equiv!=bvr ){
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index d5a430229..69cf7f73b 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -16,6 +16,7 @@
 
 #include "expr/datatype.h"
 #include "options/base_options.h"
+#include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "prop/prop_engine.h"
@@ -47,7 +48,7 @@ CegConjecture::CegConjecture(QuantifiersEngine* qe)
       d_refine_count(0),
       d_syntax_guided(false)
 {
-  if (options::sygusPbe())
+  if (options::sygusSymBreakPbe() || options::sygusUnifPbe())
   {
     d_modules.push_back(d_ceg_pbe.get());
   }
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 472cfbd89..cae2a432d 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -144,7 +144,7 @@ bool CegConjecturePbe::initialize(Node n,
     }
   }
 
-  if (!options::sygusUnifCondSol())
+  if (!options::sygusUnifPbe())
   {
     // we are not doing unification
     return false;