From: Haniel Barbosa <hanielbbarbosa@gmail.com>
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)