From: Haniel Barbosa Date: Wed, 23 Jun 2021 23:23:30 +0000 (-0300) Subject: [hol] Disable bound fmf when HOL (#6792) X-Git-Tag: cvc5-1.0.0~1560 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=14f613c36fd55b662ce29eeae54a4bc2f26322a4;p=cvc5.git [hol] Disable bound fmf when HOL (#6792) Fixes #6536 --- 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()) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ac837b957..45b695cd9 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -634,6 +634,7 @@ set(regress_0_tests regress0/ho/issue5233-part1-usort-owner.smt2 regress0/ho/issue5371.smt2 regress0/ho/issue6526.smt2 + regress0/ho/issue6536.smt2 regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 regress0/ho/match-middle.smt2 diff --git a/test/regress/regress0/ho/issue6536.smt2 b/test/regress/regress0/ho/issue6536.smt2 new file mode 100644 index 000000000..ed4d453a6 --- /dev/null +++ b/test/regress/regress0/ho/issue6536.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unknown +(set-logic HO_ALL) +(declare-datatypes ((a 0) (b 0)) (((c) (d)) ((h (j b)) (e)))) +(declare-fun f () b) +(declare-fun k (a) b) +(declare-fun g (b b) b) +(assert (forall ((i a)) (distinct (k i) (ite ((_ is c) i) e (ite ((_ is d) i) (h (g (k i) (k i))) f))))) +(check-sat)