From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 29 Mar 2022 16:46:14 +0000 (-0500)
Subject: Fix issue related to use of Boolean term variable for set/bag choose (#8423)
X-Git-Tag: cvc5-1.0.0~141
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8c92533a49b715a70d7ef187ef470901fd0c11c8;p=cvc5.git

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 b1e9b32b7..3dae04861 100644
--- 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 8f23e9232..b01895a74 100644
--- 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 e61881daa..6d5de2172 100644
--- 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 099843e3c..57835919e 100644
--- 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 8db3689eb..000cbc376 100644
--- 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
index 000000000..0fcdbdd25
--- /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)