diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-10-10 23:30:58 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-10 23:30:58 -0500 |
commit | 1d1d1908f7929f0bf3532d7d6bf09103e400cc4f (patch) | |
tree | fc337c146e56163946558ceeb1732d8094f2b06b /src | |
parent | 0da5ede58934b3a30944e32835698e84626f4c0a (diff) |
Fix default setting of CegisUnif options (#2605)
Diffstat (limited to 'src')
-rw-r--r-- | src/options/quantifiers_options.toml | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 34 |
2 files changed, 23 insertions, 13 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index c844a197d..2e5252529 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -994,7 +994,7 @@ header = "options/quantifiers_options.h" [[option]] name = "sygusUnifCondIndNoRepeatSol" category = "regular" - long = "sygus-unif-cond-indpendent-no-repeat-sol" + long = "sygus-unif-cond-independent-no-repeat-sol" type = "bool" default = "true" help = "Do not try repeated solutions when using independent synthesis of conditions in unification-based function synthesis" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1bde3975e..0a4859971 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1115,18 +1115,6 @@ void SmtEngine::setDefaults() { if (options::inputLanguage() == language::input::LANG_SYGUS) { is_sygus = true; - // must use Ferrante/Rackoff for real arithmetic - if (!options::cbqiMidpoint.wasSetByUser()) - { - options::cbqiMidpoint.set(true); - } - if (options::sygusRepairConst()) - { - if (!options::cbqi.wasSetByUser()) - { - options::cbqi.set(true); - } - } } if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) @@ -1812,6 +1800,28 @@ void SmtEngine::setDefaults() { { options::ceGuidedInst.set(true); } + // must use Ferrante/Rackoff for real arithmetic + if (!options::cbqiMidpoint.wasSetByUser()) + { + options::cbqiMidpoint.set(true); + } + if (options::sygusRepairConst()) + { + if (!options::cbqi.wasSetByUser()) + { + options::cbqi.set(true); + } + } + // setting unif requirements + if (options::sygusUnifBooleanHeuristicDt() + && !options::sygusUnifCondIndependent()) + { + options::sygusUnifCondIndependent.set(true); + } + if (options::sygusUnifCondIndependent() && !options::sygusUnif()) + { + options::sygusUnif.set(true); + } } if (options::sygusInference()) { |