Remove mkSingleton from the API (#5366)

This PR removes mkSingleton from the API after removing subtyping from set theory and introducing mkInteger to the API.
Instead the user needs to use Solver::mkTerm(api::SINGLETON, element) where element has the right type.
Internally NodeManager::mkSingleton(type, element) is still needed to determine the type of the set.
Other changes:

Renamed Solver::mkTerm(Op op, .. functions to Solver::mkTermFromOp(Op op, ...
Added mkTermFromOp to the python API

diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py
index 77de3e5b31340b44a2f6500eec42bf924465ab60..e4350ea1b8b4ed755af470c164d2f2342c0a06cc 100644 (file)
--- a/examples/api/python/sets.py
+++ b/examples/api/python/sets.py
@@ -66,9 +66,9 @@ if __name__ == "__main__":
     two = slv.mkInteger(2)
     three = slv.mkInteger(3)
 
-    singleton_one = slv.mkSingleton(integer, one)
-    singleton_two = slv.mkSingleton(integer, two)
-    singleton_three = slv.mkSingleton(integer, three)
+    singleton_one = slv.mkTerm(kinds.Singleton, one)
+    singleton_two = slv.mkTerm(kinds.Singleton, two)
+    singleton_three = slv.mkTerm(kinds.Singleton, three)
     one_two = slv.mkTerm(kinds.Union, singleton_one, singleton_two)
     two_three = slv.mkTerm(kinds.Union, singleton_two, singleton_three)
     intersection = slv.mkTerm(kinds.Intersection, one_two, two_three)

diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index 549b68e0dbbbc08f60247ab97012796eefdc71ba..f8053a756fbb1adeab4c82c1ca4a33eb90e8419a 100644 (file)
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -73,9 +73,9 @@ int main()
     Term two = slv.mkInteger(2);
     Term three = slv.mkInteger(3);
 
-    Term singleton_one = slv.mkSingleton(integer, one);
-    Term singleton_two = slv.mkSingleton(integer, two);
-    Term singleton_three = slv.mkSingleton(integer, three);
+    Term singleton_one = slv.mkTerm(SINGLETON, one);
+    Term singleton_two = slv.mkTerm(SINGLETON, two);
+    Term singleton_three = slv.mkTerm(SINGLETON, three);
     Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two);
     Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three);
     Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three);

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 2c694dbedfb39ef0f4cfafacc8ce81bd111955c1..bbe5b5459cefa9ebd106a46ac5f9005bca98488d 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3273,7 +3273,23 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
   {
     // default case, same as above
     checkMkTerm(kind, children.size());
-    res = d_exprMgr->mkExpr(k, echildren);
+    if (kind == api::SINGLETON)
+    {
+      // the type of the term is the same as the type of the internal node
+      // see Term::getSort()
+      TypeNode type = children[0].d_node->getType();
+      // Internally NodeManager::mkSingleton needs a type argument
+      // to construct a singleton, since there is no difference between
+      // integers and reals (both are Rationals).
+      // At the API, mkReal and mkInteger are different and therefore the
+      // element type can be used safely here.
+      Node singleton = getNodeManager()->mkSingleton(type, *children[0].d_node);
+      res = Term(this, singleton).getExpr();
+    }
+    else
+    {
+      res = d_exprMgr->mkExpr(k, echildren);
+    }
   }
 
   (void)res.getType(true); /* kick off type checking */
