From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 5 Apr 2021 15:21:55 +0000 (-0500)
Subject: Fix subtyping for sets care graph (#6278)
X-Git-Tag: cvc5-1.0.0~1973
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=73bc16fbba65ca8d8cdc9dd6674ae9280658ee9a;p=cvc5.git

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 8d005c6fe..ea7e773b7 100644
--- 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 e125c651e..98976994e 100644
--- 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
index 000000000..df5b2246c
--- /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)