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

25 files changed, 296 insertions, 70 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 3ca20e8dc..65223f3c5 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -773,6 +773,8 @@ libcvc4_add_sources(
   theory/sets/inference_manager.h
   theory/sets/normal_form.h
   theory/sets/rels_utils.h
+  theory/sets/singleton_op.cpp
+  theory/sets/singleton_op.h
   theory/sets/skolem_cache.cpp
   theory/sets/skolem_cache.h
   theory/sets/solver_state.cpp
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 6ed8855e4..179eb672e 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3701,6 +3701,23 @@ Term Solver::mkEmptySet(Sort s) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Term Solver::mkSingleton(Sort s, Term t) const
+{
+  NodeManagerScope scope(getNodeManager());
+
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_ARG_CHECK_EXPECTED(!t.isNull(), t) << "non-null term";
+  CVC4_API_SOLVER_CHECK_TERM(t);
+  checkMkTerm(SINGLETON, 1);
+
+  TypeNode typeNode = TypeNode::fromType(*s.d_type);
+  Node res = getNodeManager()->mkSingleton(typeNode, *t.d_node);
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
+
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 Term Solver::mkEmptyBag(Sort s) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 31ff13ba0..c53d6f828 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2600,6 +2600,15 @@ class CVC4_PUBLIC Solver
   Term mkEmptySet(Sort s) const;
 
   /**
+   * Create a singleton set from the given element t.
+   * @param s the element sort of the returned set.
+   * Note that the sort of t needs to be a subtype of s.
+   * @param t the single element in the singleton.
+   * @return a singleton set constructed from the element t.
+   */
+  Term mkSingleton(Sort s, Term t) const;
+
+  /**
    * Create a constant representing an empty bag of the given sort.
    * @param s the sort of the bag elements.
    * @return the empty bag constant
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 76dcc5317..987db9363 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -177,6 +177,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Term mkRegexpEmpty() except +
         Term mkRegexpSigma() except +
         Term mkEmptySet(Sort s) except +
+        Term mkSingleton(Sort s, Term t) except +
         Term mkSepNil(Sort sort) except +
         Term mkString(const string& s) except +
         Term mkString(const vector[unsigned]& s) except +
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index daff390b4..bf135dca2 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -691,6 +691,11 @@ cdef class Solver:
         term.cterm = self.csolver.mkEmptySet(s.csort)
         return term
 
+    def mkSingleton(self, Sort s, Term t):
+        cdef Term term = Term(self)
+        term.cterm = self.csolver.mkSingleton(s.csort, t.cterm)
+        return term
+
     def mkSepNil(self, Sort sort):
         cdef Term term = Term(self)
         term.cterm = self.csolver.mkSepNil(sort.csort)
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.
    */
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 5f959c660..6eb0924ac 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2158,9 +2158,9 @@ simpleTerm[CVC4::api::Term& f]
     /* finite set literal */
   | LBRACE formula[f] { args.push_back(f); }
     ( COMMA formula[f] { args.push_back(f); } )* RBRACE
-    { f = MK_TERM(api::SINGLETON, args[0]);
+    { f = SOLVER->mkSingleton(args[0].getSort(), args[0]);
       for(size_t i = 1; i < args.size(); ++i) {
-        f = MK_TERM(api::UNION, f, MK_TERM(api::SINGLETON, args[i]));
+        f = MK_TERM(api::UNION, f, SOLVER->mkSingleton(args[i].getSort(), args[i]));
       }
     }
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index e7bb8795c..c154db399 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1216,6 +1216,13 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       parseError(
           "eqrange predicate requires option --arrays-exp to be enabled.");
     }
+    if (kind == api::SINGLETON && args.size() == 1)
+    {
+      api::Sort sort = args[0].getSort();
+      api::Term ret = d_solver->mkSingleton(sort, args[0]);
+      Debug("parser") << "applyParseOp: return singleton " << ret << std::endl;
+      return ret;
+    }
     api::Term ret = d_solver->mkTerm(kind, args);
     Debug("parser") << "applyParseOp: return default builtin " << ret
                     << std::endl;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9350111c7..6d75279e5 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -740,10 +740,10 @@ void Smt2Printer::toStream(std::ostream& out,
     out << smtKindString(k, d_variant) << " ";
     break;
   case kind::COMPREHENSION: out << smtKindString(k, d_variant) << " "; break;
+  case kind::SINGLETON: stillNeedToPrintParams = false; CVC4_FALLTHROUGH;
   case kind::MEMBER: typeChildren = true; CVC4_FALLTHROUGH;
   case kind::INSERT:
   case kind::SET_TYPE:
-  case kind::SINGLETON:
   case kind::COMPLEMENT:
   case kind::CHOOSE:
   case kind::IS_SINGLETON: out << smtKindString(k, d_variant) << " "; break;
@@ -976,7 +976,12 @@ void Smt2Printer::toStream(std::ostream& out,
       TypeNode elemType = TypeNode::leastCommonTypeNode( n[0].getType(), n[1].getType().getSetElementType() );
       force_child_type[0] = elemType;
       force_child_type[1] = NodeManager::currentNM()->mkSetType( elemType );
-    }else{
+    }
+    else if (n.getKind() == kind::SINGLETON)
+    {
+      force_child_type[0] = n.getType().getSetElementType();
+    }
+    else{
       // APPLY_UF, APPLY_CONSTRUCTOR, etc.
       Assert(n.hasOperator());
       TypeNode opt = n.getOperator().getType();
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 28731b371..2d6af9a63 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -676,7 +676,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) {
     Assert(i < d_setm_choice[sro].size());
     choice_i = d_setm_choice[sro][i];
     choices.push_back(choice_i);
-    Node sChoiceI = nm->mkNode(SINGLETON, choice_i);
+    Node sChoiceI = nm->mkSingleton(choice_i.getType(), choice_i);
     if (nsr.isNull())
     {
       nsr = sChoiceI;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 1b86afb85..ba9962bd9 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -965,7 +965,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       Trace("sygus-grammar-def") << "...add for singleton" << std::endl;
       std::vector<TypeNode> cargsSingleton;
       cargsSingleton.push_back(unresElemType);
-      sdts[i].addConstructor(SINGLETON, cargsSingleton);
+
+      // lambda x . (singleton (singleton_op T) x) where T = x.getType()
+      Node x = nm->mkBoundVar(etype);
+      Node vars = nm->mkNode(BOUND_VAR_LIST, x);
+      Node singleton = nm->mkSingleton(etype, x);
+      Node lambda = nm->mkNode(LAMBDA,vars, singleton);
+      sdts[i].addConstructor(lambda, "singleton", cargsSingleton);
 
       // add for union, difference, intersection
       std::vector<Kind> bin_kinds = {UNION, INTERSECTION, SETMINUS};
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 578d5faba..b18ae5b95 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -412,7 +412,8 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact)
     }
     else if (satom.getKind() == SEP_PTO)
     {
-      Node ss = nm->mkNode(SINGLETON, satom[0]);
+      // TODO(project##230): Find a safe type for the singleton operator
+      Node ss = nm->mkSingleton(satom[0].getType(), satom[0]);
       if (slbl != ss)
       {
         conc = slbl.eqNode(ss);
@@ -1341,7 +1342,7 @@ Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) {
     for( unsigned i=0; i<locs.size(); i++ ){
       Node s = locs[i];
       Assert(!s.isNull());
-      s = NodeManager::currentNM()->mkNode( kind::SINGLETON, s );
+      s = NodeManager::currentNM()->mkSingleton(tn, s);
       if( u.isNull() ){
         u = s;
       }else{
@@ -1512,12 +1513,14 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
       //check if this pto reference is in the base label, if not, then it does not need to be added as an assumption
       Assert(d_label_model.find(o_lbl) != d_label_model.end());
       Node vr = d_valuation.getModel()->getRepresentative( n[0] );
-      Node svr = NodeManager::currentNM()->mkNode( kind::SINGLETON, vr );
+      // TODO(project##230): Find a safe type for the singleton operator
+      Node svr = NodeManager::currentNM()->mkSingleton(vr.getType(), vr);
       bool inBaseHeap = std::find( d_label_model[o_lbl].d_heap_locs_model.begin(), d_label_model[o_lbl].d_heap_locs_model.end(), svr )!=d_label_model[o_lbl].d_heap_locs_model.end();
       Trace("sep-inst-debug") << "Is in base (non-instantiating) heap : " << inBaseHeap << " for value ref " << vr << " in " << o_lbl << std::endl;
       std::vector< Node > children;
       if( inBaseHeap ){
-        Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] );
+        // TODO(project##230): Find a safe type for the singleton operator
+        Node s = NodeManager::currentNM()->mkSingleton(n[0].getType(),  n[0]);
         children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, n[0], n[1] ), s ) );
       }else{
         //look up value of data
@@ -1529,8 +1532,10 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
         }else{
           Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl;
         }
-      } 
-      children.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] ), lbl_v ) );
+      }
+      // TODO(project##230): Find a safe type for the singleton operator
+      Node singleton = NodeManager::currentNM()->mkSingleton(n[0].getType(), n[0]);
+      children.push_back(singleton.eqNode(lbl_v));
       Node ret = children.empty() ? NodeManager::currentNM()->mkConst( true ) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) );
       Trace("sep-inst-debug") << "Return " << ret << std::endl;
       return ret;
