Do not make assumption about model for Boolean variables in FMF (#7407)

Fixes cases where models can be wrong for FMF with Boolean variables in the bodies of quantified formulas.

Fixes #6744, all benchmarks on that issue are fixed. This PR adds 2 of the regressions from that issue.

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 7c1d36ce82c5715bdb2731d343abc498b71d50d1..94351274ab073d45760f07ed0ec15d5837dcef15 100644 (file)
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -951,10 +951,15 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
     Node r = n;
     if( !n.isConst() ){
       TypeNode tn = n.getType();
-      if( !fm->hasTerm(n) && tn.isFirstClass() ){
-        r = getSomeDomainElement(fm, tn );
+      if (!fm->hasTerm(n) && tn.isFirstClass())
+      {
+        // if the term is unknown, we do not assume any value for it
+        r = Node::null();
+      }
+      else
+      {
+        r = fm->getRepresentative(r);
       }
-      r = fm->getRepresentative( r );
     }
     Trace("fmc-debug") << "Add constant entry..." << std::endl;
     d.addEntry(fm, mkCondDefault(fm, f), r);

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index da6f4c3c9728f0e3467f9a0bd088996271afd78b..d24150cf6ef89ac9a8924cb70e348e0c7bb1dc5d 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1648,6 +1648,8 @@ set(regress_1_tests
   regress1/fmf/issue4225-univ-fun.smt2
   regress1/fmf/issue5738-dt-interp-finite.smt2
   regress1/fmf/issue6690-re-enum.smt2
+  regress1/fmf/issue6744-2-unc-bool-var.smt2
+  regress1/fmf/issue6744-3-unc-bool-var.smt2
   regress1/fmf/issue916-fmf-or.smt2
   regress1/fmf/jasmin-cdt-crash.smt2
   regress1/fmf/loopy_coda.smt2

diff --git a/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2
new file mode 100644 (file)
index 0000000..024d5b6
--- /dev/null
+++ b/test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-option :finite-model-find true)
+(set-info :status sat)
+(declare-fun v () Bool)
+(declare-fun v2 () Bool)
+(assert (exists ((q (Array Bool (Array Bool (Array Int Bool))))) (forall ((q3 (Array Bool (Array Bool (Array Int Bool))))) (xor v2 v2 v v2 (or v2 (not (= q3 q)))))))
+(check-sat)

diff --git a/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2
new file mode 100644 (file)
index 0000000..eb0c35f
--- /dev/null
+++ b/test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2
@@ -0,0 +1,5 @@
+(set-logic UFC)
+(set-info :status sat)
+(declare-fun v () Bool)
+(assert (and (forall ((q Bool)) (not (xor v (exists ((q Bool)) true) (and (not v) (not q)))))))
+(check-sat)