From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 27 May 2021 21:18:28 +0000 (-0500)
Subject: Fix CEGQI for datatypes with Boolean subfields (#6630)
X-Git-Tag: cvc5-1.0.0~1685
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b9062490a7590708bcf158d4670a23d859fe3355;p=cvc5.git

Fix CEGQI for datatypes with Boolean subfields (#6630)

Fixes a solution soundness issue caused by allowing ineligible terms of kind BOOLEAN_TERM_VARIABLE to appear in instantiations.

This also corrects the expected solution on a benchmark that had an incorrect status.

Fixes #6603.
---

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 0d85b8946..88da629a0 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1088,7 +1088,8 @@ bool CegInstantiator::doAddInstantiation(std::vector<Node>& vars,
 
 bool CegInstantiator::isEligibleForInstantiation(Node n) const
 {
-  if (n.getKind() != INST_CONSTANT && n.getKind() != SKOLEM)
+  Kind nk = n.getKind();
+  if (nk != INST_CONSTANT && nk != SKOLEM && nk != BOOLEAN_TERM_VARIABLE)
   {
     return true;
   }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 81e5ca8c6..35d2553de 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -872,6 +872,7 @@ set(regress_0_tests
   regress0/quantifiers/issue4576.smt2
   regress0/quantifiers/issue5645-dt-cm-spurious.smt2
   regress0/quantifiers/issue5693-prenex.smt2
+  regress0/quantifiers/issue6603-dt-bool-cegqi.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macro-back-subs-sat.smt2
   regress0/quantifiers/macros-int-real.smt2
diff --git a/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2
index 0d3f711bf..6ed3a1867 100644
--- a/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2
+++ b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2
@@ -1,5 +1,5 @@
 (set-logic ALL)
-(set-info :status sat)
+(set-info :status unsat)
 (declare-datatypes ((Enum1 0)) (((None) (cons (data Bool)))))
 (assert (forall ((var_1 Enum1)) (data var_1)))
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 b/test/regress/regress0/quantifiers/issue6603-dt-bool-cegqi.smt2
new file mode 100644
index 000000000..fce67f4d0
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue6603-dt-bool-cegqi.smt2
@@ -0,0 +1,5 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-datatypes ((E 0)) (((c (a Bool)))))
+(assert (forall ((v E)) (a v)))
+(check-sat)