From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 9 May 2018 16:54:59 +0000 (-0500)
Subject: Better option names for PBE (#1891)
X-Git-Tag: cvc5-1.0.0~5072
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=609a4c11eed577f127644006465d7e112139532d;p=cvc5.git

Better option names for PBE (#1891)
---

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
@@ -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 2f911bdd1..4c771c143 100644
--- 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 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;