diff options
| -rw-r--r-- | src/options/options.h | 1 | ||||
| -rw-r--r-- | src/options/options_public_functions.cpp | 4 | ||||
| -rw-r--r-- | src/options/quantifiers_options.toml | 6 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 38 | ||||
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 3 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 7 | ||||
| -rw-r--r-- | 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) |