diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-09 22:18:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-09 20:18:58 -0700 |
commit | 0e09af0be57ec4df28869e4383a40d847c0a6b5a (patch) | |
tree | 659be92f761f174f6690bd16d1d2e6b0f2301999 /src/smt/smt_engine.cpp | |
parent | 3ebc297e6ff589f7b98519cd2aa23963a4e06652 (diff) |
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.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 38 |
1 files changed, 15 insertions, 23 deletions
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); |