diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-07 19:25:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-07 19:25:27 -0500 |
commit | 8e5aba973b06fb581221a82aacdf7d3ca7938a22 (patch) | |
tree | ea5db058d5991ec44ca1f0c47054c3f0d733f367 /test/unit | |
parent | 080f0de4379c4e1fe5a016e40c7852a3abb52760 (diff) |
Add support for datatype update (#6449)
This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.
Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/api/datatype_api_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/api/op_black.cpp | 14 | ||||
-rw-r--r-- | test/unit/api/solver_black.cpp | 1 | ||||
-rw-r--r-- | test/unit/api/sort_black.cpp | 13 | ||||
-rw-r--r-- | test/unit/util/datatype_black.cpp | 4 |
5 files changed, 17 insertions, 19 deletions
diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp index 3fbdcc0b5..f82e722d3 100644 --- a/test/unit/api/datatype_api_black.cpp +++ b/test/unit/api/datatype_api_black.cpp @@ -214,6 +214,10 @@ TEST_F(TestApiBlackDatatype, datatypeNames) ASSERT_EQ(dselTail.getName(), std::string("tail")); ASSERT_EQ(dselTail.getRangeSort(), dtypeSort); + // get selector from datatype + ASSERT_NO_THROW(dt.getSelector("head")); + ASSERT_THROW(dt.getSelector("cons"), CVC5ApiException); + // possible to construct null datatype declarations if not using solver ASSERT_THROW(DatatypeDecl().getName(), CVC5ApiException); } diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp index 7183fa7a7..8c4e31c22 100644 --- a/test/unit/api/op_black.cpp +++ b/test/unit/api/op_black.cpp @@ -50,7 +50,6 @@ TEST_F(TestApiBlackOp, getNumIndices) { Op plus = d_solver.mkOp(PLUS); Op divisible = d_solver.mkOp(DIVISIBLE, 4); - Op record_update = d_solver.mkOp(RECORD_UPDATE, "test"); Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 5); Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); Op bitvector_sign_extend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7); @@ -60,7 +59,6 @@ TEST_F(TestApiBlackOp, getNumIndices) Op iand = d_solver.mkOp(IAND, 3); Op floatingpoint_to_ubv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11); Op floatingopint_to_sbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13); - Op tuple_update = d_solver.mkOp(TUPLE_UPDATE, 5); Op floatingpoint_to_fp_ieee_bitvector = d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25); Op floatingpoint_to_fp_floatingpoint = @@ -76,7 +74,6 @@ TEST_F(TestApiBlackOp, getNumIndices) ASSERT_EQ(0, plus.getNumIndices()); ASSERT_EQ(1, divisible.getNumIndices()); - ASSERT_EQ(1, record_update.getNumIndices()); ASSERT_EQ(1, bitvector_repeat.getNumIndices()); ASSERT_EQ(1, bitvector_zero_extend.getNumIndices()); ASSERT_EQ(1, bitvector_sign_extend.getNumIndices()); @@ -86,7 +83,6 @@ TEST_F(TestApiBlackOp, getNumIndices) ASSERT_EQ(1, iand.getNumIndices()); ASSERT_EQ(1, floatingpoint_to_ubv.getNumIndices()); ASSERT_EQ(1, floatingopint_to_sbv.getNumIndices()); - ASSERT_EQ(1, tuple_update.getNumIndices()); ASSERT_EQ(2, floatingpoint_to_fp_ieee_bitvector.getNumIndices()); ASSERT_EQ(2, floatingpoint_to_fp_floatingpoint.getNumIndices()); ASSERT_EQ(2, floatingpoint_to_fp_real.getNumIndices()); @@ -105,11 +101,6 @@ TEST_F(TestApiBlackOp, getIndicesString) ASSERT_TRUE(divisible_ot.isIndexed()); std::string divisible_idx = divisible_ot.getIndices<std::string>(); ASSERT_EQ(divisible_idx, "4"); - - Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test"); - std::string record_update_idx = record_update_ot.getIndices<std::string>(); - ASSERT_EQ(record_update_idx, "test"); - ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC5ApiException); } TEST_F(TestApiBlackOp, getIndicesUint) @@ -155,11 +146,6 @@ TEST_F(TestApiBlackOp, getIndicesUint) uint32_t floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIndices<uint32_t>(); ASSERT_EQ(floatingpoint_to_sbv_idx, 13); - - Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5); - uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>(); - ASSERT_EQ(tuple_update_idx, 5); - ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC5ApiException); } TEST_F(TestApiBlackOp, getIndicesPairUint) diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index c0258be9a..f7e6a3783 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -544,7 +544,6 @@ TEST_F(TestApiBlackSolver, mkOp) ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL), CVC5ApiException); // mkOp(Kind kind, const std::string& arg) - ASSERT_NO_THROW(d_solver.mkOp(RECORD_UPDATE, "asdf")); ASSERT_NO_THROW(d_solver.mkOp(DIVISIBLE, "2147483648")); ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"), CVC5ApiException); diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp index c2b924bfa..d1b096bda 100644 --- a/test/unit/api/sort_black.cpp +++ b/test/unit/api/sort_black.cpp @@ -153,11 +153,20 @@ TEST_F(TestApiBlackSort, isTester) { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); - Sort cons_sort = dt[0].getTesterTerm().getSort(); - ASSERT_TRUE(cons_sort.isTester()); + Sort testerSort = dt[0].getTesterTerm().getSort(); + ASSERT_TRUE(testerSort.isTester()); ASSERT_NO_THROW(Sort().isTester()); } +TEST_F(TestApiBlackSort, isUpdater) +{ + Sort dt_sort = create_datatype_sort(); + Datatype dt = dt_sort.getDatatype(); + Sort updaterSort = dt[0][0].getUpdaterTerm().getSort(); + ASSERT_TRUE(updaterSort.isUpdater()); + ASSERT_NO_THROW(Sort().isUpdater()); +} + TEST_F(TestApiBlackSort, isFunction) { Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index 5844868f1..a19ab31a1 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -249,9 +249,9 @@ TEST_F(TestUtilBlackDatatype, listIntUpdate) Node zero = d_nodeManager->mkConst(Rational(0)); Node truen = d_nodeManager->mkConst(true); // construct an update term - Node uterm = d_nodeManager->mkNode(kind::APPLY_DT_UPDATE, updater, gt, zero); + Node uterm = d_nodeManager->mkNode(kind::APPLY_UPDATER, updater, gt, zero); // construct a non well-formed update term - ASSERT_THROW(d_nodeManager->mkNode(kind::APPLY_DT_UPDATE, updater, gt, truen) + ASSERT_THROW(d_nodeManager->mkNode(kind::APPLY_UPDATER, updater, gt, truen) .getType(true), TypeCheckingExceptionPrivate); } |