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 | |
parent | 416f6d2d55fb24fea63bd13537b24a6a88509344 (diff) |
New C++ API: declare-datatype. (#2166)
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 15 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 11 |
2 files changed, 26 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 diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 6007aadcc..b76fbb08f 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2118,6 +2118,17 @@ class CVC4_PUBLIC Solver Term declareConst(const std::string& symbol, Sort sort) const; /** + * Create datatype sort. + * SMT-LIB: ( declare-datatype <symbol> <datatype_decl> ) + * @param symbol the name of the datatype sort + * @param ctors the constructor declarations of the datatype sort + * @return the datatype sort + */ + Sort declareDatatype( + const std::string& symbol, + const std::vector<DatatypeConstructorDecl>& ctors) const; + + /** * Declare 0-arity function symbol. * SMT-LIB: ( declare-fun <symbol> ( ) <sort> ) * @param symbol the name of the function |