From 3e9e1c54ef54627e4f38094910effb32f6ad7cd2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 20 Oct 2021 09:34:10 -0500 Subject: [PATCH] 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. --- src/theory/quantifiers/fmf/full_model_check.cpp | 11 ++++++++--- test/regress/CMakeLists.txt | 2 ++ .../regress1/fmf/issue6744-2-unc-bool-var.smt2 | 7 +++++++ .../regress1/fmf/issue6744-3-unc-bool-var.smt2 | 5 +++++ 4 files changed, 22 insertions(+), 3 deletions(-) create mode 100644 test/regress/regress1/fmf/issue6744-2-unc-bool-var.smt2 create mode 100644 test/regress/regress1/fmf/issue6744-3-unc-bool-var.smt2 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) -- 2.30.2