Better option names for PBE (#1891)

diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index ef736e913c395c6778868948c6fc7b66694ed7c7..8d6f0baf33ba60971980cbcd42c327dbcf2076ad 100644 (file)
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -112,6 +112,14 @@ header = "options/datatypes_options.h"
   read_only  = true
   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"

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 2f911bdd1645628fd8f0ec857d190f4cc74f5e7a..4c771c1437ea40af2892a0ea595bd0ec653b007b 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -959,14 +959,6 @@ header = "options/quantifiers_options.h"
   read_only  = true
   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"
@@ -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 c750b8a12be75f1b9f39351fdf31d37a84ed4483..aeec5298a9120c1bf4e45b22aaa01f25941710ff 100644 (file)
--- 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 6f660642e0884ed1dc530c6ad25c99f22efbcbf2..757f4d040ff370a61ba4e715bd0850b35e8b89ff 100644 (file)
--- 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 d5a43022921aac8d8add793c89611eba506c847c..69cf7f73babe0f24275bea7f3259cfc4eac09979 100644 (file)
--- 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 472cfbd89f562375df1bb8659390a3207cc08b11..cae2a432df2cc98a801b8ccb2e23cfc9730ea59f 100644 (file)
--- 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;