@@ -1650,7 +1655,8 @@ void TheorySep::computeLabelModel( Node lbl ) {
       }else{
         tt = itm->second;
       }
-      Node stt = NodeManager::currentNM()->mkNode( kind::SINGLETON, tt );
+      // TODO(project##230): Find a safe type for the singleton operator
+      Node stt = NodeManager::currentNM()->mkSingleton(tt.getType(), tt);
       Trace("sep-process-debug") << "...model : add " << tt << " for " << u << " in lbl " << lbl << std::endl;
       d_label_model[lbl].d_heap_locs.push_back( stt );
     }
diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 87a849a78..78837508e 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -102,7 +102,9 @@ RewriteResponse TheorySepRewriter::postRewrite(TNode node) {
   switch (node.getKind()) {
     case kind::SEP_LABEL: {
       if( node[0].getKind()==kind::SEP_PTO ){
-        Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, node[0][0] );
+        // TODO(project##230): Find a safe type for the singleton operator
+        Node s = NodeManager::currentNM()->mkSingleton(node[0][0].getType(),
+                                                       node[0][0]);
         if( node[1]!=s ){
           Node c1 = node[1].eqNode( s );
           Node c2 = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, node[0][0], node[0][1] ), s );
diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 07672605d..21344ee73 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -1028,7 +1028,7 @@ void CardinalityExtension::mkModelValueElementsFor(
           // the current members of this finite type.
 
           Node slack = nm->mkSkolem("slack", elementType);
-          Node singleton = nm->mkNode(SINGLETON, slack);
+          Node singleton = nm->mkSingleton(elementType, slack);
           els.push_back(singleton);
           d_finite_type_slack_elements[elementType].push_back(slack);
           Trace("sets-model") << "Added slack element " << slack << " to set "
@@ -1037,7 +1037,7 @@ void CardinalityExtension::mkModelValueElementsFor(
         else
         {
           els.push_back(
-              nm->mkNode(SINGLETON, nm->mkSkolem("msde", elementType)));
+              nm->mkSingleton(elementType, nm->mkSkolem("msde", elementType)));
         }
       }
     }
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index fd941ab29..57120e42e 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -35,15 +35,23 @@ enumerator SET_TYPE \
     "theory/sets/theory_sets_type_enumerator.h"
 
 # operators
-operator UNION         2  "set union"
-operator INTERSECTION  2  "set intersection"
-operator SETMINUS      2  "set subtraction"
-operator SUBSET        2  "subset predicate; first parameter a subset of second"
-operator MEMBER        2  "set membership predicate; first parameter a member of second"
-operator SINGLETON     1  "the set of the single element given as a parameter"
-operator INSERT        2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
-operator CARD          1  "set cardinality operator"
-operator COMPLEMENT    1  "set COMPLEMENT (with respect to finite universe)"
+operator UNION          2  "set union"
+operator INTERSECTION   2  "set intersection"
+operator SETMINUS       2  "set subtraction"
+operator SUBSET         2  "subset predicate; first parameter a subset of second"
+operator MEMBER         2  "set membership predicate; first parameter a member of second"
+
+constant SINGLETON_OP \
+	::CVC4::SingletonOp \
+	::CVC4::SingletonOpHashFunction \
+	"theory/sets/singleton_op.h" \
+	"operator for singletons; payload is an instance of the CVC4::SingletonOp class"
+parameterized SINGLETON SINGLETON_OP 1  \
+"constructs a set of a single element. First parameter is a SingletonOp. Second is a term"
+
+operator INSERT         2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)"
+operator CARD           1  "set cardinality operator"
+operator COMPLEMENT     1  "set COMPLEMENT (with respect to finite universe)"
 nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it."
 
 # A set comprehension is specified by:
