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

1 files changed, 50 insertions, 0 deletions

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