diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-02-11 09:04:54 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-02-11 09:04:54 -0800 |
commit | c86e0178bfaa662b6586d866c953a56f81cefe51 (patch) | |
tree | ac85369968820dbe825d0f8fd8c9920ed483a1b9 /src | |
parent | 104b28b4c16b90a819c8f79d60f94a42fb0c0261 (diff) |
New C++ API: Unit tests for declare* functions. (#2831)
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 23 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 10 |
2 files changed, 31 insertions, 2 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index ddb17c3a7..ea70fc056 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1373,6 +1373,13 @@ std::ostream& operator<<(std::ostream& out, return out; } +std::ostream& operator<<(std::ostream& out, + const std::vector<DatatypeConstructorDecl>& vector) +{ + container_to_stream(out, vector); + return out; +} + /* DatatypeDecl ------------------------------------------------------------- */ DatatypeDecl::DatatypeDecl(const std::string& name, bool isCoDatatype) @@ -2980,7 +2987,17 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const */ Term Solver::declareConst(const std::string& symbol, Sort sort) const { - return d_exprMgr->mkVar(symbol, *sort.d_type); + try + { + CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort"; + Term res = d_exprMgr->mkVar(symbol, *sort.d_type); + (void)res.d_expr->getType(true); /* kick off type checking */ + return res; + } + catch (const CVC4::TypeCheckingException& e) + { + throw CVC4ApiException(e.getMessage()); + } } /** @@ -2990,12 +3007,14 @@ Sort Solver::declareDatatype( const std::string& symbol, const std::vector<DatatypeConstructorDecl>& ctors) const { + CVC4_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors) + << "a datatype declaration with at least one constructor"; DatatypeDecl dtdecl(symbol); for (const DatatypeConstructorDecl& ctor : ctors) { dtdecl.addConstructor(ctor); } - return mkDatatypeSort(dtdecl); + return d_exprMgr->mkDatatypeType(*dtdecl.d_dtype); } /** diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index b8da070fc..955aff21a 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -1456,6 +1456,16 @@ std::ostream& operator<<(std::ostream& out, const DatatypeConstructorDecl& ctordecl) CVC4_PUBLIC; /** + * Serialize a vector of datatype constructor declarations to given stream. + * @param out the output stream + * @param vector the vector of datatype constructor declarations to be + * serialized to the given stream + * @return the output stream + */ +std::ostream& operator<<(std::ostream& out, + const std::vector<DatatypeConstructorDecl>& vector); + +/** * Serialize a datatype selector declaration to given stream. * @param out the output stream * @param stordecl the datatype selector declaration to be serialized |