diff options
Diffstat (limited to 'src/smt/set_defaults.cpp')
| -rw-r--r-- | src/smt/set_defaults.cpp | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 67c5c5647..cd05b84c4 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -271,11 +271,15 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) // Set default options associated with strings-exp. We also set these options // if we are using eager string preprocessing, which may introduce quantified // formulas at preprocess time. + // + // We don't want to set this option when we are in logics that contain ALL. if (!logic.hasEverything() && logic.isTheoryEnabled(THEORY_STRINGS)) { // If the user explicitly set a logic that includes strings, but is not // the generic "ALL" logic, then enable stringsExp. opts.strings.stringExp = true; + Trace("smt") << "Turning stringExp on since logic does not have everything " + "and string theory is enabled\n"; } if (options::stringExp() || !options::stringLazyPreproc()) { @@ -753,7 +757,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } // If in arrays, set the UF handler to arrays - if (logic.isTheoryEnabled(THEORY_ARRAYS) && !options::ufHo() + if (logic.isTheoryEnabled(THEORY_ARRAYS) && !logic.isHigherOrder() && !options::finiteModelFind() && (!logic.isQuantified() || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF)))) @@ -890,7 +894,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) options::DecisionMode decMode = // anything that uses sygus uses internal usesSygus ? options::DecisionMode::INTERNAL : - // ALL + // ALL or its supersets logic.hasEverything() ? options::DecisionMode::JUSTIFICATION : ( // QF_BV @@ -922,7 +926,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) : options::DecisionMode::INTERNAL); bool stoponly = - // ALL + // ALL or its supersets logic.hasEverything() || logic.isTheoryEnabled(THEORY_STRINGS) ? false : ( // QF_AUFLIA @@ -986,8 +990,9 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.quantifiers.prenexQuant = options::PrenexQuantMode::NONE; } } - if (options::ufHo()) + if (logic.isHigherOrder()) { + opts.uf.ufHo = true; // if higher-order, then current variants of model-based instantiation // cannot be used if (options::mbqiMode() != options::MbqiMode::NONE) |