@@ -3838,22 +3854,6 @@ 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);
-
-  Node res = getNodeManager()->mkSingleton(*s.d_type, *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;
@@ -4197,35 +4197,12 @@ Term Solver::mkTerm(Kind kind) const
 
 Term Solver::mkTerm(Kind kind, Term child) const
 {
-  NodeManagerScope scope(getNodeManager());
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
-  CVC4_API_SOLVER_CHECK_TERM(child);
-  checkMkTerm(kind, 1);
-
-  Node res = getNodeManager()->mkNode(extToIntKind(kind), *child.d_node);
-  (void)res.getType(true); /* kick off type checking */
-  return Term(this, res);
-
-  CVC4_API_SOLVER_TRY_CATCH_END;
+  return mkTermHelper(kind, std::vector<Term>{child});
 }
 
 Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
 {
-  NodeManagerScope scope(getNodeManager());
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
-  CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
-  CVC4_API_SOLVER_CHECK_TERM(child1);
-  CVC4_API_SOLVER_CHECK_TERM(child2);
-  checkMkTerm(kind, 2);
-
-  Node res = getNodeManager()->mkNode(
-      extToIntKind(kind), *child1.d_node, *child2.d_node);
-  (void)res.getType(true); /* kick off type checking */
-  return Term(this, res);
-
-  CVC4_API_SOLVER_TRY_CATCH_END;
+  return mkTermHelper(kind, std::vector<Term>{child1, child2});
 }
 
 Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const
@@ -4246,17 +4223,14 @@ Term Solver::mkTerm(Op op) const
   CVC4_API_SOLVER_CHECK_OP(op);
   checkMkTerm(op.d_kind, 0);
 
-  Term res;
-  if (op.isIndexedHelper())
-  {
-    const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-    res = Term(this, getNodeManager()->mkNode(int_kind, *op.d_node));
-  }
-  else
+  if (!op.isIndexedHelper())
   {
-    res = mkTermFromKind(op.d_kind);
+    return mkTermFromKind(op.d_kind);
   }
 
+  const CVC4::Kind int_kind = extToIntKind(op.d_kind);
+  Term res = Term(this, getNodeManager()->mkNode(int_kind, *op.d_node));
+
   (void)res.d_node->getType(true); /* kick off type checking */
   return res;
 
@@ -4265,92 +4239,31 @@ Term Solver::mkTerm(Op op) const
 
 Term Solver::mkTerm(Op op, Term child) const
 {
-  NodeManagerScope scope(getNodeManager());
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_SOLVER_CHECK_OP(op);
-  CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
-  CVC4_API_SOLVER_CHECK_TERM(child);
-  checkMkTerm(op.d_kind, 1);
-
-  const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-  Node res;
-  if (op.isIndexedHelper())
-  {
-    res = getNodeManager()->mkNode(int_kind, *op.d_node, *child.d_node);
-  }
-  else
-  {
-    res = getNodeManager()->mkNode(int_kind, *child.d_node);
-  }
-
-  (void)res.getType(true); /* kick off type checking */
-  return Term(this, res);
-
-  CVC4_API_SOLVER_TRY_CATCH_END;
+  return mkTermHelper(op, std::vector<Term>{child});
 }
 
 Term Solver::mkTerm(Op op, Term child1, Term child2) const
 {
-  NodeManagerScope scope(getNodeManager());
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_SOLVER_CHECK_OP(op);
-  CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
-  CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
-  CVC4_API_SOLVER_CHECK_TERM(child1);
-  CVC4_API_SOLVER_CHECK_TERM(child2);
-  checkMkTerm(op.d_kind, 2);
-
-  const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-  Node res;
-  if (op.isIndexedHelper())
-  {
-    res = getNodeManager()->mkNode(
-        int_kind, *op.d_node, *child1.d_node, *child2.d_node);
-  }
-  else
-  {
-    res = getNodeManager()->mkNode(int_kind, *child1.d_node, *child2.d_node);
-  }
-
-  (void)res.getType(true); /* kick off type checking */
-  return Term(this, res);
-  CVC4_API_SOLVER_TRY_CATCH_END;
+  return mkTermHelper(op, std::vector<Term>{child1, child2});
 }
 
 Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
 {
-  NodeManagerScope scope(getNodeManager());
-  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_SOLVER_CHECK_OP(op);
-  CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
-  CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
-  CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
-  CVC4_API_SOLVER_CHECK_TERM(child1);
-  CVC4_API_SOLVER_CHECK_TERM(child2);
-  CVC4_API_SOLVER_CHECK_TERM(child3);
-  checkMkTerm(op.d_kind, 3);
-
-  const CVC4::Kind int_kind = extToIntKind(op.d_kind);
-  Node res;
-  if (op.isIndexedHelper())
-  {
-    res = getNodeManager()->mkNode(
-        int_kind, *op.d_node, *child1.d_node, *child2.d_node, *child3.d_node);
-  }
-  else
-  {
-    res = getNodeManager()->mkNode(
-        int_kind, *child1.d_node, *child2.d_node, *child3.d_node);
-  }
-
-  (void)res.getType(true); /* kick off type checking */
-  return Term(this, res);
-
-  CVC4_API_SOLVER_TRY_CATCH_END;
+  return mkTermHelper(op, std::vector<Term>{child1, child2, child3});
 }
 
 Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
 {
+  return mkTermHelper(op, children);
+}
+
+Term Solver::mkTermHelper(const Op& op, const std::vector<Term>& children) const
+{
+  if (!op.isIndexedHelper())
+  {
+    return mkTermHelper(op.d_kind, children);
+  }
+
   NodeManagerScope scope(getNodeManager());
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_SOLVER_CHECK_OP(op);
@@ -4367,18 +4280,11 @@ Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
 
   const CVC4::Kind int_kind = extToIntKind(op.d_kind);
   std::vector<Node> echildren = termVectorToNodes(children);
-  Node res;
-  if (op.isIndexedHelper())
-  {
-    NodeBuilder<> nb(int_kind);
-    nb << *op.d_node;
-    nb.append(echildren);
-    res = nb.constructNode();
-  }
-  else
-  {
-    res = getNodeManager()->mkNode(int_kind, echildren);
-  }
+
+  NodeBuilder<> nb(int_kind);
+  nb << *op.d_node;
+  nb.append(echildren);
+  Node res = nb.constructNode();
 
   (void)res.getType(true); /* kick off type checking */
   return Term(this, res);

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 33d87af91eb1966a0a5e4d13b1ace22531943b3c..ae6384e91a7f0f23778b8c5f0c4a8b1b6af68e12 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2475,8 +2475,7 @@ class CVC4_PUBLIC Solver
   /**
    * Create n-ary term of given kind from a given operator.
    * Create operators with mkOp().
-   * @param kind the kind of the term
-   * @param the operator
+   * @param op the operator
    * @children the children of the term
    * @return the Term
    */
@@ -2638,15 +2637,6 @@ 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.
@@ -3491,6 +3481,14 @@ class CVC4_PUBLIC Solver
    */
   Term mkTermHelper(Kind kind, const std::vector<Term>& children) const;
 
+  /**
+   * Create n-ary term of given kind from a given operator.
+   * @param op the operator
+   * @param children the children of the term
+   * @return the Term
+   */
+  Term mkTermHelper(const Op& op, const std::vector<Term>& children) const;
+
   /**
    * Create a vector of datatype sorts, using unresolved sorts.
    * @param dtypedecls the datatype declarations from which the sort is created

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index 113895ad7abcc35a079354721cb03aacf99a8975..13f4606daa655b681ceb7a12e16dc28541334f6b 100644 (file)
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -178,7 +178,6 @@ 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 4cdd60893ed7ba4f684ebd8e0d72f090d258dbb1..16f4543112a8ea496d526d6c3fd6ce2506cda691 100644 (file)
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -697,10 +697,6 @@ 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)

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 81319e25a351592b2405ed2cf337a267e1b7ab50..b62fb0bbb44c495d37a7f3a440a665995dd5de69 100644 (file)
--- 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 = SOLVER->mkSingleton(args[0].getSort(), args[0]);
+    { f = MK_TERM(api::SINGLETON, args[0]);
       for(size_t i = 1; i < args.size(); ++i) {
-        f = MK_TERM(api::UNION, f, SOLVER->mkSingleton(args[i].getSort(), args[i]));
+        f = MK_TERM(api::UNION, f, MK_TERM(api::SINGLETON, args[i]));
       }
     }
 

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index edeb47f06d5f25e92a07c13a8fc9f539de04e4c6..a8a2eb27a5cc133a2a11bb0c42ba18217ff1d208 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1163,8 +1163,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     }
     if (kind == api::SINGLETON && args.size() == 1)
     {
-      api::Sort sort = args[0].getSort();
-      api::Term ret = d_solver->mkSingleton(sort, args[0]);
+      api::Term ret = d_solver->mkTerm(api::SINGLETON, args[0]);
       Debug("parser") << "applyParseOp: return singleton " << ret << std::endl;
       return ret;
     }

diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index f5e83c8f0abd7dc7e4a33cbf00dec57a83202b06..5bd02cf192cb6d389405381a15e6477fc9bed307 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -179,7 +179,6 @@ void NonlinearExtension::getAssertions(std::vector<Node>& assertions)
     useRelevance = true;
   }
   Valuation v = d_containing.getValuation();
-  NodeManager* nm = NodeManager::currentNM();
 
   BoundInference bounds;
 

diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h
index f06c1f77d67bbecfb55c23a6b12b5492f0b6f8a6..66c8dc123fee77254f42a4edb2f63c001f3ac33b 100644 (file)
--- a/test/unit/theory/theory_sets_type_rules_white.h
+++ b/test/unit/theory/theory_sets_type_rules_white.h
@@ -56,9 +56,10 @@ class SetsTypeRuleWhite : public CxxTest::TestSuite
     Sort realSort = d_slv->getRealSort();
     Sort intSort = d_slv->getIntegerSort();
     Term emptyReal = d_slv->mkEmptySet(d_slv->mkSetSort(realSort));
-    Term one = d_slv->mkInteger(1);
-    Term singletonInt = d_slv->mkSingleton(intSort, one);
-    Term singletonReal = d_slv->mkSingleton(realSort, one);
+    Term integerOne = d_slv->mkInteger(1);
+    Term realOne = d_slv->mkReal(1);
+    Term singletonInt = d_slv->mkTerm(api::SINGLETON, integerOne);
+    Term singletonReal = d_slv->mkTerm(api::SINGLETON, realOne);
     // (union
     //    (singleton (singleton_op Int) 1)
     //    (as emptyset (Set Real)))