@@ -82,6 +90,7 @@ typerule INTERSECTION   ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 typerule SETMINUS       ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
 typerule SUBSET         ::CVC4::theory::sets::SubsetTypeRule
 typerule MEMBER         ::CVC4::theory::sets::MemberTypeRule
+typerule SINGLETON_OP   "SimpleTypeRule<RBuiltinOperator>"
 typerule SINGLETON      ::CVC4::theory::sets::SingletonTypeRule
 typerule EMPTYSET       ::CVC4::theory::sets::EmptySetTypeRule
 typerule INSERT         ::CVC4::theory::sets::InsertTypeRule
diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index 8989fbc15..2654344f3 100644
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -44,11 +44,13 @@ class NormalForm {
     }
     else
     {
+      TypeNode elementType = setType.getSetElementType();
       ElementsIterator it = elements.begin();
-      Node cur = nm->mkNode(kind::SINGLETON, *it);
+      Node cur = nm->mkSingleton(elementType, *it);
       while (++it != elements.end())
       {
-        cur = nm->mkNode(kind::UNION, nm->mkNode(kind::SINGLETON, *it), cur);
+        Node singleton = nm->mkSingleton(elementType, *it);
+        cur = nm->mkNode(kind::UNION, singleton, cur);
       }
       return cur;
     }
