diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-13 12:24:07 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-13 18:24:07 +0000 |
| commit | 8c9fff99a2be7369e33520a120e25e6d8c3ec07c (patch) | |
| tree | 75ea187648825cc7ae3a135cb58078c49864d0c4 /src/api/cpp/cvc5.cpp | |
| parent | b7164b45928fe5a03a6debb21e345948cb814d69 (diff) | |
Fixes and additions for API for parametric datatypes (#7760)
Diffstat (limited to 'src/api/cpp/cvc5.cpp')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index aa3e7fa3f..1e5738ed8 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -3804,7 +3804,7 @@ Term DatatypeConstructor::getConstructorTerm() const CVC5_API_TRY_CATCH_END; } -Term DatatypeConstructor::getSpecializedConstructorTerm( +Term DatatypeConstructor::getInstantiatedConstructorTerm( const Sort& retSort) const { CVC5_API_TRY_CATCH_BEGIN; @@ -4109,6 +4109,18 @@ size_t Datatype::getNumConstructors() const CVC5_API_TRY_CATCH_END; } +std::vector<Sort> Datatype::getParameters() const +{ + CVC5_API_TRY_CATCH_BEGIN; + CVC5_API_CHECK_NOT_NULL; + CVC5_API_CHECK(isParametric()) << "Expected parametric datatype"; + //////// all checks before this line + std::vector<cvc5::TypeNode> params = d_dtype->getParameters(); + return Sort::typeNodeVectorToSorts(d_solver, params); + //////// + CVC5_API_TRY_CATCH_END; +} + bool Datatype::isParametric() const { CVC5_API_TRY_CATCH_BEGIN; |