diff options
Diffstat (limited to 'test/unit/api/cpp/op_black.cpp')
-rw-r--r-- | test/unit/api/cpp/op_black.cpp | 280 |
1 files changed, 280 insertions, 0 deletions
diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp new file mode 100644 index 000000000..fd45b1c22 --- /dev/null +++ b/test/unit/api/cpp/op_black.cpp @@ -0,0 +1,280 @@ +/****************************************************************************** + * Top contributors (to current version): + * Makai Mann, Aina Niemetz + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Black box testing of the Op class. + */ + +#include "test_api.h" + +namespace cvc5 { + +using namespace api; + +namespace test { + +class TestApiBlackOp : public TestApi +{ +}; + +TEST_F(TestApiBlackOp, getKind) +{ + Op x; + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); + ASSERT_NO_THROW(x.getKind()); +} + +TEST_F(TestApiBlackOp, isNull) +{ + Op x; + ASSERT_TRUE(x.isNull()); + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); + ASSERT_FALSE(x.isNull()); +} + +TEST_F(TestApiBlackOp, opFromKind) +{ + ASSERT_NO_THROW(d_solver.mkOp(PLUS)); + ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC5ApiException); +} + +TEST_F(TestApiBlackOp, getNumIndices) +{ + Op plus = d_solver.mkOp(PLUS); + Op divisible = d_solver.mkOp(DIVISIBLE, 4); + 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); + Op bitvector_rotate_left = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8); + Op bitvector_rotate_right = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9); + Op int_to_bitvector = d_solver.mkOp(INT_TO_BITVECTOR, 10); + 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 floatingpoint_to_fp_ieee_bitvector = + d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25); + Op floatingpoint_to_fp_floatingpoint = + d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25); + Op floatingpoint_to_fp_real = d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25); + Op floatingpoint_to_fp_signed_bitvector = + d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25); + Op floatingpoint_to_fp_unsigned_bitvector = + d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25); + Op floatingpoint_to_fp_generic = + d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25); + Op regexp_loop = d_solver.mkOp(REGEXP_LOOP, 2, 3); + + ASSERT_EQ(0, plus.getNumIndices()); + ASSERT_EQ(1, divisible.getNumIndices()); + ASSERT_EQ(1, bitvector_repeat.getNumIndices()); + ASSERT_EQ(1, bitvector_zero_extend.getNumIndices()); + ASSERT_EQ(1, bitvector_sign_extend.getNumIndices()); + ASSERT_EQ(1, bitvector_rotate_left.getNumIndices()); + ASSERT_EQ(1, bitvector_rotate_right.getNumIndices()); + ASSERT_EQ(1, int_to_bitvector.getNumIndices()); + ASSERT_EQ(1, iand.getNumIndices()); + ASSERT_EQ(1, floatingpoint_to_ubv.getNumIndices()); + ASSERT_EQ(1, floatingopint_to_sbv.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()); + ASSERT_EQ(2, floatingpoint_to_fp_signed_bitvector.getNumIndices()); + ASSERT_EQ(2, floatingpoint_to_fp_unsigned_bitvector.getNumIndices()); + ASSERT_EQ(2, floatingpoint_to_fp_generic.getNumIndices()); + ASSERT_EQ(2, regexp_loop.getNumIndices()); +} + +TEST_F(TestApiBlackOp, subscriptOperator) +{ + Op plus = d_solver.mkOp(PLUS); + Op divisible = d_solver.mkOp(DIVISIBLE, 4); + Op bitvector_repeat = d_solver.mkOp(BITVECTOR_REPEAT, 4); + Op bitvector_zero_extend = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 4); + Op bitvector_sign_extend = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 4); + Op bitvector_rotate_left = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 4); + Op bitvector_rotate_right = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 4); + Op int_to_bitvector = d_solver.mkOp(INT_TO_BITVECTOR, 4); + Op iand = d_solver.mkOp(IAND, 4); + Op floatingpoint_to_ubv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 4); + Op floatingopint_to_sbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 4); + Op floatingpoint_to_fp_ieee_bitvector = + d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 5); + Op floatingpoint_to_fp_floatingpoint = + d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 5); + Op floatingpoint_to_fp_real = d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 5); + Op floatingpoint_to_fp_signed_bitvector = + d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 5); + Op floatingpoint_to_fp_unsigned_bitvector = + d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 5); + Op floatingpoint_to_fp_generic = + d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 5); + Op regexp_loop = d_solver.mkOp(REGEXP_LOOP, 4, 5); + + ASSERT_THROW(plus[0], CVC5ApiException); + ASSERT_EQ(4, divisible[0].getUInt32Value()); + ASSERT_EQ(4, bitvector_repeat[0].getUInt32Value()); + ASSERT_EQ(4, bitvector_zero_extend[0].getUInt32Value()); + ASSERT_EQ(4, bitvector_sign_extend[0].getUInt32Value()); + ASSERT_EQ(4, bitvector_rotate_left[0].getUInt32Value()); + ASSERT_EQ(4, bitvector_rotate_right[0].getUInt32Value()); + ASSERT_EQ(4, int_to_bitvector[0].getUInt32Value()); + ASSERT_EQ(4, iand[0].getUInt32Value()); + ASSERT_EQ(4, floatingpoint_to_ubv[0].getUInt32Value()); + ASSERT_EQ(4, floatingopint_to_sbv[0].getUInt32Value()); + ASSERT_EQ(4, floatingpoint_to_fp_ieee_bitvector[0].getUInt32Value()); + ASSERT_EQ(4, floatingpoint_to_fp_floatingpoint[0].getUInt32Value()); + ASSERT_EQ(4, floatingpoint_to_fp_real[0].getUInt32Value()); + ASSERT_EQ(4, floatingpoint_to_fp_signed_bitvector[0].getUInt32Value()); + ASSERT_EQ(4, floatingpoint_to_fp_unsigned_bitvector[0].getUInt32Value()); + ASSERT_EQ(4, floatingpoint_to_fp_generic[0].getUInt32Value()); + ASSERT_EQ(4, regexp_loop[0].getUInt32Value()); +} + +TEST_F(TestApiBlackOp, getIndicesString) +{ + Op x; + ASSERT_THROW(x.getIndices<std::string>(), CVC5ApiException); + + Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4); + ASSERT_TRUE(divisible_ot.isIndexed()); + std::string divisible_idx = divisible_ot.getIndices<std::string>(); + ASSERT_EQ(divisible_idx, "4"); +} + +TEST_F(TestApiBlackOp, getIndicesUint) +{ + Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); + ASSERT_TRUE(bitvector_repeat_ot.isIndexed()); + uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices<uint32_t>(); + ASSERT_EQ(bitvector_repeat_idx, 5); + ASSERT_THROW( + (bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()), + CVC5ApiException); + + 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>(); + ASSERT_EQ(bitvector_zero_extend_idx, 6); + + 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>(); + ASSERT_EQ(bitvector_sign_extend_idx, 7); + + 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>(); + ASSERT_EQ(bitvector_rotate_left_idx, 8); + + 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>(); + ASSERT_EQ(bitvector_rotate_right_idx, 9); + + 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>(); + ASSERT_EQ(int_to_bitvector_idx, 10); + + 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>(); + ASSERT_EQ(floatingpoint_to_ubv_idx, 11); + + 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>(); + ASSERT_EQ(floatingpoint_to_sbv_idx, 13); +} + +TEST_F(TestApiBlackOp, getIndicesPairUint) +{ + Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); + ASSERT_TRUE(bitvector_extract_ot.isIndexed()); + std::pair<uint32_t, uint32_t> bitvector_extract_indices = + bitvector_extract_ot.getIndices<std::pair<uint32_t, uint32_t>>(); + ASSERT_TRUE( + (bitvector_extract_indices == std::pair<uint32_t, uint32_t>{4, 0})); + + 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>>(); + ASSERT_TRUE((floatingpoint_to_fp_ieee_bitvector_indices + == std::pair<uint32_t, uint32_t>{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>>(); + ASSERT_TRUE((floatingpoint_to_fp_floatingpoint_indices + == std::pair<uint32_t, uint32_t>{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>>(); + ASSERT_TRUE((floatingpoint_to_fp_real_indices + == std::pair<uint32_t, uint32_t>{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>>(); + ASSERT_TRUE((floatingpoint_to_fp_signed_bitvector_indices + == std::pair<uint32_t, uint32_t>{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>>(); + ASSERT_TRUE((floatingpoint_to_fp_unsigned_bitvector_indices + == std::pair<uint32_t, uint32_t>{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>>(); + ASSERT_TRUE((floatingpoint_to_fp_generic_indices + == std::pair<uint32_t, uint32_t>{4, 25})); + ASSERT_THROW(floatingpoint_to_fp_generic_ot.getIndices<std::string>(), + CVC5ApiException); +} + +TEST_F(TestApiBlackOp, getIndicesVector) +{ + std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2}; + Op tuple_project_op = d_solver.mkOp(TUPLE_PROJECT, indices); + + ASSERT_TRUE(tuple_project_op.isIndexed()); + std::vector<Term> tuple_project_extract_indices = + tuple_project_op.getIndices<std::vector<Term>>(); + ASSERT_THROW(tuple_project_op.getIndices<std::string>(), CVC5ApiException); + for (size_t i = 0; i < indices.size(); i++) + { + ASSERT_EQ(indices[i], tuple_project_extract_indices[i].getUInt32Value()); + ASSERT_EQ(indices[i], tuple_project_op[i].getUInt32Value()); + } +} + +TEST_F(TestApiBlackOp, opScopingToString) +{ + Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); + std::string op_repr = bitvector_repeat_ot.toString(); + Solver solver2; + ASSERT_EQ(bitvector_repeat_ot.toString(), op_repr); +} +} // namespace test +} // namespace cvc5 |