diff --git a/src/theory/sets/singleton_op.cpp b/src/theory/sets/singleton_op.cpp
new file mode 100644
index 000000000..d7f318314
--- /dev/null
+++ b/src/theory/sets/singleton_op.cpp
@@ -0,0 +1,50 @@
+/*********************                                                        */
+/*! \file singleton_op.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief a class for singleton operator for sets
+ **/
+
+#include "singleton_op.h"
+
+#include <iostream>
+
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const SingletonOp& op)
+{
+  return out << "(singleton_op " << op.getType() << ')';
+}
+
+size_t SingletonOpHashFunction::operator()(const SingletonOp& op) const
+{
+  return TypeNodeHashFunction()(op.getType());
+}
+
+SingletonOp::SingletonOp(const TypeNode& elementType)
+    : d_type(new TypeNode(elementType))
+{
+}
+
+SingletonOp::SingletonOp(const SingletonOp& op)
+    : d_type(new TypeNode(op.getType()))
+{
+}
+
+const TypeNode& SingletonOp::getType() const { return *d_type; }
+
+bool SingletonOp::operator==(const SingletonOp& op) const
+{
+  return getType() == op.getType();
+}
+
+}  // namespace CVC4
diff --git a/src/theory/sets/singleton_op.h b/src/theory/sets/singleton_op.h
new file mode 100644
index 000000000..57118999a
--- /dev/null
+++ b/src/theory/sets/singleton_op.h
@@ -0,0 +1,63 @@
+/*********************                                                        */
+/*! \file singleton_op.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief a class for singleton operator for sets
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__SINGLETON_OP_H
+#define CVC4__SINGLETON_OP_H
+
+#include <memory>
+
+namespace CVC4 {
+
+class TypeNode;
+
+/**
+ * The class is an operator for kind SINGLETON used to construct singleton sets.
+ * It specifies the type of the single element especially when it is a constant.
+ * e.g. the type of rational 1 is Int, however
+ * (singleton (singleton_op Real) 1) is of type (Set Real), not (Set Int).
+ * Note that the type passed to the constructor is the element's type, not the
+ * set type.
+ */
+class SingletonOp
+{
+ public:
+  SingletonOp(const TypeNode& elementType);
+  SingletonOp(const SingletonOp& op);
+
+  /** return the type of the current object */
+  const TypeNode& getType() const;
+
+  bool operator==(const SingletonOp& op) const;
+
+ private:
+  SingletonOp();
+  /** a pointer to the type of the singleton element */
+  std::unique_ptr<TypeNode> d_type;
+}; /* class Singleton */
+
+std::ostream& operator<<(std::ostream& out, const SingletonOp& op);
+
+/**
+ * Hash function for the SingletonHashFunction objects.
+ */
+struct CVC4_PUBLIC SingletonOpHashFunction
+{
+  size_t operator()(const SingletonOp& op) const;
+}; /* struct SingletonOpHashFunction */
+
+}  // namespace CVC4
+
+#endif /* CVC4__SINGLETON_OP_H */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 51f49ad1d..18df43e9f 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1143,9 +1143,10 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
         const std::map<Node, Node>& emems = d_state.getMembers(eqc);
         if (!emems.empty())
         {
+          TypeNode elementType = eqc.getType().getSetElementType();
           for (const std::pair<const Node, Node>& itmm : emems)
           {
-            Node t = nm->mkNode(kind::SINGLETON, itmm.first);
+            Node t = nm->mkSingleton(elementType, itmm.first);
             els.push_back(t);
           }
         }
