diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-16 15:47:31 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-16 15:47:31 -0600 |
commit | f5c8fa4f2edf773d1942110b7fee6411894c6961 (patch) | |
tree | b321476b9a74f3146ac65818ab73dca7087cb00d /src | |
parent | e3231523b7bd8da0871b1efb63f23f1b3c4adbe7 (diff) |
Add temporary global API conversion utilities. (#3759)
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 111 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 21 |
2 files changed, 98 insertions, 34 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index ddc1a61a0..f2c4d3dd3 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -562,26 +562,6 @@ bool isDefinedIntKind(CVC4::Kind k) } #endif -Kind intToExtKind(CVC4::Kind k) -{ - auto it = s_kinds_internal.find(k); - if (it == s_kinds_internal.end()) - { - return INTERNAL_KIND; - } - return it->second; -} - -CVC4::Kind extToIntKind(Kind k) -{ - auto it = s_kinds.find(k); - if (it == s_kinds.end()) - { - return CVC4::Kind::UNDEFINED_KIND; - } - return it->second; -} - uint32_t minArity(Kind k) { Assert(isDefinedKind(k)); @@ -796,17 +776,6 @@ Sort::~Sort() {} bool Sort::isNullHelper() const { return d_type->isNull(); } -std::vector<Sort> Sort::typeVectorToSorts( - const std::vector<CVC4::Type>& types) const -{ - std::vector<Sort> res; - for (const CVC4::Type& t : types) - { - res.push_back(Sort(t)); - } - return res; -} - bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; } bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; } @@ -3984,5 +3953,85 @@ ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); } */ SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); } + +/* -------------------------------------------------------------------------- */ +/* Conversions */ +/* -------------------------------------------------------------------------- */ + +std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms) +{ + std::vector<Expr> exprs; + for (size_t i = 0, tsize = terms.size(); i < tsize; i++) + { + exprs.push_back(terms[i].getExpr()); + } + return exprs; +} + +std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts) +{ + std::vector<Type> types; + for (size_t i = 0, ssize = sorts.size(); i < ssize; i++) + { + types.push_back(sorts[i].getType()); + } + return types; +} + +std::set<Type> sortSetToTypes(const std::set<Sort>& sorts) +{ + std::set<Type> types; + for (const Sort& s : sorts) + { + types.insert(s.getType()); + } + return types; +} + +std::vector<Term> exprVectorToTerms(const std::vector<Expr>& exprs) +{ + std::vector<Term> terms; + for (size_t i = 0, esize = exprs.size(); i < esize; i++) + { + terms.push_back(Term(exprs[i])); + } + return terms; +} + +std::vector<Sort> typeVectorToSorts(const std::vector<Type>& types) +{ + std::vector<Sort> sorts; + for (size_t i = 0, tsize = types.size(); i < tsize; i++) + { + sorts.push_back(Sort(types[i])); + } + return sorts; +} + } // namespace api + +/* -------------------------------------------------------------------------- */ +/* Kind Conversions */ +/* -------------------------------------------------------------------------- */ + +CVC4::api::Kind intToExtKind(CVC4::Kind k) +{ + auto it = api::s_kinds_internal.find(k); + if (it == api::s_kinds_internal.end()) + { + return api::INTERNAL_KIND; + } + return it->second; +} + +CVC4::Kind extToIntKind(CVC4::api::Kind k) +{ + auto it = api::s_kinds.find(k); + if (it == api::s_kinds.end()) + { + return CVC4::Kind::UNDEFINED_KIND; + } + return it->second; +} + } // namespace CVC4 diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 396c4eedb..84615afc0 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -20,6 +20,10 @@ #define CVC4__API__CVC4CPP_H #include "api/cvc4cppkind.h" +// !!! Only temporarily public until the parser is fully migrated to the new +// API. !!! +#include "expr/kind.h" +// !!! #include <map> #include <memory> @@ -510,9 +514,6 @@ class CVC4_PUBLIC Sort */ bool isNullHelper() const; - /* Helper to convert a vector of sorts into a vector of internal types. */ - std::vector<Sort> typeVectorToSorts( - const std::vector<CVC4::Type>& vector) const; /** * The interal type wrapped by this sort. * This is a shared_ptr rather than a unique_ptr to avoid overhead due to @@ -2689,6 +2690,20 @@ class CVC4_PUBLIC Solver std::unique_ptr<Random> d_rng; }; +// !!! Only temporarily public until the parser is fully migrated to the +// new API. !!! +std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms); +std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts); +std::vector<Term> exprVectorToTerms(const std::vector<Expr>& terms); +std::vector<Sort> typeVectorToSorts(const std::vector<Type>& sorts); +std::set<Type> sortSetToTypes(const std::set<Sort>& sorts); + } // namespace api + +// !!! Only temporarily public until the parser is fully migrated to the +// new API. !!! +CVC4::api::Kind intToExtKind(CVC4::Kind k); +CVC4::Kind extToIntKind(CVC4::api::Kind k); + } // namespace CVC4 #endif |