diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-06 11:00:33 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-12-06 11:00:33 -0600 |
| commit | c7c2d593674e3776ab0c720be1c0c759db8f9453 (patch) | |
| tree | fc129a2f0453eb2944009249c4a83ba3bdbaf5a0 /test/unit/api/solver_black.h | |
| parent | 499aa5641e2b830f60159c2ce1c791bf4d45aac1 (diff) | |
Add ExprManager as argument to Datatype (#3535)
Diffstat (limited to 'test/unit/api/solver_black.h')
| -rw-r--r-- | test/unit/api/solver_black.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 92313ac3c..2831b840d 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -179,7 +179,7 @@ void SolverBlack::testMkFloatingPointSort() void SolverBlack::testMkDatatypeSort() { - DatatypeDecl dtypeSpec("list"); + DatatypeDecl dtypeSpec = d_solver->mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); cons.addSelector(head); @@ -187,7 +187,7 @@ void SolverBlack::testMkDatatypeSort() DatatypeConstructorDecl nil("nil"); dtypeSpec.addConstructor(nil); TS_ASSERT_THROWS_NOTHING(d_solver->mkDatatypeSort(dtypeSpec)); - DatatypeDecl throwsDtypeSpec("list"); + DatatypeDecl throwsDtypeSpec = d_solver->mkDatatypeDecl("list"); TS_ASSERT_THROWS(d_solver->mkDatatypeSort(throwsDtypeSpec), CVC4ApiException&); } @@ -627,7 +627,7 @@ void SolverBlack::testMkTermFromOp() // list datatype Sort sort = d_solver->mkParamSort("T"); - DatatypeDecl listDecl("paramlist", sort); + DatatypeDecl listDecl = d_solver->mkDatatypeDecl("paramlist", sort); DatatypeConstructorDecl cons("cons"); DatatypeConstructorDecl nil("nil"); DatatypeSelectorDecl head("head", sort); @@ -930,7 +930,7 @@ void SolverBlack::testGetOp() TS_ASSERT_EQUALS(exta.getOp(), ext); // Test Datatypes -- more complicated - DatatypeDecl consListSpec("list"); + DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); @@ -1036,7 +1036,7 @@ 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"); + DatatypeDecl consListSpec = d_solver->mkDatatypeDecl("list"); DatatypeConstructorDecl cons("cons"); DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); |