@@ -1357,7 +1358,7 @@ TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node)
 
   TypeNode setType = set.getType();
   Node boundVar = nm->mkBoundVar(setType.getSetElementType());
-  Node singleton = nm->mkNode(kind::SINGLETON, boundVar);
+  Node singleton = nm->mkSingleton(setType.getSetElementType(), boundVar);
   Node equal = set.eqNode(singleton);
   std::vector<Node> variables = {boundVar};
   Node boundVars = nm->mkNode(BOUND_VAR_LIST, variables);
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index ebbc24d12..617b458c9 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -247,12 +247,13 @@ void TheorySetsRels::check(Theory::Effort level)
         }
         else if (erType.isTuple() && !eqc_node.isConst() && !eqc_node.isVar())
         {
+          std::vector<TypeNode> tupleTypes = erType.getTupleTypes();
           for (unsigned i = 0, tlen = erType.getTupleLength(); i < tlen; i++)
           {
-            Node element = RelsUtils::nthElementOfTuple( eqc_node, i );
-
-            if( !element.isConst() ) {
-              makeSharedTerm( element );
+            Node element = RelsUtils::nthElementOfTuple(eqc_node, i);
+            if (!element.isConst())
+            {
+              makeSharedTerm(element, tupleTypes[i]);
             }
           }
         }
@@ -863,7 +864,7 @@ void TheorySetsRels::check(Theory::Effort level)
     sendInfer(fact, reason, "JOIN-Split-1");
     fact = NodeManager::currentNM()->mkNode(kind::MEMBER, mem2, join_rel[1]);
     sendInfer(fact, reason, "JOIN-Split-2");
-    makeSharedTerm( shared_x );
+    makeSharedTerm(shared_x, shared_type);
   }
 
   /*
@@ -1153,8 +1154,9 @@ void TheorySetsRels::check(Theory::Effort level)
       }
       return equal;
     } else if(!a.getType().isBoolean()){
-      makeSharedTerm(a);
-      makeSharedTerm(b);
+      // TODO(project##230): Find a safe type for the singleton operator
+      makeSharedTerm(a, a.getType());
+      makeSharedTerm(b, b.getType());
     }
     return false;
   }
@@ -1183,14 +1185,15 @@ void TheorySetsRels::check(Theory::Effort level)
     return false;
   }
 
-  void TheorySetsRels::makeSharedTerm( Node n ) {
+  void TheorySetsRels::makeSharedTerm(Node n, TypeNode t)
+  {
     if (d_shared_terms.find(n) != d_shared_terms.end())
     {
       return;
     }
     Trace("rels-share") << " [sets-rels] making shared term " << n << std::endl;
     // force a proxy lemma to be sent for the singleton containing n
-    Node ss = NodeManager::currentNM()->mkNode(SINGLETON, n);
+    Node ss = NodeManager::currentNM()->mkSingleton(t, n);
     d_treg.getProxy(ss);
     d_shared_terms.insert(n);
   }
@@ -1216,9 +1219,11 @@ void TheorySetsRels::check(Theory::Effort level)
       Trace("rels-debug") << "[Theory::Rels] Reduce tuple var: " << n[0] << " to a concrete one " << " node = " << n << std::endl;
       std::vector<Node> tuple_elements;
       tuple_elements.push_back((n[0].getType().getDType())[0].getConstructor());
-      for(unsigned int i = 0; i < n[0].getType().getTupleLength(); i++) {
+      std::vector<TypeNode> tupleTypes = n[0].getType().getTupleTypes();
+      for (unsigned int i = 0; i < n[0].getType().getTupleLength(); i++)
+      {
         Node element = RelsUtils::nthElementOfTuple(n[0], i);
-        makeSharedTerm(element);
+        makeSharedTerm(element, tupleTypes[i]);
         tuple_elements.push_back(element);
       }
       Node tuple_reduct = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, tuple_elements);
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 9b8fd0cb7..95a13f4d5 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -176,7 +176,7 @@ private:
 
   /** Helper functions */
   bool hasTerm( Node a );
