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

4 files changed, 32 insertions, 0 deletions

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)