diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-07-23 12:29:03 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-23 12:29:03 -0700 |
commit | 35c39b2cdc3905af8ad4739c20971d8b35889582 (patch) | |
tree | d2e6a6c647b3f3404aac7006eaf9497d1161d353 /src/api/cvc4cpp.cpp | |
parent | 416f6d2d55fb24fea63bd13537b24a6a88509344 (diff) |
New C++ API: declare-datatype. (#2166)
Diffstat (limited to 'src/api/cvc4cpp.cpp')
-rw-r--r-- | src/api/cvc4cpp.cpp | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 488590deb..938dc127d 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -2213,5 +2213,20 @@ std::vector<Expr> Solver::termVectorToExprs( return res; } +/** + * ( declare-datatype <symbol> <datatype_decl> ) + */ +Sort Solver::declareDatatype( + const std::string& symbol, + const std::vector<DatatypeConstructorDecl>& ctors) const +{ + DatatypeDecl dtdecl(symbol); + for (const DatatypeConstructorDecl& ctor : ctors) + { + dtdecl.addConstructor(ctor); + } + return mkDatatypeSort(dtdecl); +} + } // namespace api } // namespace CVC4 |