From ac8b2593bed81125cb1a494e4b8311e517d0e3d9 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Thu, 5 Nov 2020 17:13:44 -0600 Subject: [PATCH] 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 --- examples/api/python/sets.py | 6 +- examples/api/sets.cpp | 6 +- src/api/cvc4cpp.cpp | 178 +++++------------- src/api/cvc4cpp.h | 20 +- src/api/python/cvc4.pxd | 1 - src/api/python/cvc4.pxi | 4 - src/parser/cvc/Cvc.g | 4 +- src/parser/smt2/smt2.cpp | 3 +- src/theory/arith/nl/nonlinear_extension.cpp | 1 - .../theory/theory_sets_type_rules_white.h | 7 +- 10 files changed, 64 insertions(+), 166 deletions(-) diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py index 77de3e5b3..e4350ea1b 100644 --- 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 549b68e0d..f8053a756 100644 --- 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 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) diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 81319e25a..b62fb0bbb 100644 --- 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 edeb47f06..a8a2eb27a 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1163,8 +1163,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& 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 f5e83c8f0..5bd02cf19 100644 --- 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& 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 f06c1f77d..66c8dc123 100644 --- 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))) -- 2.30.2