Fix issue related to use of Boolean term variable for set/bag choose (#8423)

Fixes cvc5/cvc5-projects#501.

I am considering making this detail internal to SkolemManager to avoid similar issues in the future. However, there are some subtle performance implications in doing so, so this will be addressed later.

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index b1e9b32b7361a66ebf3374336e67d3204e38b784..3dae04861fe02cf8c629229e31086e8bc14508f1 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -117,7 +117,13 @@ TrustNode TheoryBags::expandChooseOperator(const Node& node,
 
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
-  Node x = sm->mkPurifySkolem(node, "bagChoose");
+  // the skolem will occur in a term context, thus we give it Boolean
+  // term variable kind immediately.
+  SkolemManager::SkolemFlags flags = node.getType().isBoolean()
+                                         ? SkolemManager::SKOLEM_BOOL_TERM_VAR
+                                         : SkolemManager::SKOLEM_DEFAULT;
+  Node x = sm->mkPurifySkolem(
+      node, "bagChoose", "a variable used to eliminate bag choose", flags);
   Node A = node[0];
   TypeNode bagType = A.getType();
   TypeNode ufType = nm->mkFunctionType(bagType, bagType.getBagElementType());

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 8f23e9232f687e5da8263dadfa65b41e61a10b0d..b01895a74d5cfa8fd1f5e93e327a78e88177e918 100644 (file)
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -1030,7 +1030,12 @@ void CardinalityExtension::mkModelValueElementsFor(
 {
   TypeNode elementType = eqc.getType().getSetElementType();
   bool elementTypeFinite = d_env.isFiniteType(elementType);
-  if (isModelValueBasic(eqc))
+  bool isBasic = isModelValueBasic(eqc);
+  Trace("sets-model") << "mkModelValueElementsFor: " << eqc
+                      << ", isBasic = " << isBasic
+                      << ", isFinite = " << elementTypeFinite
+                      << ", els = " << els << std::endl;
+  if (isBasic)
   {
     std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
     if (it != d_eqc_to_card_term.end())

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index e61881daa4daa4d1513481ac2c63ff0eb0c45c97..6d5de217219b5394830a30c026dc2bdf7fc5818e 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -218,7 +218,7 @@ void TheorySets::processCarePairArgs(TNode a, TNode b)
   // equality or disequality between members affects the number of elements
   // in a set. Therefore we need to split on (= x y) for kind SET_MEMBER.
   // Example:
-  // Suppose (= (member x S) member(y S)) is true and there are
+  // Suppose (set.member x S) = (set.member y S) = true and there are
   // no other members in S. We would get S = {x} if (= x y) is true.
   // Otherwise we would get S = {x, y}.
   if (a.getKind() != SET_MEMBER && d_state.areEqual(a, b))

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 099843e3c03b4c97910bc537f8b0df17bdccf9bb..57835919e781f0bb718c33dddabfea70d90b9d02 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -247,7 +247,14 @@ void TheorySetsPrivate::fullEffortCheck()
         Node n = (*eqc_i);
         if (n != eqc)
         {
-          Trace("sets-eqc") << n << " (" << n.isConst() << ") ";
+          if (TraceIsOn("sets-eqc"))
+          {
+            Trace("sets-eqc") << n;
+            if (n.isConst())
+            {
+              Trace("sets-eqc") << " (const) ";
+            }
+          }
         }
         TypeNode tnn = n.getType();
         if (isSet)
@@ -1211,7 +1218,13 @@ TrustNode TheorySetsPrivate::expandChooseOperator(
 
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = nm->getSkolemManager();
-  Node x = sm->mkPurifySkolem(node, "setChoose");
+  // the skolem will occur in a term context, thus we give it Boolean
+  // term variable kind immediately.
+  SkolemManager::SkolemFlags flags = node.getType().isBoolean()
+                                         ? SkolemManager::SKOLEM_BOOL_TERM_VAR
+                                         : SkolemManager::SKOLEM_DEFAULT;
+  Node x = sm->mkPurifySkolem(
+      node, "setChoose", "a variable used to eliminate set choose", flags);
   Node A = node[0];
   TypeNode setType = A.getType();
   ensureFirstClassSetType(setType);

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 8db3689eb61e86b5af671bdea0d8fd902301a3ce..000cbc3769a530826f62ca1c69a3fa692cc1fa1f 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1263,6 +1263,7 @@ set(regress_0_tests
   regress0/sets/proj-issue177.smt2
   regress0/sets/proj-issue486-sets-split-eq.smt2
   regress0/sets/proj-issue493-choose-det.smt2
+  regress0/sets/proj-issue501-choose-bool-term-var.smt2
   regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
   regress0/sets/setel-eq.smt2
   regress0/sets/sets-deq-dd.smt2

diff --git a/test/regress/cli/regress0/sets/proj-issue501-choose-bool-term-var.smt2 b/test/regress/cli/regress0/sets/proj-issue501-choose-bool-term-var.smt2
new file mode 100644 (file)
index 0000000..0fcdbdd
--- /dev/null
+++ b/test/regress/cli/regress0/sets/proj-issue501-choose-bool-term-var.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-option :sets-ext true)
+(set-option :fmf-bound true)
+(declare-const x (Bag (Set Bool)))
+(declare-const x1 (Set Bool))
+(declare-const x3 (Set Bool))
+(declare-const x6 (Set Bool))
+(assert (set.choose (ite (set.is_singleton x3) x6 x1)))
+(assert (<= (set.card x6) (bag.count x6 x)))
+(check-sat)