From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 20 Oct 2021 14:34:10 +0000 (-0500)
Subject: Do not make assumption about model for Boolean variables in FMF (#7407)
X-Git-Tag: cvc5-1.0.0~1044
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3e9e1c54ef54627e4f38094910effb32f6ad7cd2;p=cvc5.git

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 7c1d36ce8..94351274a 100644
--- 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 da6f4c3c9..d24150cf6 100644
--- 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
index 000000000..024d5b6a3
--- /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
index 000000000..eb0c35f68
--- /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)