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.h | |
| parent | 416f6d2d55fb24fea63bd13537b24a6a88509344 (diff) | |
New C++ API: declare-datatype. (#2166)
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 11 |
1 files changed, 11 insertions, 0 deletions
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 |