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 0d85b89466ac9eb22754bc8a96de7b051b2c0298..88da629a0a63679a31d03cb3990cc329e8ddafc3 100644 (file)
--- 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 81e5ca8c64518f864307f3fd7bcf9a54392337b0..35d2553de78a3764eb828b4e7d859687056ca5a0 100644 (file)
--- 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 0d3f711bf27aef1b8654f68be8da59003d86ff8d..6ed3a1867011c103894020ab349da35d84656b88 100644 (file)
--- 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 (file)
index 0000000..fce67f4
--- /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)