Remove subtyping for sets theory (#5179)

This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631.
Changes:

Add SingletonOp for singletons to specify the type of the single element in the set.
Add mkSingleton to the solver to enable the user to pass the sort of the single element.
Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON

2 files changed, 6 insertions, 6 deletions

diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py
index 99a8d4c40..67d9808e7 100644
--- a/examples/api/python/sets.py
+++ b/examples/api/python/sets.py
@@ -66,9 +66,9 @@ if __name__ == "__main__":
     two = slv.mkReal(2)
     three = slv.mkReal(3)
 
-    singleton_one = slv.mkTerm(kinds.Singleton, one)
-    singleton_two = slv.mkTerm(kinds.Singleton, two)
-    singleton_three = slv.mkTerm(kinds.Singleton, three)
+    singleton_one = slv.mkSingleton(integer, one)
+    singleton_two = slv.mkSingleton(integer, two)
+    singleton_three = slv.mkSingleton(integer, three)
     one_two = slv.mkTerm(kinds.Union, singleton_one, singleton_two)
     two_three = slv.mkTerm(kinds.Union, singleton_two, singleton_three)
     intersection = slv.mkTerm(kinds.Intersection, one_two, two_three)
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index 9e0c0a2af..fd85858a2 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -73,9 +73,9 @@ int main()
     Term two = slv.mkReal(2);
     Term three = slv.mkReal(3);
 
-    Term singleton_one = slv.mkTerm(SINGLETON, one);
-    Term singleton_two = slv.mkTerm(SINGLETON, two);
-    Term singleton_three = slv.mkTerm(SINGLETON, three);
+    Term singleton_one = slv.mkSingleton(integer, one);
+    Term singleton_two = slv.mkSingleton(integer, two);
+    Term singleton_three = slv.mkSingleton(integer, three);
     Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two);
     Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three);
     Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three);