Fix sets cardinality inference involving equivalent parents (#6855)

This fixes an unsoundness issue in the sets + cardinality solver.

One rule of this solver applies in sets when two parents of a child of a cardinality graph are equal, in which case we know that child or one of its siblings must be equal to the opposite parent. For example, this rule tells us that:

if T = (union T S), then (intersect T S) = S.

The explanation of this rule could consider the representative term of one the parents instead of the term itself say (union T S) is representative T, giving the unsound inference: if (union T S) = (union T S), then (intersect T S) = S. This ensures we use the original terms.

This PR also does some minor cleanup.

4 files changed, 37 insertions, 23 deletions

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 063c440a5..62dedb35a 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -305,7 +305,7 @@ void CardinalityExtension::checkCardCycles()
   // build order of equivalence classes, also build cardinality graph
   const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
   d_oSetEqc.clear();
-  d_card_parent.clear();
+  d_cardParent.clear();
   for (const Node& s : setEqc)
   {
     std::vector<Node> curr;
@@ -317,7 +317,6 @@ void CardinalityExtension::checkCardCycles()
     }
   }
 
-  Trace("sets") << "d_card_parent: " << d_card_parent << std::endl;
   Trace("sets") << "d_oSetEqc: " << d_oSetEqc << std::endl;
   Trace("sets") << "Done check cardinality cycles" << std::endl;
 }
@@ -432,14 +431,6 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
       {
         return;
       }
-      else
-      {
-        // justify why there is no edge to parents (necessary?)
-        for (unsigned e = 0; e < n_parents; e++)
-        {
-          Node p = (e == true_sib) ? u : n[e];
-        }
-      }
       continue;
     }
     std::vector<Node> card_parents;
@@ -521,7 +512,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
         card_parent_ids.push_back(is_union ? 2 : e);
       }
     }
-    Assert(d_card_parent[n].empty());
+    Assert(d_cardParent[n].empty());
     Trace("sets-debug") << "get parent representatives..." << std::endl;
     // for each parent, take their representatives
     for (unsigned k = 0, numcp = card_parents.size(); k < numcp; k++)
@@ -573,9 +564,9 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
       else
       {
         bool dup = false;
-        for (unsigned l = 0, numcpn = d_card_parent[n].size(); l < numcpn; l++)
+        for (unsigned l = 0, numcpn = d_cardParent[n].size(); l < numcpn; l++)
         {
-          Node cpnl = d_card_parent[n][l];
+          Node cpnl = d_cardParent[n][l].first;
           if (eqcc != cpnl)
           {
             continue;
@@ -613,7 +604,13 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
               conc.push_back(cpk.eqNode(n));
             }
           }
-          d_im.assertInference(conc, InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2, cpk.eqNode(cpnl));
+          // use the original term, not the representative.
+          // for example, we conclude T = (union T S) => (intersect T S) = S
+          // here where we do not use the representative of T or (union T S).
+          Node cpnlb = d_cardParent[n][l].second;
+          d_im.assertInference(conc,
+                               InferenceId::SETS_CARD_GRAPH_EQ_PARENT_2,
+                               cpk.eqNode(cpnlb));
           d_im.doPendingLemmas();
           if (d_im.hasSent())
           {
@@ -622,18 +619,18 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc,
         }
         if (!dup)
         {
-          d_card_parent[n].push_back(eqcc);
+          d_cardParent[n].emplace_back(eqcc, cpk);
         }
       }
     }
     // now recurse on parents (to ensure their normal will be computed after
     // this eqc)
     exp.push_back(eqc.eqNode(n));
-    for (const Node& cpnc : d_card_parent[n])
+    for (const std::pair<Node, Node>& cpnc : d_cardParent[n])
     {
-      Trace("sets-cycle-debug")
-          << "Traverse card parent " << eqc << " -> " << cpnc << std::endl;
-      checkCardCyclesRec(cpnc, curr, exp);
+      Trace("sets-cycle-debug") << "Traverse card parent " << eqc << " -> "
+                                << cpnc.first << std::endl;
+      checkCardCyclesRec(cpnc.first, curr, exp);
       if (d_im.hasSent())
       {
         return;
@@ -897,7 +894,7 @@ void CardinalityExtension::checkNormalForm(Node eqc,
   for (const Node& n : nvsets)
   {
     Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
-    if (d_card_parent[n].empty())
+    if (d_cardParent[n].empty())
     {
       // nothing to do
       continue;
@@ -905,8 +902,9 @@ void CardinalityExtension::checkNormalForm(Node eqc,
     Assert(d_localBase.find(n) != d_localBase.end());
     Node cbase = d_localBase[n];
     Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
-    for (const Node& p : d_card_parent[n])
+    for (const std::pair<Node, Node>& cp : d_cardParent[n])
     {
+      Node p = cp.first;
       Trace("sets-nf-debug") << "Check parent " << p << std::endl;
       if (parents_proc[cbase].find(p) != parents_proc[cbase].end())
       {
diff --git a/src/theory/sets/cardinality_extension.h b/src/theory/sets/cardinality_extension.h
index ce2f29bd5..bddcfaf1b 100644
--- a/src/theory/sets/cardinality_extension.h
+++ b/src/theory/sets/cardinality_extension.h
@@ -357,9 +357,12 @@ class CardinalityExtension
   std::vector<Node> d_oSetEqc;
   /**
    * This maps set terms to the set of representatives of their "parent" sets,
-   * see checkCardCycles.
+   * see checkCardCycles. Parents are stored as a pair of the form
+   *   (r, t)
+   * where t is the parent term and r is the representative of equivalence
+   * class of t.
    */
-  std::map<Node, std::vector<Node> > d_card_parent;
+  std::map<Node, std::vector<std::pair<Node, Node>>> d_cardParent;
   /**
    * Maps equivalence classes + set terms in that equivalence class to their
    * "flat form" (see checkNormalForms).
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ea78096dc..cdc77c980 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2068,6 +2068,7 @@ set(regress_1_tests
   regress1/sets/remove_check_free_31_6.smt2
   regress1/sets/sets-disequal.smt2
   regress1/sets/sets-tuple-poly.cvc
+  regress1/sets/sets-uc-wrong.smt2
   regress1/sets/set-comp-sat.smt2
   regress1/sets/sharingbug.smt2
   regress1/sets/univ-set-uf-elim.smt2
diff --git a/test/regress/regress1/sets/sets-uc-wrong.smt2 b/test/regress/regress1/sets/sets-uc-wrong.smt2
new file mode 100644
index 000000000..e8b768d36
--- /dev/null
+++ b/test/regress/regress1/sets/sets-uc-wrong.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun t () (Set Int))
+(declare-fun s () (Set Int))
+(declare-const v Bool)
+(assert (forall ((q Bool)) (distinct v (subset s t))))
+(assert (= 1 (card t)))
+(check-sat)
+(assert v)
+(check-sat)