From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Sat, 24 Oct 2020 14:16:52 +0000 (-0500)
Subject: Fix issue 5271 (#5335)
X-Git-Tag: cvc5-1.0.0~2663
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0a4ee1ac60e6b914ca8173c773eb9db54cdf0f61;p=cvc5.git

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 b951d0333..a382688a9 100644
--- 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 4653f1c3e..9bb89dd9c 100644
--- 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
index 000000000..ba8180b5e
--- /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)