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.

diff --git a/src/options/options.h b/src/options/options.h
index fcf99134d06f213690650be21ecdf54902fbf0eb..ad2729205c7875b262c82464323d829d47736282 100644 (file)
--- 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 a556f2152a65bbbabd9bec8f74b664b2b6f4c639..d1022c51c45530ca55a5f4f6f990d7a791c7c40c 100644 (file)
--- 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 1101f70c5d4bbd600a834d4f412d43a7d41e2638..926eacaae5fb1a36648a8e23cf079ebab6f5f51c 100644 (file)
--- 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 180b33fe010474775406321515854a24f6158241..7b0571274ad7992325073d816170d0d7723a4a80 100644 (file)
--- 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 fc8dedbd38e53c4a7b1ebf75a2dffcf7aa8da7e8..d202648f4939a838e98db22866308b0dff4ae5e2 100644 (file)
--- 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 b3ee7ad4979d94af7271e02a7f8797ba820846b3..f6c17ebf92c8bc2d3cdbced8330b71a9fbfed709 100644 (file)
--- 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)

diff --git a/test/regress/regress1/sygus/hd-01-d1-prog.sy b/test/regress/regress1/sygus/hd-01-d1-prog.sy
index 1379d42063fb5e0a2f6cb3d3f106d12013fbaf56..bbdbda1bd3a73231356b617feae877ec8a356d61 100644 (file)
--- a/test/regress/regress1/sygus/hd-01-d1-prog.sy
+++ b/test/regress/regress1/sygus/hd-01-d1-prog.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --sygus-out=status
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic BV)