From 0e09af0be57ec4df28869e4383a40d847c0a6b5a Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 9 Mar 2020 22:18:58 -0500 Subject: [PATCH] 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. --- src/options/options.h | 1 - src/options/options_public_functions.cpp | 4 --- src/options/quantifiers_options.toml | 6 ++-- src/smt/smt_engine.cpp | 38 ++++++++------------ src/theory/datatypes/theory_datatypes.cpp | 3 +- src/theory/quantifiers_engine.cpp | 7 ++-- test/regress/regress1/sygus/hd-01-d1-prog.sy | 2 +- 7 files changed, 25 insertions(+), 36 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) diff --git a/test/regress/regress1/sygus/hd-01-d1-prog.sy b/test/regress/regress1/sygus/hd-01-d1-prog.sy index 1379d4206..bbdbda1bd 100644 --- 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) -- 2.30.2