Rename sygus option name (#3977)

This option enables the sygus solver (previous name was ceGuidedInst, deprecated from CAV 15 specific approach).

It also improves when this option is set. In particular we ensure it is enabled when sygus is enabled for any reason.

6 files changed, 24 insertions, 35 deletions

diff --git a/src/options/options.h b/src/options/options.h
index fcf99134d..ad2729205 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -240,7 +240,6 @@ public:
   void setOut(std::ostream*);
   void setOutputLanguage(OutputLanguage);
 
-  bool wasSetByUserCeGuidedInst() const;
   bool wasSetByUserDumpSynth() const;
   bool wasSetByUserEarlyExit() const;
   bool wasSetByUserForceLogicString() const;
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index a556f2152..d1022c51c 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -218,10 +218,6 @@ void Options::setOutputLanguage(OutputLanguage value) {
   set(options::outputLanguage, value);
 }
 
-bool Options::wasSetByUserCeGuidedInst() const {
-  return wasSetByUser(options::ceGuidedInst);
-}
-
 bool Options::wasSetByUserDumpSynth() const {
   return wasSetByUser(options::dumpSynth);
 }
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 1101f70c5..926eacaae 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1032,12 +1032,12 @@ header = "options/quantifiers_options.h"
   help       = "attempt to preprocess arbitrary inputs to sygus conjectures"
 
 [[option]]
-  name       = "ceGuidedInst"
+  name       = "sygus"
   category   = "regular"
-  long       = "cegqi"
+  long       = "sygus"
   type       = "bool"
   default    = "false"
-  help       = "counterexample-guided quantifier instantiation for sygus"
+  help       = "use sygus solver (default is true for sygus inputs)"
 
 [[option]]
   name       = "cegqiSingleInvMode"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 180b33fe0..7b0571274 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1950,14 +1950,15 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  //apply counterexample guided instantiation options
-  // if we are attempting to rewrite everything to SyGuS, use ceGuidedInst
+  // apply sygus options
+  // if we are attempting to rewrite everything to SyGuS, use sygus()
   if (is_sygus)
   {
-    if (!options::ceGuidedInst.wasSetByUser())
+    if (!options::sygus())
     {
-      options::ceGuidedInst.set(true);
+      Trace("smt") << "turning on sygus" << std::endl;
     }
+    options::sygus.set(true);
     // must use Ferrante/Rackoff for real arithmetic
     if (!options::cbqiMidpoint.wasSetByUser())
     {
@@ -1970,27 +1971,18 @@ void SmtEngine::setDefaults() {
         options::cbqi.set(true);
       }
     }
-  }
-  if (options::sygusInference())
-  {
-    // optimization: apply preskolemization, makes it succeed more often
-    if (!options::preSkolemQuant.wasSetByUser())
-    {
-      options::preSkolemQuant.set(true);
-    }
-    if (!options::preSkolemQuantNested.wasSetByUser())
+    if (options::sygusInference())
     {
-      options::preSkolemQuantNested.set(true);
-    }
-  }
-  if (options::cegqiSingleInvMode() != options::CegqiSingleInvMode::NONE)
-  {
-    if( !options::ceGuidedInst.wasSetByUser() ){
-      options::ceGuidedInst.set( true );
+      // optimization: apply preskolemization, makes it succeed more often
+      if (!options::preSkolemQuant.wasSetByUser())
+      {
+        options::preSkolemQuant.set(true);
+      }
+      if (!options::preSkolemQuantNested.wasSetByUser())
+      {
+        options::preSkolemQuantNested.set(true);
+      }
     }
-  }
-  // if sygus is enabled, set the defaults for sygus
-  if( options::ceGuidedInst() ){
     //counterexample-guided instantiation for sygus
     if( !options::cegqiSingleInvMode.wasSetByUser() ){
       options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::USE);
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index fc8dedbd3..d202648f4 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -548,7 +548,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n) {
 }
 
 void TheoryDatatypes::finishInit() {
-  if( getQuantifiersEngine() && options::ceGuidedInst() ){
+  if (getQuantifiersEngine() && options::sygus())
+  {
     d_sygusExtension.reset(
         new SygusExtension(this, getQuantifiersEngine(), getSatContext()));
     // do congruence on evaluation functions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index b3ee7ad49..f6c17ebf9 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -124,7 +124,7 @@ class QuantifiersEnginePrivate
       modules.push_back(d_i_cbqi.get());
       qe->getInstantiate()->addRewriter(d_i_cbqi->getInstRewriter());
     }
-    if (options::ceGuidedInst())
+    if (options::sygus())
     {
       d_synth_e.reset(new quantifiers::SynthEngine(qe, c));
       modules.push_back(d_synth_e.get());
@@ -212,7 +212,8 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c,
   d_util.push_back(d_term_util.get());
   d_util.push_back(d_term_db.get());
 
-  if (options::ceGuidedInst()) {
+  if (options::sygus())
+  {
     d_sygus_tdb.reset(new quantifiers::TermDbSygus(c, this));
   }  
 
@@ -499,7 +500,7 @@ void QuantifiersEngine::ppNotifyAssertions(
     theory_sep->initializeBounds();
     d_qepr->finishInit();
   }
-  if (options::ceGuidedInst())
+  if (options::sygus())
   {
     quantifiers::SynthEngine* sye = d_private->d_synth_e.get();
     for (const Node& a : assertions)