diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-06-23 20:23:30 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-23 23:23:30 +0000 |
| commit | 14f613c36fd55b662ce29eeae54a4bc2f26322a4 (patch) | |
| tree | 357b0674d0c996531c2ba6411a5d6f75a116e62b /src/smt/set_defaults.cpp | |
| parent | 228d35b578404b4931c6b4b9c9a0a199a0a9236e (diff) | |
[hol] Disable bound fmf when HOL (#6792)
Fixes #6536
Diffstat (limited to 'src/smt/set_defaults.cpp')
| -rw-r--r-- | src/smt/set_defaults.cpp | 24 |
1 files changed, 20 insertions, 4 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index e119ce4d4..7ae07d196 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -296,7 +296,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (!opts.quantifiers.fmfBoundWasSetByUser) { opts.quantifiers.fmfBound = true; - Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl; + Trace("smt") << "turning on fmf-bound, for strings-exp" << std::endl; } // Note we allow E-matching by default to support combinations of sequences // and quantifiers. @@ -894,7 +894,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) options::DecisionMode decMode = // anything that uses sygus uses internal usesSygus ? options::DecisionMode::INTERNAL : - // ALL or its supersets + // ALL or its supersets logic.hasEverything() ? options::DecisionMode::JUSTIFICATION : ( // QF_BV @@ -973,9 +973,11 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) || (opts.quantifiers.fmfBoundIntWasSetByUser && options::fmfBoundInt())) { opts.quantifiers.fmfBound = true; + Trace("smt") + << "turning on fmf-bound, for fmf-bound-int or fmf-bound-lazy\n"; } - // now have determined whether fmfBoundInt is on/off - // apply fmfBoundInt options + // now have determined whether fmfBound is on/off + // apply fmfBound options if (options::fmfBound()) { if (!opts.quantifiers.mbqiModeWasSetByUser @@ -1015,6 +1017,20 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { opts.quantifiers.macrosQuant = false; } + // HOL is incompatible with fmfBound + if (options::fmfBound()) + { + if (opts.quantifiers.fmfBoundWasSetByUser + || opts.quantifiers.fmfBoundLazyWasSetByUser + || opts.quantifiers.fmfBoundIntWasSetByUser) + { + Notice() << "Disabling bound finite-model finding since it is " + "incompatible with HOL.\n"; + } + + opts.quantifiers.fmfBound = false; + Trace("smt") << "turning off fmf-bound, since HOL\n"; + } } if (options::fmfFunWellDefinedRelevant()) { |