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

11 files changed, 202 insertions, 56 deletions

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)