From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 27 Dec 2017 22:25:22 +0000 (-0600)
Subject: Disable sygus PBE when sygus stream is enabled (#1451)
X-Git-Tag: cvc5-1.0.0~5407
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=576f20751dc17348b6b680d6ea350f6e42f405ac;p=cvc5.git

Disable sygus PBE when sygus stream is enabled (#1451)
---

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index c3091a131..65731547d 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -261,7 +261,7 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default
   include constants when reconstruct solutions for single invocation conjectures in original grammar
 option cegqiSingleInvAbort --cegqi-si-abort bool :default false
   abort if synthesis conjecture is not single invocation
-option sygusPbe --sygus-pbe bool :default true
+option sygusPbe --sygus-pbe bool :default true :read-write
   sygus advanced pruning based on examples
 option sygusQePreproc --sygus-qe-preproc bool :default false
   use quantifier elimination as a preprocessing step for sygus
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4336b7a05..9b4837d43 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1873,6 +1873,14 @@ void SmtEngine::setDefaults() {
     if( !options::instNoEntail.wasSetByUser() ){
       options::instNoEntail.set( false );
     }
+    if (options::sygusStream())
+    {
+      // PBE and streaming modes are incompatible
+      if (!options::sygusPbe.wasSetByUser())
+      {
+        options::sygusPbe.set(false);
+      }
+    }
     //do not allow partial functions
     if( !options::bitvectorDivByZeroConst.wasSetByUser() ){
       options::bitvectorDivByZeroConst.set( true );