diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-02 21:42:55 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-02 21:42:55 -0500 |
commit | 76d03115cfcade000a9fd18ff9ba7008636eb662 (patch) | |
tree | 26e949b462259e045430705a45e00dbefde541e0 /src/smt | |
parent | 0dec323ac1b45ce1ca194e9bb2a335c8def525d2 (diff) |
sygusComp2018: update sygus-related options setting in smt engine (#2108)
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 53ea9fd58..22916e354 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1292,8 +1292,10 @@ void SmtEngine::setDefaults() { options::bitvectorDivByZeroConst.set( language::isInputLang_smt2_6(options::inputLanguage())); } + bool is_sygus = false; if (options::inputLanguage() == language::input::LANG_SYGUS) { + is_sygus = true; if (!options::ceGuidedInst.wasSetByUser()) { options::ceGuidedInst.set(true); @@ -1303,17 +1305,14 @@ void SmtEngine::setDefaults() { { options::cbqiMidpoint.set(true); } - // do not assign function values (optimization) - if (!options::assignFunctionValues.wasSetByUser()) + if (options::sygusRepairConst()) { - options::assignFunctionValues.set(false); + if (!options::cbqi.wasSetByUser()) + { + options::cbqi.set(true); + } } } - else - { - // cannot use sygus repair constants - options::sygusRepairConst.set(false); - } if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { @@ -1603,7 +1602,7 @@ void SmtEngine::setDefaults() { // cases where we need produce models if (!options::produceModels() && (options::produceAssignments() || options::sygusRewSynthCheck() - || options::sygusRepairConst())) + || is_sygus)) { Notice() << "SmtEngine: turning on produce-models" << endl; setOption("produce-models", SExpr("true")); |