diff options
Diffstat (limited to 'test/unit/api')
-rw-r--r-- | test/unit/api/opterm_black.h | 106 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 234 | ||||
-rw-r--r-- | test/unit/api/term_black.h | 6 |
3 files changed, 199 insertions, 147 deletions
diff --git a/test/unit/api/opterm_black.h b/test/unit/api/opterm_black.h index 150cebcbf..0dd7587ff 100644 --- a/test/unit/api/opterm_black.h +++ b/test/unit/api/opterm_black.h @@ -18,7 +18,7 @@ using namespace CVC4::api; -class OpTermBlack : public CxxTest::TestSuite +class OpBlack : public CxxTest::TestSuite { public: void setUp() override {} @@ -27,6 +27,7 @@ class OpTermBlack : public CxxTest::TestSuite void testGetKind(); void testGetSort(); void testIsNull(); + void testOpTermFromKind(); void testGetIndicesString(); void testGetIndicesKind(); void testGetIndicesUint(); @@ -36,168 +37,173 @@ class OpTermBlack : public CxxTest::TestSuite Solver d_solver; }; -void OpTermBlack::testGetKind() +void OpBlack::testGetKind() { - OpTerm x; + Op x; TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&); - x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); TS_ASSERT_THROWS_NOTHING(x.getKind()); } -void OpTermBlack::testGetSort() +void OpBlack::testGetSort() { - OpTerm x; + Op x; TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&); - x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); TS_ASSERT_THROWS_NOTHING(x.getSort()); } -void OpTermBlack::testIsNull() +void OpBlack::testIsNull() { - OpTerm x; + Op x; TS_ASSERT(x.isNull()); - x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); TS_ASSERT(!x.isNull()); } -void OpTermBlack::testGetIndicesString() +void OpBlack::testOpTermFromKind() { - OpTerm x; + Op plus(PLUS); + TS_ASSERT(!plus.isIndexed()); + TS_ASSERT_THROWS(plus.getIndices<uint32_t>(), CVC4ApiException&); +} + +void OpBlack::testGetIndicesString() +{ + Op x; TS_ASSERT_THROWS(x.getIndices<std::string>(), CVC4ApiException&); - OpTerm divisible_ot = d_solver.mkOpTerm(DIVISIBLE_OP, 4); + Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4); + TS_ASSERT(divisible_ot.isIndexed()); std::string divisible_idx = divisible_ot.getIndices<std::string>(); TS_ASSERT(divisible_idx == "4"); - OpTerm record_update_ot = d_solver.mkOpTerm(RECORD_UPDATE_OP, "test"); + Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test"); std::string record_update_idx = record_update_ot.getIndices<std::string>(); TS_ASSERT(record_update_idx == "test"); TS_ASSERT_THROWS(record_update_ot.getIndices<uint32_t>(), CVC4ApiException&); } -void OpTermBlack::testGetIndicesKind() +void OpBlack::testGetIndicesKind() { - OpTerm chain_ot = d_solver.mkOpTerm(CHAIN_OP, AND); + Op chain_ot = d_solver.mkOp(CHAIN, AND); + TS_ASSERT(chain_ot.isIndexed()); Kind chain_idx = chain_ot.getIndices<Kind>(); TS_ASSERT(chain_idx == AND); } -void OpTermBlack::testGetIndicesUint() +void OpBlack::testGetIndicesUint() { - OpTerm bitvector_repeat_ot = d_solver.mkOpTerm(BITVECTOR_REPEAT_OP, 5); + Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); + TS_ASSERT(bitvector_repeat_ot.isIndexed()); uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices<uint32_t>(); TS_ASSERT(bitvector_repeat_idx == 5); TS_ASSERT_THROWS( (bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()), CVC4ApiException&); - OpTerm bitvector_zero_extend_ot = - d_solver.mkOpTerm(BITVECTOR_ZERO_EXTEND_OP, 6); + Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); uint32_t bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIndices<uint32_t>(); TS_ASSERT(bitvector_zero_extend_idx == 6); - OpTerm bitvector_sign_extend_ot = - d_solver.mkOpTerm(BITVECTOR_SIGN_EXTEND_OP, 7); + Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7); uint32_t bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIndices<uint32_t>(); TS_ASSERT(bitvector_sign_extend_idx == 7); - OpTerm bitvector_rotate_left_ot = - d_solver.mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 8); + Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8); uint32_t bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIndices<uint32_t>(); TS_ASSERT(bitvector_rotate_left_idx == 8); - OpTerm bitvector_rotate_right_ot = - d_solver.mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 9); + Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9); uint32_t bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIndices<uint32_t>(); TS_ASSERT(bitvector_rotate_right_idx == 9); - OpTerm int_to_bitvector_ot = d_solver.mkOpTerm(INT_TO_BITVECTOR_OP, 10); + Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10); uint32_t int_to_bitvector_idx = int_to_bitvector_ot.getIndices<uint32_t>(); TS_ASSERT(int_to_bitvector_idx == 10); - OpTerm floatingpoint_to_ubv_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_OP, 11); + Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11); uint32_t floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIndices<uint32_t>(); TS_ASSERT(floatingpoint_to_ubv_idx == 11); - OpTerm floatingpoint_to_ubv_total_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_TOTAL_OP, 12); + Op floatingpoint_to_ubv_total_ot = + d_solver.mkOp(FLOATINGPOINT_TO_UBV_TOTAL, 12); uint32_t floatingpoint_to_ubv_total_idx = floatingpoint_to_ubv_total_ot.getIndices<uint32_t>(); TS_ASSERT(floatingpoint_to_ubv_total_idx == 12); - OpTerm floatingpoint_to_sbv_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_OP, 13); + Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13); uint32_t floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIndices<uint32_t>(); TS_ASSERT(floatingpoint_to_sbv_idx == 13); - OpTerm floatingpoint_to_sbv_total_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_TOTAL_OP, 14); + Op floatingpoint_to_sbv_total_ot = + d_solver.mkOp(FLOATINGPOINT_TO_SBV_TOTAL, 14); uint32_t floatingpoint_to_sbv_total_idx = floatingpoint_to_sbv_total_ot.getIndices<uint32_t>(); TS_ASSERT(floatingpoint_to_sbv_total_idx == 14); - OpTerm tuple_update_ot = d_solver.mkOpTerm(TUPLE_UPDATE_OP, 5); + Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5); uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>(); TS_ASSERT(tuple_update_idx == 5); TS_ASSERT_THROWS(tuple_update_ot.getIndices<std::string>(), CVC4ApiException&); } -void OpTermBlack::testGetIndicesPairUint() +void OpBlack::testGetIndicesPairUint() { - OpTerm bitvector_extract_ot = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 4, 0); + Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); + TS_ASSERT(bitvector_extract_ot.isIndexed()); std::pair<uint32_t, uint32_t> bitvector_extract_indices = bitvector_extract_ot.getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((bitvector_extract_indices == std::pair<uint32_t, uint32_t>{4, 0})); - OpTerm floatingpoint_to_fp_ieee_bitvector_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, 4, 25); + Op floatingpoint_to_fp_ieee_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot .getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((floatingpoint_to_fp_ieee_bitvector_indices == std::pair<uint32_t, uint32_t>{4, 25})); - OpTerm floatingpoint_to_fp_floatingpoint_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, 4, 25); + Op floatingpoint_to_fp_floatingpoint_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot .getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((floatingpoint_to_fp_floatingpoint_indices == std::pair<uint32_t, uint32_t>{4, 25})); - OpTerm floatingpoint_to_fp_real_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_REAL_OP, 4, 25); + Op floatingpoint_to_fp_real_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((floatingpoint_to_fp_real_indices == std::pair<uint32_t, uint32_t>{4, 25})); - OpTerm floatingpoint_to_fp_signed_bitvector_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, 4, 25); + Op floatingpoint_to_fp_signed_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot .getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((floatingpoint_to_fp_signed_bitvector_indices == std::pair<uint32_t, uint32_t>{4, 25})); - OpTerm floatingpoint_to_fp_unsigned_bitvector_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, 4, 25); + Op floatingpoint_to_fp_unsigned_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot .getIndices<std::pair<uint32_t, uint32_t>>(); TS_ASSERT((floatingpoint_to_fp_unsigned_bitvector_indices == std::pair<uint32_t, uint32_t>{4, 25})); - OpTerm floatingpoint_to_fp_generic_ot = - d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_GENERIC_OP, 4, 25); + Op floatingpoint_to_fp_generic_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25); std::pair<uint32_t, uint32_t> floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot .getIndices<std::pair<uint32_t, uint32_t>>(); diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index 374a3ff2a..92313ac3c 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -40,7 +40,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkFloatingPointSort(); void testMkDatatypeSort(); void testMkFunctionSort(); - void testMkOpTerm(); + void testMkOp(); void testMkParamSort(); void testMkPredicateSort(); void testMkRecordSort(); @@ -70,7 +70,7 @@ class SolverBlack : public CxxTest::TestSuite void testMkSepNil(); void testMkString(); void testMkTerm(); - void testMkTermFromOpTerm(); + void testMkTermFromOp(); void testMkTrue(); void testMkTuple(); void testMkUninterpretedConst(); @@ -85,6 +85,9 @@ class SolverBlack : public CxxTest::TestSuite void testDefineFunRec(); void testDefineFunsRec(); + void testUFIteration(); + void testGetOp(); + void testPush1(); void testPush2(); void testPop1(); @@ -453,29 +456,27 @@ void SolverBlack::testMkPosZero() } } -void SolverBlack::testMkOpTerm() +void SolverBlack::testMkOp() { - // mkOpTerm(Kind kind, Kind k) - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(CHAIN_OP, EQUAL)); - TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, EQUAL), - CVC4ApiException&); + // mkOp(Kind kind, Kind k) + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(CHAIN, EQUAL)); + TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, EQUAL), CVC4ApiException&); - // mkOpTerm(Kind kind, const std::string& arg) - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(RECORD_UPDATE_OP, "asdf")); - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, "2147483648")); - TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, "asdf"), + // mkOp(Kind kind, const std::string& arg) + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(RECORD_UPDATE, "asdf")); + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(DIVISIBLE, "2147483648")); + TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, "asdf"), CVC4ApiException&); - // mkOpTerm(Kind kind, uint32_t arg) - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, 1)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 1)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 1)); - TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1), - CVC4ApiException&); + // mkOp(Kind kind, uint32_t arg) + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(DIVISIBLE, 1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_ROTATE_LEFT, 1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_ROTATE_RIGHT, 1)); + TS_ASSERT_THROWS(d_solver->mkOp(BITVECTOR_EXTRACT, 1), CVC4ApiException&); - // mkOpTerm(Kind kind, uint32_t arg1, uint32_t arg2) - TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 1, 1)); - TS_ASSERT_THROWS(d_solver->mkOpTerm(DIVISIBLE_OP, 1, 2), CVC4ApiException&); + // mkOp(Kind kind, uint32_t arg1, uint32_t arg2) + TS_ASSERT_THROWS_NOTHING(d_solver->mkOp(BITVECTOR_EXTRACT, 1, 1)); + TS_ASSERT_THROWS(d_solver->mkOp(DIVISIBLE, 1, 2), CVC4ApiException&); } void SolverBlack::testMkPi() { TS_ASSERT_THROWS_NOTHING(d_solver->mkPi()); } @@ -611,7 +612,7 @@ void SolverBlack::testMkTerm() TS_ASSERT_THROWS(d_solver->mkTerm(DISTINCT, v6), CVC4ApiException&); } -void SolverBlack::testMkTermFromOpTerm() +void SolverBlack::testMkTermFromOp() { Sort bv32 = d_solver->mkBitVectorSort(32); Term a = d_solver->mkConst(bv32, "a"); @@ -620,9 +621,9 @@ void SolverBlack::testMkTermFromOpTerm() std::vector<Term> v2 = {d_solver->mkReal(1), Term()}; std::vector<Term> v3 = {}; // simple operator terms - OpTerm opterm1 = d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, 2, 1); - OpTerm opterm2 = d_solver->mkOpTerm(DIVISIBLE_OP, 1); - OpTerm opterm3 = d_solver->mkOpTerm(CHAIN_OP, EQUAL); + Op opterm1 = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1); + Op opterm2 = d_solver->mkOp(DIVISIBLE, 1); + Op opterm3 = d_solver->mkOp(CHAIN, EQUAL); // list datatype Sort sort = d_solver->mkParamSort("T"); @@ -641,80 +642,60 @@ void SolverBlack::testMkTermFromOpTerm() Term c = d_solver->mkConst(intListSort, "c"); Datatype list = listSort.getDatatype(); // list datatype constructor and selector operator terms - OpTerm consTerm1 = list.getConstructorTerm("cons"); - OpTerm consTerm2 = list.getConstructor("cons").getConstructorTerm(); - OpTerm nilTerm1 = list.getConstructorTerm("nil"); - OpTerm nilTerm2 = list.getConstructor("nil").getConstructorTerm(); - OpTerm headTerm1 = list["cons"].getSelectorTerm("head"); - OpTerm headTerm2 = list["cons"].getSelector("head").getSelectorTerm(); - OpTerm tailTerm1 = list["cons"].getSelectorTerm("tail"); - OpTerm tailTerm2 = list["cons"]["tail"].getSelectorTerm(); - - // mkTerm(Kind kind, OpTerm opTerm) const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm2)); - TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm2), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_CONSTRUCTOR, opterm1), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, headTerm1), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2), - CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1), + Op consTerm1 = list.getConstructorTerm("cons"); + Op consTerm2 = list.getConstructor("cons").getConstructorTerm(); + Op nilTerm1 = list.getConstructorTerm("nil"); + Op nilTerm2 = list.getConstructor("nil").getConstructorTerm(); + Op headTerm1 = list["cons"].getSelectorTerm("head"); + Op headTerm2 = list["cons"].getSelector("head").getSelectorTerm(); + Op tailTerm1 = list["cons"].getSelectorTerm("tail"); + Op tailTerm2 = list["cons"]["tail"].getSelectorTerm(); + + // mkTerm(Kind kind, Op op) const + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm1)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(nilTerm2)); + TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(consTerm2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(headTerm1), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(tailTerm2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1), CVC4ApiException&); + + // mkTerm(Kind kind, Op op, Term child) const + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm1, a)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm2, d_solver->mkReal(1))); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(headTerm1, c)); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(tailTerm2, c)); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm2, a), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, Term()), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(consTerm1, d_solver->mkReal(0)), CVC4ApiException&); - // mkTerm(Kind kind, OpTerm opTerm, Term child) const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a)); + // mkTerm(Kind kind, Op op, Term child1, Term child2) const TS_ASSERT_THROWS_NOTHING( - d_solver->mkTerm(DIVISIBLE, opterm2, d_solver->mkReal(1))); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, headTerm1, c)); - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(APPLY_SELECTOR, tailTerm2, c)); - TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm1, a), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(DIVISIBLE, opterm2, a), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, Term()), - CVC4ApiException&); - TS_ASSERT_THROWS( - d_solver->mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver->mkReal(0)), - CVC4ApiException&); - - // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2) const + d_solver->mkTerm(opterm3, d_solver->mkReal(1), d_solver->mkReal(2))); TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( - CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(2))); - TS_ASSERT_THROWS_NOTHING( - d_solver->mkTerm(APPLY_CONSTRUCTOR, - consTerm1, - d_solver->mkReal(0), - d_solver->mkTerm(APPLY_CONSTRUCTOR, nilTerm1))); - TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b), + consTerm1, d_solver->mkReal(0), d_solver->mkTerm(nilTerm1))); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, d_solver->mkReal(1), Term()), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, Term(), d_solver->mkReal(1)), CVC4ApiException&); - TS_ASSERT_THROWS( - d_solver->mkTerm(CHAIN, opterm3, d_solver->mkReal(1), Term()), - CVC4ApiException&); - TS_ASSERT_THROWS( - d_solver->mkTerm(CHAIN, opterm3, Term(), d_solver->mkReal(1)), - CVC4ApiException&); - // mkTerm(Kind kind, OpTerm opTerm, Term child1, Term child2, Term child3) + // mkTerm(Kind kind, Op op, Term child1, Term child2, Term child3) // const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN, - opterm3, - d_solver->mkReal(1), - d_solver->mkReal(1), - d_solver->mkReal(2))); - TS_ASSERT_THROWS(d_solver->mkTerm(BITVECTOR_EXTRACT, opterm1, a, b, a), - CVC4ApiException&); + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm( + opterm3, d_solver->mkReal(1), d_solver->mkReal(1), d_solver->mkReal(2))); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm1, a, b, a), CVC4ApiException&); TS_ASSERT_THROWS( d_solver->mkTerm( - CHAIN, opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()), + opterm3, d_solver->mkReal(1), d_solver->mkReal(1), Term()), CVC4ApiException&); - // mkTerm(OpTerm opTerm, const std::vector<Term>& children) const - TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(CHAIN, opterm3, v1)); - TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v2), CVC4ApiException&); - TS_ASSERT_THROWS(d_solver->mkTerm(CHAIN, opterm3, v3), CVC4ApiException&); + // mkTerm(Op op, const std::vector<Term>& children) const + TS_ASSERT_THROWS_NOTHING(d_solver->mkTerm(opterm3, v1)); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v2), CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->mkTerm(opterm3, v3), CVC4ApiException&); } void SolverBlack::testMkTrue() @@ -916,6 +897,73 @@ void SolverBlack::testDefineFunsRec() CVC4ApiException&); } +void SolverBlack::testUFIteration() +{ + Sort intSort = d_solver->getIntegerSort(); + Sort funSort = d_solver->mkFunctionSort({intSort, intSort}, intSort); + Term x = d_solver->mkConst(intSort, "x"); + Term y = d_solver->mkConst(intSort, "y"); + Term f = d_solver->mkConst(funSort, "f"); + Term fxy = d_solver->mkTerm(APPLY_UF, f, x, y); + + // Expecting the uninterpreted function to be one of the children + Term expected_children[3] = {f, x, y}; + uint32_t idx = 0; + for (auto c : fxy) + { + TS_ASSERT(idx < 3); + TS_ASSERT(c == expected_children[idx]); + idx++; + } +} + +void SolverBlack::testGetOp() +{ + Sort bv32 = d_solver->mkBitVectorSort(32); + Term a = d_solver->mkConst(bv32, "a"); + Op ext = d_solver->mkOp(BITVECTOR_EXTRACT, 2, 1); + Term exta = d_solver->mkTerm(ext, a); + + TS_ASSERT(!a.hasOp()); + TS_ASSERT_THROWS(a.getOp(), CVC4ApiException&); + TS_ASSERT(exta.hasOp()); + TS_ASSERT_EQUALS(exta.getOp(), ext); + + // Test Datatypes -- more complicated + DatatypeDecl consListSpec("list"); + DatatypeConstructorDecl cons("cons"); + DatatypeSelectorDecl head("head", d_solver->getIntegerSort()); + DatatypeSelectorDecl tail("tail", DatatypeDeclSelfSort()); + cons.addSelector(head); + cons.addSelector(tail); + consListSpec.addConstructor(cons); + DatatypeConstructorDecl nil("nil"); + consListSpec.addConstructor(nil); + Sort consListSort = d_solver->mkDatatypeSort(consListSpec); + Datatype consList = consListSort.getDatatype(); + + Op consTerm = consList.getConstructorTerm("cons"); + Op nilTerm = consList.getConstructorTerm("nil"); + Op headTerm = consList["cons"].getSelectorTerm("head"); + + TS_ASSERT(consTerm.getKind() == APPLY_CONSTRUCTOR); + TS_ASSERT(nilTerm.getKind() == APPLY_CONSTRUCTOR); + TS_ASSERT(headTerm.getKind() == APPLY_SELECTOR); + + Term listnil = d_solver->mkTerm(nilTerm); + Term listcons1 = d_solver->mkTerm(consTerm, d_solver->mkReal(1), listnil); + Term listhead = d_solver->mkTerm(headTerm, listcons1); + + TS_ASSERT(listnil.hasOp()); + TS_ASSERT_EQUALS(listnil.getOp(), nilTerm); + + TS_ASSERT(listcons1.hasOp()); + TS_ASSERT_EQUALS(listcons1.getOp(), consTerm); + + TS_ASSERT(listhead.hasOp()); + TS_ASSERT_EQUALS(listhead.getOp(), headTerm); +} + void SolverBlack::testPush1() { d_solver->setOption("incremental", "true"); @@ -1026,14 +1074,12 @@ void SolverBlack::testSimplify() TS_ASSERT(i1 == d_solver->simplify(i3)); Datatype consList = consListSort.getDatatype(); - Term dt1 = d_solver->mkTerm( - APPLY_CONSTRUCTOR, - consList.getConstructorTerm("cons"), - d_solver->mkReal(0), - d_solver->mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil"))); + Term dt1 = + d_solver->mkTerm(consList.getConstructorTerm("cons"), + d_solver->mkReal(0), + d_solver->mkTerm(consList.getConstructorTerm("nil"))); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt1)); - Term dt2 = d_solver->mkTerm( - APPLY_SELECTOR, consList["cons"].getSelectorTerm("head"), dt1); + Term dt2 = d_solver->mkTerm(consList["cons"].getSelectorTerm("head"), dt1); TS_ASSERT_THROWS_NOTHING(d_solver->simplify(dt2)); Term b1 = d_solver->mkVar(bvSort, "b1"); diff --git a/test/unit/api/term_black.h b/test/unit/api/term_black.h index c5300dbfe..0d5400f5f 100644 --- a/test/unit/api/term_black.h +++ b/test/unit/api/term_black.h @@ -207,7 +207,7 @@ void TermBlack::testAndTerm() Term b = d_solver.mkTrue(); TS_ASSERT_THROWS(Term().andTerm(b), CVC4ApiException&); - TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&); + TS_ASSERT_THROWS(b.andTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.andTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.andTerm(b), CVC4ApiException&); @@ -471,7 +471,7 @@ void TermBlack::testImpTerm() Term b = d_solver.mkTrue(); TS_ASSERT_THROWS(Term().impTerm(b), CVC4ApiException&); - TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&); + TS_ASSERT_THROWS(b.impTerm(Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.impTerm(b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS(x.impTerm(b), CVC4ApiException&); @@ -538,7 +538,7 @@ void TermBlack::testIteTerm() Term b = d_solver.mkTrue(); TS_ASSERT_THROWS(Term().iteTerm(b, b), CVC4ApiException&); TS_ASSERT_THROWS(b.iteTerm(Term(), b), CVC4ApiException&); - TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&); + TS_ASSERT_THROWS(b.iteTerm(b, Term()), CVC4ApiException&); TS_ASSERT_THROWS_NOTHING(b.iteTerm(b, b)); Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x"); TS_ASSERT_THROWS_NOTHING(b.iteTerm(x, x)); |