From: Aina Niemetz Date: Thu, 4 Mar 2021 01:58:33 +0000 (-0800) Subject: New C++ API: Clean up usage of internal Type/TypeNodes. (#6044) X-Git-Tag: cvc5-1.0.0~2159 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=786b9ab247b938a10f0b944d28d448ddb2f4f974;p=cvc5.git New C++ API: Clean up usage of internal Type/TypeNodes. (#6044) This disables the temporarily available internals of Sort. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index a426c9270..380a427ff 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1008,6 +1008,38 @@ Sort::~Sort() } } +std::set Sort::sortSetToTypeNodes(const std::set& sorts) +{ + std::set types; + for (const Sort& s : sorts) + { + types.insert(s.getTypeNode()); + } + return types; +} + +std::vector Sort::sortVectorToTypeNodes( + const std::vector& sorts) +{ + std::vector typeNodes; + for (const Sort& sort : sorts) + { + typeNodes.push_back(sort.getTypeNode()); + } + return typeNodes; +} + +std::vector Sort::typeNodeVectorToSorts( + const Solver* slv, const std::vector& types) +{ + std::vector sorts; + for (size_t i = 0, tsize = types.size(); i < tsize; i++) + { + sorts.push_back(Sort(slv, types[i])); + } + return sorts; +} + /* Helpers */ /* -------------------------------------------------------------------------- */ @@ -1144,14 +1176,6 @@ std::string Sort::toString() const return d_type->toString(); } -// !!! This is only temporarily available until the parser is fully migrated -// to the new API. !!! -CVC4::Type Sort::getType(void) const -{ - if (d_type->isNull()) return Type(); - NodeManagerScope scope(d_solver->getNodeManager()); - return d_type->toType(); -} const CVC4::TypeNode& Sort::getTypeNode(void) const { return *d_type; } /* Constructor sort ------------------------------------------------------- */ @@ -2359,7 +2383,7 @@ DatatypeDecl::DatatypeDecl(const Solver* slv, bool isCoDatatype) : d_solver(slv) { - std::vector tparams = sortVectorToTypeNodes(params); + std::vector tparams = Sort::sortVectorToTypeNodes(params); d_dtype = std::shared_ptr( new CVC4::DType(name, tparams, isCoDatatype)); } @@ -3131,7 +3155,7 @@ void Grammar::addSygusConstructorTerm( d_solver->getExprManager()->mkExpr( CVC4::kind::LAMBDA, {lbvl.d_node->toExpr(), op.d_node->toExpr()})); } - std::vector cargst = sortVectorToTypeNodes(cargs); + std::vector cargst = Sort::sortVectorToTypeNodes(cargs); dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst); } @@ -3513,10 +3537,10 @@ std::vector Solver::mkDatatypeSortsInternal( CVC4_API_SOLVER_CHECK_SORT(sort); } - std::set utypes = sortSetToTypeNodes(unresolvedSorts); + std::set utypes = Sort::sortSetToTypeNodes(unresolvedSorts); std::vector dtypes = getNodeManager()->mkMutualDatatypeTypes(datatypes, utypes); - std::vector retTypes = typeNodeVectorToSorts(this, dtypes); + std::vector retTypes = Sort::typeNodeVectorToSorts(this, dtypes); return retTypes; CVC4_API_SOLVER_TRY_CATCH_END; @@ -3525,18 +3549,6 @@ std::vector Solver::mkDatatypeSortsInternal( /* Helpers for converting vectors. */ /* .......................................................................... */ -std::vector Solver::sortVectorToTypes( - const std::vector& sorts) const -{ - std::vector res; - for (const Sort& s : sorts) - { - CVC4_API_SOLVER_CHECK_SORT(s); - res.push_back(s.d_type->toType()); - } - return res; -} - std::vector Solver::termVectorToExprs( const std::vector& terms) const { @@ -3760,7 +3772,7 @@ Sort Solver::mkFunctionSort(const std::vector& sorts, Sort codomain) const << "first-class sort as codomain sort for function sort"; Assert(!codomain.isFunction()); /* A function sort is not first-class. */ - std::vector argTypes = sortVectorToTypeNodes(sorts); + std::vector argTypes = Sort::sortVectorToTypeNodes(sorts); return Sort(this, getNodeManager()->mkFunctionType(argTypes, *codomain.d_type)); @@ -3795,7 +3807,7 @@ Sort Solver::mkPredicateSort(const std::vector& sorts) const sorts[i].isFirstClass(), "parameter sort", sorts[i], i) << "first-class sort as parameter sort for predicate sort"; } - std::vector types = sortVectorToTypeNodes(sorts); + std::vector types = Sort::sortVectorToTypeNodes(sorts); return Sort(this, getNodeManager()->mkPredicateType(types)); @@ -3901,7 +3913,7 @@ Sort Solver::mkTupleSort(const std::vector& sorts) const !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i) << "non-function-like sort as parameter sort for tuple sort"; } - std::vector typeNodes = sortVectorToTypeNodes(sorts); + std::vector typeNodes = Sort::sortVectorToTypeNodes(sorts); return Sort(this, getNodeManager()->mkTupleType(typeNodes)); CVC4_API_SOLVER_TRY_CATCH_END; @@ -4969,7 +4981,7 @@ Term Solver::declareFun(const std::string& symbol, TypeNode type = *sort.d_type; if (!sorts.empty()) { - std::vector types = sortVectorToTypeNodes(sorts); + std::vector types = Sort::sortVectorToTypeNodes(sorts); type = getNodeManager()->mkFunctionType(types, type); } return Term(this, d_exprMgr->mkVar(symbol, type.toType())); @@ -6058,36 +6070,6 @@ std::vector termVectorToNodes(const std::vector& terms) return res; } -std::vector sortVectorToTypes(const std::vector& sorts) -{ - std::vector types; - for (size_t i = 0, ssize = sorts.size(); i < ssize; i++) - { - types.push_back(sorts[i].getTypeNode().toType()); - } - return types; -} - -std::vector sortVectorToTypeNodes(const std::vector& sorts) -{ - std::vector typeNodes; - for (const Sort& sort : sorts) - { - typeNodes.push_back(sort.getTypeNode()); - } - return typeNodes; -} - -std::set sortSetToTypeNodes(const std::set& sorts) -{ - std::set types; - for (const Sort& s : sorts) - { - types.insert(s.getTypeNode()); - } - return types; -} - std::vector exprVectorToTerms(const Solver* slv, const std::vector& exprs) { @@ -6099,27 +6081,6 @@ std::vector exprVectorToTerms(const Solver* slv, return terms; } -std::vector typeVectorToSorts(const Solver* slv, - const std::vector& types) -{ - std::vector sorts; - for (size_t i = 0, tsize = types.size(); i < tsize; i++) - { - sorts.push_back(Sort(slv, TypeNode::fromType(types[i]))); - } - return sorts; -} -std::vector typeNodeVectorToSorts(const Solver* slv, - const std::vector& types) -{ - std::vector sorts; - for (size_t i = 0, tsize = types.size(); i < tsize; i++) - { - sorts.push_back(Sort(slv, types[i])); - } - return sorts; -} - } // namespace api /* -------------------------------------------------------------------------- */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index f68fe4c0b..00326204e 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -40,11 +40,18 @@ template class NodeTemplate; typedef NodeTemplate Node; class Expr; +class DatatypeDeclarationCommand; +class DeclareFunctionCommand; +class DeclareHeapCommand; +class DeclareSortCommand; +class DeclareSygusVarCommand; +class DefineSortCommand; class DType; class DTypeConstructor; class DTypeSelector; class ExprManager; class GetAbductCommand; +class GetModelCommand; class GetInterpolCommand; class NodeManager; class SmtEngine; @@ -223,8 +230,19 @@ class Datatype; */ class CVC4_PUBLIC Sort { + friend class CVC4::DatatypeDeclarationCommand; + friend class CVC4::DeclareFunctionCommand; + friend class CVC4::DeclareHeapCommand; + friend class CVC4::DeclareSortCommand; + friend class CVC4::DeclareSygusVarCommand; + friend class CVC4::DefineSortCommand; + friend class CVC4::GetAbductCommand; + friend class CVC4::GetInterpolCommand; + friend class CVC4::GetModelCommand; + friend class CVC4::SynthFunCommand; friend class DatatypeConstructor; friend class DatatypeConstructorDecl; + friend class DatatypeSelector; friend class DatatypeDecl; friend class Op; friend class Solver; @@ -233,17 +251,6 @@ class CVC4_PUBLIC Sort friend class Term; public: - // !!! This constructor is only temporarily public until the parser is fully - // migrated to the new API. !!! - /** - * Constructor. - * @param slv the associated solver object - * @param t the internal type that is to be wrapped by this sort - * @return the Sort - */ - Sort(const Solver* slv, const CVC4::Type& t); - Sort(const Solver* slv, const CVC4::TypeNode& t); - /** * Constructor. */ @@ -519,11 +526,6 @@ class CVC4_PUBLIC Sort */ std::string toString() const; - // !!! This is only temporarily available until the parser is fully migrated - // to the new API. !!! - CVC4::Type getType(void) const; - const CVC4::TypeNode& getTypeNode(void) const; - /* Constructor sort ------------------------------------------------------- */ /** @@ -688,6 +690,27 @@ class CVC4_PUBLIC Sort std::vector getTupleSorts() const; private: + /** @return the internal wrapped TypeNode of this sort. */ + const CVC4::TypeNode& getTypeNode(void) const; + + /** Helper to convert a set of Sorts to internal TypeNodes. */ + std::set static sortSetToTypeNodes(const std::set& sorts); + /* Helper to convert a vector of Sorts to internal TypeNodes. */ + std::vector static sortVectorToTypeNodes( + const std::vector& sorts); + /** Helper to convert a vector of internal TypeNodes to Sorts. */ + std::vector static typeNodeVectorToSorts( + const Solver* slv, const std::vector& types); + + /** + * Constructor. + * @param slv the associated solver object + * @param t the internal type that is to be wrapped by this sort + * @return the Sort + */ + Sort(const Solver* slv, const CVC4::Type& t); + Sort(const Solver* slv, const CVC4::TypeNode& t); + /** * Helper for isNull checks. This prevents calling an API function with * CVC4_API_CHECK_NOT_NULL @@ -3530,9 +3553,7 @@ class CVC4_PUBLIC Solver Options& getOptions(void); private: - /* Helper to convert a vector of internal types to sorts. */ - std::vector sortVectorToTypes(const std::vector& vector) const; - /* Helper to convert a vector of sorts to internal types. */ + /* Helper to convert a vector of Terms to internal Exprs. */ std::vector termVectorToExprs(const std::vector& vector) const; /* Helper to check for API misuse in mkOp functions. */ void checkMkTerm(Kind kind, uint32_t nchildren) const; @@ -3626,15 +3647,8 @@ class CVC4_PUBLIC Solver // new API. !!! std::vector termVectorToExprs(const std::vector& terms); std::vector termVectorToNodes(const std::vector& terms); -std::vector sortVectorToTypes(const std::vector& sorts); -std::vector sortVectorToTypeNodes(const std::vector& sorts); -std::set sortSetToTypeNodes(const std::set& sorts); std::vector exprVectorToTerms(const Solver* slv, const std::vector& terms); -std::vector typeVectorToSorts(const Solver* slv, - const std::vector& sorts); -std::vector typeNodeVectorToSorts(const Solver* slv, - const std::vector& types); } // namespace api diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 9227c3703..3b723de1f 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1213,7 +1213,7 @@ void DefineSortCommand::toStream(std::ostream& out, Printer::getPrinter(language)->toStreamCmdDefineType( out, d_symbol, - api::sortVectorToTypeNodes(d_params), + api::Sort::sortVectorToTypeNodes(d_params), d_sort.getTypeNode()); } @@ -2809,7 +2809,7 @@ void DatatypeDeclarationCommand::toStream(std::ostream& out, OutputLanguage language) const { Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration( - out, api::sortVectorToTypeNodes(d_datatypes)); + out, api::Sort::sortVectorToTypeNodes(d_datatypes)); } } // namespace CVC4