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, 20 insertions, 0 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 3c3d6df4a..f8057006c 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -950,6 +950,17 @@ Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
   }
 }
 
+Node NodeManager::mkSingleton(const TypeNode& t, const TNode n)
+{
+  Assert(n.getType().isSubtypeOf(t))
+      << "Invalid operands for mkSingleton. The type '" << n.getType()
+      << "' of node '" << n << "' is not a subtype of '" << t << "'."
+      << std::endl;
+  Node op = mkConst(SingletonOp(t));
+  Node singleton = mkNode(kind::SINGLETON, op, n);
+  return singleton;
+}
+
 Node NodeManager::mkAbstractValue(const TypeNode& type) {
   Node n = mkConst(AbstractValue(++d_abstractValueCount));
   n.setAttribute(TypeAttr(), type);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index ef22101f0..5427c3b6a 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -576,6 +576,15 @@ class NodeManager {
   Node mkNullaryOperator(const TypeNode& type, Kind k);
 
   /**
+  * Create a singleton set from the given element n.
+  * @param t the element type of the returned set.
+  * Note that the type of n needs to be a subtype of t.
+  * @param n the single element in the singleton.
+  * @return a singleton set constructed from the element n.
+  */
+  Node mkSingleton(const TypeNode& t, const TNode n);
+
+  /**
    * Create a constant of type T.  It will have the appropriate
    * CONST_* kind defined for T.
    */