From ac8b2593bed81125cb1a494e4b8311e517d0e3d9 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Thu, 5 Nov 2020 17:13:44 -0600 Subject: 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 --- src/api/cvc4cpp.cpp | 178 ++++++++++++------------------------------------ src/api/cvc4cpp.h | 20 +++--- src/api/python/cvc4.pxd | 1 - src/api/python/cvc4.pxi | 4 -- 4 files changed, 51 insertions(+), 152 deletions(-) (limited to 'src/api') diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 2c694dbed..bbe5b5459 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3273,7 +3273,23 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& 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{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{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{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{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{child1, child2, child3}); } Term Solver::mkTerm(Op op, const std::vector& children) const { + return mkTermHelper(op, children); +} + +Term Solver::mkTermHelper(const Op& op, const std::vector& 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& children) const const CVC4::Kind int_kind = extToIntKind(op.d_kind); std::vector 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 33d87af91..ae6384e91 100644 --- 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& 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& 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 113895ad7..13f4606da 100644 --- 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 4cdd60893..16f454311 100644 --- 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) -- cgit v1.2.3