Fix subtyping for sets care graph (#6278)

We were getting types for set singleton/membership in a way that was unsafe for subtyping, which was leading to incorrectly computing care graphs for sets of reals.

Fixes #5705.

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 8d005c6fea627f0ef1683cf44b0e00f0da304294..ea7e773b7dfff040a1d3a3529e1f04f0e0d403b1 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -985,9 +985,20 @@ void TheorySetsPrivate::computeCareGraph()
       {
         Trace("sets-cg-debug") << "...build for " << f1 << std::endl;
         Assert(d_equalityEngine->hasTerm(f1));
-        // break into index based on operator, and type of first argument (since
-        // some operators are parametric)
-        TypeNode tn = f1[0].getType();
+        // break into index based on operator, and the type of the element
+        // type of the proper set, which notice must be safe wrt subtyping.
+        TypeNode tn;
+        if (k == kind::SINGLETON)
+        {
+          // get the type of the singleton set (not the type of its element)
+          tn = f1.getType().getSetElementType();
+        }
+        else
+        {
+          Assert (k == kind::MEMBER);
+          // get the element type of the set (not the type of the element)
+          tn = f1[1].getType().getSetElementType();
+        }
         std::vector<TNode> reps;
         bool hasCareArg = false;
         for (unsigned j = 0; j < f1.getNumChildren(); j++)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e125c651e17c59bf19e392bb660b602bfa35132b..98976994e94b3960a0e5c684ec91c238c9535ccf 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1917,6 +1917,7 @@ set(regress_1_tests
   regress1/sets/choose2.smt2
   regress1/sets/choose3.smt2
   regress1/sets/choose4.smt2
+  regress1/sets/issue5705-cg-subtyping.smt2
   regress1/sets/ListElem.hs.fqout.cvc4.38.smt2
   regress1/sets/ListElts.hs.fqout.cvc4.317.smt2
   regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2

diff --git a/test/regress/regress1/sets/issue5705-cg-subtyping.smt2 b/test/regress/regress1/sets/issue5705-cg-subtyping.smt2
new file mode 100644 (file)
index 0000000..df5b224
--- /dev/null
+++ b/test/regress/regress1/sets/issue5705-cg-subtyping.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_LIRAFS)
+(set-info :status sat)
+(declare-fun s () (Set Real))
+(declare-fun t3 () (Set Real))
+(assert (or (member 1.0 t3) (member 0.0 s)))
+(assert (not (= t3 (setminus s (singleton 1.0)))))
+(check-sat)