From: makaimann Date: Tue, 3 Dec 2019 00:53:27 +0000 (-0800) Subject: Minor refactor: rename opterm_black to op_black (#3521) X-Git-Tag: cvc5-1.0.0~3808 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=274aa297537a7cbf268c8f8b73f671498e372fe0;p=cvc5.git Minor refactor: rename opterm_black to op_black (#3521) --- diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index ca3c59750..7566c432d 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -2,7 +2,7 @@ # Add unit tests cvc4_add_unit_test_black(datatype_api_black api) -cvc4_add_unit_test_black(opterm_black api) +cvc4_add_unit_test_black(op_black api) cvc4_add_unit_test_black(solver_black api) cvc4_add_unit_test_black(sort_black api) cvc4_add_unit_test_black(term_black api) diff --git a/test/unit/api/op_black.h b/test/unit/api/op_black.h new file mode 100644 index 000000000..3bf9b93c3 --- /dev/null +++ b/test/unit/api/op_black.h @@ -0,0 +1,214 @@ +/********************* */ +/*! \file op_black.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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.\endverbatim + ** + ** \brief Black box testing of the Term class + **/ + +#include + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +class OpBlack : public CxxTest::TestSuite +{ + public: + void setUp() override {} + void tearDown() override {} + + void testGetKind(); + void testGetSort(); + void testIsNull(); + void testOpFromKind(); + void testGetIndicesString(); + void testGetIndicesKind(); + void testGetIndicesUint(); + void testGetIndicesPairUint(); + + private: + Solver d_solver; +}; + +void OpBlack::testGetKind() +{ + Op x; + TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&); + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); + TS_ASSERT_THROWS_NOTHING(x.getKind()); +} + +void OpBlack::testGetSort() +{ + Op x; + TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&); + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); + TS_ASSERT_THROWS_NOTHING(x.getSort()); +} + +void OpBlack::testIsNull() +{ + Op x; + TS_ASSERT(x.isNull()); + x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); + TS_ASSERT(!x.isNull()); +} + +void OpBlack::testOpFromKind() +{ + Op plus(PLUS); + TS_ASSERT(!plus.isIndexed()); + TS_ASSERT_THROWS(plus.getIndices(), CVC4ApiException&); +} + +void OpBlack::testGetIndicesString() +{ + Op x; + TS_ASSERT_THROWS(x.getIndices(), CVC4ApiException&); + + Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4); + TS_ASSERT(divisible_ot.isIndexed()); + std::string divisible_idx = divisible_ot.getIndices(); + TS_ASSERT(divisible_idx == "4"); + + Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test"); + std::string record_update_idx = record_update_ot.getIndices(); + TS_ASSERT(record_update_idx == "test"); + TS_ASSERT_THROWS(record_update_ot.getIndices(), CVC4ApiException&); +} + +void OpBlack::testGetIndicesKind() +{ + Op chain_ot = d_solver.mkOp(CHAIN, AND); + TS_ASSERT(chain_ot.isIndexed()); + Kind chain_idx = chain_ot.getIndices(); + TS_ASSERT(chain_idx == AND); +} + +void OpBlack::testGetIndicesUint() +{ + 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(); + TS_ASSERT(bitvector_repeat_idx == 5); + TS_ASSERT_THROWS( + (bitvector_repeat_ot.getIndices>()), + CVC4ApiException&); + + Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); + uint32_t bitvector_zero_extend_idx = + bitvector_zero_extend_ot.getIndices(); + TS_ASSERT(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(); + TS_ASSERT(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(); + TS_ASSERT(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(); + TS_ASSERT(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(); + TS_ASSERT(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(); + TS_ASSERT(floatingpoint_to_ubv_idx == 11); + + 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(); + TS_ASSERT(floatingpoint_to_ubv_total_idx == 12); + + Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13); + uint32_t floatingpoint_to_sbv_idx = + floatingpoint_to_sbv_ot.getIndices(); + TS_ASSERT(floatingpoint_to_sbv_idx == 13); + + 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(); + TS_ASSERT(floatingpoint_to_sbv_total_idx == 14); + + Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5); + uint32_t tuple_update_idx = tuple_update_ot.getIndices(); + TS_ASSERT(tuple_update_idx == 5); + TS_ASSERT_THROWS(tuple_update_ot.getIndices(), + CVC4ApiException&); +} + +void OpBlack::testGetIndicesPairUint() +{ + Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); + TS_ASSERT(bitvector_extract_ot.isIndexed()); + std::pair bitvector_extract_indices = + bitvector_extract_ot.getIndices>(); + TS_ASSERT((bitvector_extract_indices == std::pair{4, 0})); + + Op floatingpoint_to_fp_ieee_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25); + std::pair floatingpoint_to_fp_ieee_bitvector_indices = + floatingpoint_to_fp_ieee_bitvector_ot + .getIndices>(); + TS_ASSERT((floatingpoint_to_fp_ieee_bitvector_indices + == std::pair{4, 25})); + + Op floatingpoint_to_fp_floatingpoint_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25); + std::pair floatingpoint_to_fp_floatingpoint_indices = + floatingpoint_to_fp_floatingpoint_ot + .getIndices>(); + TS_ASSERT((floatingpoint_to_fp_floatingpoint_indices + == std::pair{4, 25})); + + Op floatingpoint_to_fp_real_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25); + std::pair floatingpoint_to_fp_real_indices = + floatingpoint_to_fp_real_ot.getIndices>(); + TS_ASSERT((floatingpoint_to_fp_real_indices + == std::pair{4, 25})); + + Op floatingpoint_to_fp_signed_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25); + std::pair floatingpoint_to_fp_signed_bitvector_indices = + floatingpoint_to_fp_signed_bitvector_ot + .getIndices>(); + TS_ASSERT((floatingpoint_to_fp_signed_bitvector_indices + == std::pair{4, 25})); + + Op floatingpoint_to_fp_unsigned_bitvector_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25); + std::pair floatingpoint_to_fp_unsigned_bitvector_indices = + floatingpoint_to_fp_unsigned_bitvector_ot + .getIndices>(); + TS_ASSERT((floatingpoint_to_fp_unsigned_bitvector_indices + == std::pair{4, 25})); + + Op floatingpoint_to_fp_generic_ot = + d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25); + std::pair floatingpoint_to_fp_generic_indices = + floatingpoint_to_fp_generic_ot + .getIndices>(); + TS_ASSERT((floatingpoint_to_fp_generic_indices + == std::pair{4, 25})); + TS_ASSERT_THROWS(floatingpoint_to_fp_generic_ot.getIndices(), + CVC4ApiException&); +} diff --git a/test/unit/api/opterm_black.h b/test/unit/api/opterm_black.h deleted file mode 100644 index 0dd7587ff..000000000 --- a/test/unit/api/opterm_black.h +++ /dev/null @@ -1,214 +0,0 @@ -/********************* */ -/*! \file opterm_black.h - ** \verbatim - ** Top contributors (to current version): - ** Aina Niemetz - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 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.\endverbatim - ** - ** \brief Black box testing of the Term class - **/ - -#include - -#include "api/cvc4cpp.h" - -using namespace CVC4::api; - -class OpBlack : public CxxTest::TestSuite -{ - public: - void setUp() override {} - void tearDown() override {} - - void testGetKind(); - void testGetSort(); - void testIsNull(); - void testOpTermFromKind(); - void testGetIndicesString(); - void testGetIndicesKind(); - void testGetIndicesUint(); - void testGetIndicesPairUint(); - - private: - Solver d_solver; -}; - -void OpBlack::testGetKind() -{ - Op x; - TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&); - x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); - TS_ASSERT_THROWS_NOTHING(x.getKind()); -} - -void OpBlack::testGetSort() -{ - Op x; - TS_ASSERT_THROWS(x.getSort(), CVC4ApiException&); - x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); - TS_ASSERT_THROWS_NOTHING(x.getSort()); -} - -void OpBlack::testIsNull() -{ - Op x; - TS_ASSERT(x.isNull()); - x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); - TS_ASSERT(!x.isNull()); -} - -void OpBlack::testOpTermFromKind() -{ - Op plus(PLUS); - TS_ASSERT(!plus.isIndexed()); - TS_ASSERT_THROWS(plus.getIndices(), CVC4ApiException&); -} - -void OpBlack::testGetIndicesString() -{ - Op x; - TS_ASSERT_THROWS(x.getIndices(), CVC4ApiException&); - - Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4); - TS_ASSERT(divisible_ot.isIndexed()); - std::string divisible_idx = divisible_ot.getIndices(); - TS_ASSERT(divisible_idx == "4"); - - Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test"); - std::string record_update_idx = record_update_ot.getIndices(); - TS_ASSERT(record_update_idx == "test"); - TS_ASSERT_THROWS(record_update_ot.getIndices(), CVC4ApiException&); -} - -void OpBlack::testGetIndicesKind() -{ - Op chain_ot = d_solver.mkOp(CHAIN, AND); - TS_ASSERT(chain_ot.isIndexed()); - Kind chain_idx = chain_ot.getIndices(); - TS_ASSERT(chain_idx == AND); -} - -void OpBlack::testGetIndicesUint() -{ - 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(); - TS_ASSERT(bitvector_repeat_idx == 5); - TS_ASSERT_THROWS( - (bitvector_repeat_ot.getIndices>()), - CVC4ApiException&); - - Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6); - uint32_t bitvector_zero_extend_idx = - bitvector_zero_extend_ot.getIndices(); - TS_ASSERT(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(); - TS_ASSERT(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(); - TS_ASSERT(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(); - TS_ASSERT(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(); - TS_ASSERT(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(); - TS_ASSERT(floatingpoint_to_ubv_idx == 11); - - 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(); - TS_ASSERT(floatingpoint_to_ubv_total_idx == 12); - - Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13); - uint32_t floatingpoint_to_sbv_idx = - floatingpoint_to_sbv_ot.getIndices(); - TS_ASSERT(floatingpoint_to_sbv_idx == 13); - - 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(); - TS_ASSERT(floatingpoint_to_sbv_total_idx == 14); - - Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5); - uint32_t tuple_update_idx = tuple_update_ot.getIndices(); - TS_ASSERT(tuple_update_idx == 5); - TS_ASSERT_THROWS(tuple_update_ot.getIndices(), - CVC4ApiException&); -} - -void OpBlack::testGetIndicesPairUint() -{ - Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0); - TS_ASSERT(bitvector_extract_ot.isIndexed()); - std::pair bitvector_extract_indices = - bitvector_extract_ot.getIndices>(); - TS_ASSERT((bitvector_extract_indices == std::pair{4, 0})); - - Op floatingpoint_to_fp_ieee_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25); - std::pair floatingpoint_to_fp_ieee_bitvector_indices = - floatingpoint_to_fp_ieee_bitvector_ot - .getIndices>(); - TS_ASSERT((floatingpoint_to_fp_ieee_bitvector_indices - == std::pair{4, 25})); - - Op floatingpoint_to_fp_floatingpoint_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25); - std::pair floatingpoint_to_fp_floatingpoint_indices = - floatingpoint_to_fp_floatingpoint_ot - .getIndices>(); - TS_ASSERT((floatingpoint_to_fp_floatingpoint_indices - == std::pair{4, 25})); - - Op floatingpoint_to_fp_real_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25); - std::pair floatingpoint_to_fp_real_indices = - floatingpoint_to_fp_real_ot.getIndices>(); - TS_ASSERT((floatingpoint_to_fp_real_indices - == std::pair{4, 25})); - - Op floatingpoint_to_fp_signed_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25); - std::pair floatingpoint_to_fp_signed_bitvector_indices = - floatingpoint_to_fp_signed_bitvector_ot - .getIndices>(); - TS_ASSERT((floatingpoint_to_fp_signed_bitvector_indices - == std::pair{4, 25})); - - Op floatingpoint_to_fp_unsigned_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25); - std::pair floatingpoint_to_fp_unsigned_bitvector_indices = - floatingpoint_to_fp_unsigned_bitvector_ot - .getIndices>(); - TS_ASSERT((floatingpoint_to_fp_unsigned_bitvector_indices - == std::pair{4, 25})); - - Op floatingpoint_to_fp_generic_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25); - std::pair floatingpoint_to_fp_generic_indices = - floatingpoint_to_fp_generic_ot - .getIndices>(); - TS_ASSERT((floatingpoint_to_fp_generic_indices - == std::pair{4, 25})); - TS_ASSERT_THROWS(floatingpoint_to_fp_generic_ot.getIndices(), - CVC4ApiException&); -}