Fix issue 5271 (#5335)

This PR fixes #5271 by splitting on the equality of set members which ensures members are distinct when collectModelInfo is called.
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index b951d03339f5fb4c5747f4a4f3bd452c22299760..a382688a9c12bae1c8bd6334fa93848c96d2f092 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -850,7 +850,17 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
     {
       Node f1 = t1->getData();
       Node f2 = t2->getData();
-      if (!d_state.areEqual(f1, f2))
+
+      // Usually when (= (f x) (f y)), we don't care whether (= x y) is true or
+      // not for the shared variables x, y in the care graph.
+      // However, this does not apply to the membership operator since the
+      // equality or disequality between members affects the number of elements
+      // in a set. Therefore we need to split on (= x y) for kind MEMBER.
+      // Example:
+      // Suppose (= (member x S) member( y, S)) is 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 (f1.getKind() == MEMBER || !d_state.areEqual(f1, f2))
       {
         Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
         vector<pair<TNode, TNode> > currentPairs;
@@ -1101,6 +1111,9 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
           TypeNode elementType = eqc.getType().getSetElementType();
           for (const std::pair<const Node, Node>& itmm : emems)
           {
+            Trace("sets-model")
+                << "m->getRepresentative(" << itmm.first
+                << ")= " << m->getRepresentative(itmm.first) << std::endl;
             Node t = nm->mkSingleton(elementType, itmm.first);
             els.push_back(t);
           }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4653f1c3e0b818ef0e4ca603c9681caa512195c2..9bb89dd9c7d507a035f94ae67941a611f746b465 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1791,6 +1791,7 @@ set(regress_1_tests
   regress1/sets/issue2568.smt2
   regress1/sets/issue2904.smt2
   regress1/sets/issue4391-card-lasso.smt2
+  regress1/sets/issue5271.smt2
   regress1/sets/issue5309.smt2
   regress1/sets/lemmabug-ListElts317minimized.smt2
   regress1/sets/remove_check_free_31_6.smt2

diff --git a/test/regress/regress1/sets/issue5271.smt2 b/test/regress/regress1/sets/issue5271.smt2
new file mode 100644 (file)
index 0000000..ba8180b
--- /dev/null
+++ b/test/regress/regress1/sets/issue5271.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun s () (Set Int))
+(assert (> (card s) 1))
+(assert (and (member 0 s) (exists ((x Int)) (member (mod x 1) s))))
+(check-sat)