-  void makeSharedTerm( Node );
+  void makeSharedTerm(Node, TypeNode t);
   void reduceTupleVar( Node );
   bool hasMember( Node, Node );
   void computeTupleReps( Node );
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index d821a0059..847bf34eb 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -161,7 +161,7 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
                             std::inserter(newSet, newSet.begin()));
       Node newNode = NormalForm::elementsToSet(newSet, node.getType());
-      Assert(newNode.isConst());
+      Assert(newNode.isConst() && newNode.getType() == node.getType());
       Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
       return RewriteResponse(REWRITE_DONE, newNode);
     }
@@ -488,12 +488,14 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
   }
   else if (k == kind::INSERT)
   {
-    Node insertedElements = nm->mkNode(kind::SINGLETON, node[0]);
     size_t setNodeIndex =  node.getNumChildren()-1;
-    for(size_t i = 1; i < setNodeIndex; ++i) {
-      insertedElements = nm->mkNode(kind::UNION, 
-                                    insertedElements,
-                                    nm->mkNode(kind::SINGLETON, node[i]));
+    TypeNode elementType = node[setNodeIndex].getType().getSetElementType();
+    Node insertedElements = nm->mkSingleton(elementType, node[0]);
+
+    for (size_t i = 1; i < setNodeIndex; ++i)
+    {
+      Node singleton = nm->mkSingleton(elementType, node[i]);
+      insertedElements = nm->mkNode(kind::UNION, insertedElements, singleton);
     }
     return RewriteResponse(REWRITE_AGAIN, 
                            nm->mkNode(kind::UNION,
diff --git a/src/theory/sets/theory_sets_type_enumerator.cpp b/src/theory/sets/theory_sets_type_enumerator.cpp
index 321b9ffcd..1d932b590 100644
--- a/src/theory/sets/theory_sets_type_enumerator.cpp
+++ b/src/theory/sets/theory_sets_type_enumerator.cpp
@@ -89,7 +89,8 @@ SetEnumerator& SetEnumerator::operator++()
     // get a new element and return it as a singleton set
     Node element = *d_elementEnumerator;
     d_elementsSoFar.push_back(element);
-    d_currentSet = d_nodeManager->mkNode(kind::SINGLETON, element);
+    TypeNode elementType = d_elementEnumerator.getType();
+    d_currentSet = d_nodeManager->mkSingleton(elementType, element);
     d_elementEnumerator++;
   }
   else
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 3e2834aaf..20e5e57e2 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -31,9 +31,8 @@ struct SetsBinaryOperatorTypeRule
                                      TNode n,
                                      bool check)
   {
-    Assert(n.getKind() == kind::UNION ||
-           n.getKind() == kind::INTERSECTION ||
-           n.getKind() == kind::SETMINUS);
+    Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION
+           || n.getKind() == kind::SETMINUS);
     TypeNode setType = n[0].getType(check);
     if (check)
     {
@@ -45,19 +44,11 @@ struct SetsBinaryOperatorTypeRule
       TypeNode secondSetType = n[1].getType(check);
       if (secondSetType != setType)
       {
-        if (n.getKind() == kind::INTERSECTION)
-        {
-          setType = TypeNode::mostCommonTypeNode(secondSetType, setType);
-        }
-        else
-        {
-          setType = TypeNode::leastCommonTypeNode(secondSetType, setType);
-        }
-        if (setType.isNull())
-        {
-          throw TypeCheckingExceptionPrivate(
-              n, "operator expects two sets of comparable types");
-        }
+        std::stringstream ss;
+        ss << "Operator " << n.getKind()
+           << " expects two sets of the same type. Found types '" << setType
+           << "' and '" << secondSetType << "'.";
+        throw TypeCheckingExceptionPrivate(n, ss.str());
       }
     }
     return setType;
@@ -132,18 +123,40 @@ struct MemberTypeRule {
   }
 };/* struct MemberTypeRule */
 
-struct SingletonTypeRule {
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+struct SingletonTypeRule
+{
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
   {
-    Assert(n.getKind() == kind::SINGLETON);
-    return nodeManager->mkSetType(n[0].getType(check));
+    Assert(n.getKind() == kind::SINGLETON && n.hasOperator()
+           && n.getOperator().getKind() == kind::SINGLETON_OP);
+
+    SingletonOp op = n.getOperator().getConst<SingletonOp>();
+    TypeNode type1 = op.getType();
+    if (check)
+    {
+      TypeNode type2 = n[0].getType(check);
+      TypeNode leastCommonType = TypeNode::leastCommonTypeNode(type1, type2);
+      // the type of the element should be a subtype of the type of the operator
+      // e.g. (singleton (singleton_op Real) 1) where 1 is an Int
+      if (leastCommonType.isNull() || leastCommonType != type1)
+      {
+        std::stringstream ss;
+        ss << "The type '" << type2 << "' of the element is not a subtype of '"
+           << type1 << "' in term : " << n;
+        throw TypeCheckingExceptionPrivate(n, ss.str());
+      }
+    }
+    return nodeManager->mkSetType(type1);
   }
 
-  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+  inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
+  {
     Assert(n.getKind() == kind::SINGLETON);
     return n[0].isConst();
   }
-};/* struct SingletonTypeRule */
+}; /* struct SingletonTypeRule */
 
 struct EmptySetTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)