diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-17 20:19:24 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-11-17 20:19:24 -0600 |
| commit | 11bc0e4c3147b0fce3033b6a4290d8730aa401ad (patch) | |
| tree | ce273375634b5e9ea3981855f57f693125b6f8cd /test/unit/api/solver_black.h | |
| parent | 990ff24487fd0b6998231894825eb9cd4610494e (diff) | |
Updates to the unit tests, api, and examples for datatypes (#3459)
* Updates to the unit tests, api, and examples for datatypes
* Format
Diffstat (limited to 'test/unit/api/solver_black.h')
| -rw-r--r-- | test/unit/api/solver_black.h | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 41c4a86dd..374a3ff2a 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -624,6 +624,7 @@ void SolverBlack::testMkTermFromOpTerm() OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1); OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL); // list datatype + Sort sort = d_solver->mkParamSort("T"); DatatypeDecl listDecl("paramlist", sort); DatatypeConstructorDecl cons("cons"); @@ -776,17 +777,21 @@ void SolverBlack::testMkConstArray() void SolverBlack::testDeclareDatatype() { - DatatypeConstructorDecl cons("cons"); DatatypeConstructorDecl nil("nil"); std::vector<DatatypeConstructorDecl> ctors1 = {nil}; - std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil}; - std::vector<DatatypeConstructorDecl> ctors3; TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("a"), ctors1)); + DatatypeConstructorDecl cons("cons"); + DatatypeConstructorDecl nil2("nil"); + std::vector<DatatypeConstructorDecl> ctors2 = {cons, nil2}; TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string("b"), ctors2)); - TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors2)); - TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors3), + DatatypeConstructorDecl cons2("cons"); + DatatypeConstructorDecl nil3("nil"); + std::vector<DatatypeConstructorDecl> ctors3 = {cons2, nil3}; + TS_ASSERT_THROWS_NOTHING(d_solver->declareDatatype(std::string(""), ctors3)); + std::vector<DatatypeConstructorDecl> ctors4; + TS_ASSERT_THROWS(d_solver->declareDatatype(std::string("c"), ctors4), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors3), + TS_ASSERT_THROWS(d_solver->declareDatatype(std::string(""), ctors4), CVC4ApiException&); } @@ -983,7 +988,6 @@ void SolverBlack::testSimplify() Sort uSort = d_solver->mkUninterpretedSort("u"); Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort()); - DatatypeDecl consListSpec("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); |