From 942f66a8b9dd92cb7c1ba72e6a521e86a1a7e341 Mon Sep 17 00:00:00 2001 From: makaimann Date: Sun, 11 Aug 2019 09:07:31 -0700 Subject: [PATCH] New C++ API: Add templated getIndices method for OpTerm (#3073) * Implement templated getIndices method for OpTerm * Add getIndices unit tests * Update src/api/cvc4cpp.cpp Co-Authored-By: Aina Niemetz * Update src/api/cvc4cpp.cpp Co-Authored-By: Aina Niemetz * Add comment about DIVISIBLE_OP * Update test/unit/api/opterm_black.h Co-Authored-By: Aina Niemetz * Update test/unit/api/opterm_black.h Co-Authored-By: Aina Niemetz * Update test/unit/api/opterm_black.h Co-Authored-By: Aina Niemetz * Update test/unit/api/opterm_black.h Co-Authored-By: Aina Niemetz * Add exception checks to other unit tests (instead of having its own function) * Fix unit test names in opterm_black.h * Add description to docstring for getIndices * Formatting * Clang format older commits * Use '-' in docstring list to match other docstrings * Support creating DIVISIBLE_OP with a string (for arbitrary precision integers) * Move mkOpTerm(DIVISIBLE_OP, ) test to solver_black.h * Fix pointer access * Replace switch statement with if statement * Guard string input for CVC4::Integer in mkOpTerm for consistency on GMP/CLN back-end --- src/api/cvc4cpp.cpp | 162 ++++++++++++++++++++++++++++++++++- src/api/cvc4cpp.h | 14 +++ test/unit/api/opterm_black.h | 151 ++++++++++++++++++++++++++++++++ test/unit/api/solver_black.h | 1 + 4 files changed, 324 insertions(+), 4 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index bdb5f2f59..942235e9c 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -1288,6 +1288,144 @@ Sort OpTerm::getSort() const bool OpTerm::isNull() const { return d_expr->isNull(); } +template <> +std::string OpTerm::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + std::string i; + Kind k = intToExtKind(d_expr->getKind()); + + if (k == DIVISIBLE_OP) + { + // DIVISIBLE_OP returns a string index to support + // arbitrary precision integers + CVC4::Integer _int = d_expr->getConst().k; + i = _int.toString(); + } + else if (k == RECORD_UPDATE_OP) + { + i = d_expr->getConst().getField(); + } + else + { + CVC4_API_CHECK(false) << "Can't get string index from" + << " kind " << kindToString(k); + } + + return i; +} + +template <> +Kind OpTerm::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + Kind kind = intToExtKind(d_expr->getKind()); + CVC4_API_KIND_CHECK_EXPECTED(kind == CHAIN_OP, kind) << "CHAIN_OP"; + return intToExtKind(d_expr->getConst().getOperator()); +} + +template <> +uint32_t OpTerm::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + uint32_t i; + Kind k = intToExtKind(d_expr->getKind()); + switch (k) + { + case BITVECTOR_REPEAT_OP: + i = d_expr->getConst().repeatAmount; + break; + case BITVECTOR_ZERO_EXTEND_OP: + i = d_expr->getConst().zeroExtendAmount; + break; + case BITVECTOR_SIGN_EXTEND_OP: + i = d_expr->getConst().signExtendAmount; + break; + case BITVECTOR_ROTATE_LEFT_OP: + i = d_expr->getConst().rotateLeftAmount; + break; + case BITVECTOR_ROTATE_RIGHT_OP: + i = d_expr->getConst().rotateRightAmount; + break; + case INT_TO_BITVECTOR_OP: + i = d_expr->getConst().size; + break; + case FLOATINGPOINT_TO_UBV_OP: + i = d_expr->getConst().bvs.size; + break; + case FLOATINGPOINT_TO_UBV_TOTAL_OP: + i = d_expr->getConst().bvs.size; + break; + case FLOATINGPOINT_TO_SBV_OP: + i = d_expr->getConst().bvs.size; + break; + case FLOATINGPOINT_TO_SBV_TOTAL_OP: + i = d_expr->getConst().bvs.size; + break; + case TUPLE_UPDATE_OP: i = d_expr->getConst().getIndex(); break; + default: + CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from" + << " kind " << kindToString(k); + } + return i; +} + +template <> +std::pair OpTerm::getIndices() const +{ + CVC4_API_CHECK_NOT_NULL; + std::pair indices; + Kind k = intToExtKind(d_expr->getKind()); + + // using if/else instead of case statement because want local variables + if (k == BITVECTOR_EXTRACT_OP) + { + CVC4::BitVectorExtract ext = d_expr->getConst(); + indices = std::make_pair(ext.high, ext.low); + } + else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP) + { + CVC4::FloatingPointToFPIEEEBitVector ext = + d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP) + { + CVC4::FloatingPointToFPFloatingPoint ext = + d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_REAL_OP) + { + CVC4::FloatingPointToFPReal ext = d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP) + { + CVC4::FloatingPointToFPSignedBitVector ext = + d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP) + { + CVC4::FloatingPointToFPUnsignedBitVector ext = + d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else if (k == FLOATINGPOINT_TO_FP_GENERIC_OP) + { + CVC4::FloatingPointToFPGeneric ext = + d_expr->getConst(); + indices = std::make_pair(ext.t.exponent(), ext.t.significand()); + } + else + { + CVC4_API_CHECK(false) << "Can't get pair indices from" + << " kind " << kindToString(k); + } + return indices; +} + std::string OpTerm::toString() const { return d_expr->toString(); } // !!! This is only temporarily available until the parser is fully migrated @@ -2724,10 +2862,26 @@ OpTerm Solver::mkOpTerm(Kind kind, Kind k) const OpTerm Solver::mkOpTerm(Kind kind, const std::string& arg) const { CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4_API_KIND_CHECK_EXPECTED(kind == RECORD_UPDATE_OP, kind) - << "RECORD_UPDATE_OP"; - - return *mkValHelper(CVC4::RecordUpdate(arg)).d_expr.get(); + CVC4_API_KIND_CHECK_EXPECTED( + (kind == RECORD_UPDATE_OP) || (kind == DIVISIBLE_OP), kind) + << "RECORD_UPDATE_OP or DIVISIBLE_OP"; + OpTerm res; + if (kind == RECORD_UPDATE_OP) + { + res = + *mkValHelper(CVC4::RecordUpdate(arg)).d_expr.get(); + } + else + { + /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP + * throws an std::invalid_argument exception. For consistency, we treat it + * as invalid. */ + CVC4_API_ARG_CHECK_EXPECTED(arg != ".", arg) + << "a string representing an integer, real or rational value."; + res = *mkValHelper(CVC4::Divisible(CVC4::Integer(arg))) + .d_expr.get(); + } + return res; CVC4_API_SOLVER_TRY_CATCH_END; } diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 2ff1cb91d..67e8bb6e7 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -872,6 +872,19 @@ class CVC4_PUBLIC OpTerm */ bool isNull() const; + /** + * Get the indices used to create this OpTerm. + * Supports the following template arguments: + * - string + * - Kind + * - uint32_t + * - pair + * Check the OpTerm Kind with getKind() to determine which argument to use. + * @return the indices used to create this OpTerm + */ + template + T getIndices() const; + /** * @return a string representation of this operator term */ @@ -1818,6 +1831,7 @@ class CVC4_PUBLIC Solver /** * Create operator of kind: * - RECORD_UPDATE_OP + * - DIVISIBLE_OP (to support arbitrary precision integers) * See enum Kind for a description of the parameters. * @param kind the kind of the operator * @param arg the string argument to this operator diff --git a/test/unit/api/opterm_black.h b/test/unit/api/opterm_black.h index 395ee8451..150cebcbf 100644 --- a/test/unit/api/opterm_black.h +++ b/test/unit/api/opterm_black.h @@ -27,6 +27,10 @@ class OpTermBlack : public CxxTest::TestSuite void testGetKind(); void testGetSort(); void testIsNull(); + void testGetIndicesString(); + void testGetIndicesKind(); + void testGetIndicesUint(); + void testGetIndicesPairUint(); private: Solver d_solver; @@ -55,3 +59,150 @@ void OpTermBlack::testIsNull() x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1); TS_ASSERT(!x.isNull()); } + +void OpTermBlack::testGetIndicesString() +{ + OpTerm x; + TS_ASSERT_THROWS(x.getIndices(), CVC4ApiException&); + + OpTerm divisible_ot = d_solver.mkOpTerm(DIVISIBLE_OP, 4); + std::string divisible_idx = divisible_ot.getIndices(); + TS_ASSERT(divisible_idx == "4"); + + OpTerm record_update_ot = d_solver.mkOpTerm(RECORD_UPDATE_OP, "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 OpTermBlack::testGetIndicesKind() +{ + OpTerm chain_ot = d_solver.mkOpTerm(CHAIN_OP, AND); + Kind chain_idx = chain_ot.getIndices(); + TS_ASSERT(chain_idx == AND); +} + +void OpTermBlack::testGetIndicesUint() +{ + OpTerm bitvector_repeat_ot = d_solver.mkOpTerm(BITVECTOR_REPEAT_OP, 5); + uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices(); + TS_ASSERT(bitvector_repeat_idx == 5); + TS_ASSERT_THROWS( + (bitvector_repeat_ot.getIndices>()), + CVC4ApiException&); + + OpTerm bitvector_zero_extend_ot = + d_solver.mkOpTerm(BITVECTOR_ZERO_EXTEND_OP, 6); + uint32_t bitvector_zero_extend_idx = + bitvector_zero_extend_ot.getIndices(); + TS_ASSERT(bitvector_zero_extend_idx == 6); + + OpTerm bitvector_sign_extend_ot = + d_solver.mkOpTerm(BITVECTOR_SIGN_EXTEND_OP, 7); + uint32_t bitvector_sign_extend_idx = + bitvector_sign_extend_ot.getIndices(); + TS_ASSERT(bitvector_sign_extend_idx == 7); + + OpTerm bitvector_rotate_left_ot = + d_solver.mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 8); + uint32_t bitvector_rotate_left_idx = + bitvector_rotate_left_ot.getIndices(); + TS_ASSERT(bitvector_rotate_left_idx == 8); + + OpTerm bitvector_rotate_right_ot = + d_solver.mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 9); + uint32_t bitvector_rotate_right_idx = + bitvector_rotate_right_ot.getIndices(); + TS_ASSERT(bitvector_rotate_right_idx == 9); + + OpTerm int_to_bitvector_ot = d_solver.mkOpTerm(INT_TO_BITVECTOR_OP, 10); + uint32_t int_to_bitvector_idx = int_to_bitvector_ot.getIndices(); + TS_ASSERT(int_to_bitvector_idx == 10); + + OpTerm floatingpoint_to_ubv_ot = + d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_OP, 11); + uint32_t floatingpoint_to_ubv_idx = + floatingpoint_to_ubv_ot.getIndices(); + TS_ASSERT(floatingpoint_to_ubv_idx == 11); + + OpTerm floatingpoint_to_ubv_total_ot = + d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_TOTAL_OP, 12); + uint32_t floatingpoint_to_ubv_total_idx = + floatingpoint_to_ubv_total_ot.getIndices(); + TS_ASSERT(floatingpoint_to_ubv_total_idx == 12); + + OpTerm floatingpoint_to_sbv_ot = + d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_OP, 13); + uint32_t floatingpoint_to_sbv_idx = + floatingpoint_to_sbv_ot.getIndices(); + TS_ASSERT(floatingpoint_to_sbv_idx == 13); + + OpTerm floatingpoint_to_sbv_total_ot = + d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_TOTAL_OP, 14); + uint32_t floatingpoint_to_sbv_total_idx = + floatingpoint_to_sbv_total_ot.getIndices(); + TS_ASSERT(floatingpoint_to_sbv_total_idx == 14); + + OpTerm tuple_update_ot = d_solver.mkOpTerm(TUPLE_UPDATE_OP, 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 OpTermBlack::testGetIndicesPairUint() +{ + OpTerm bitvector_extract_ot = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 4, 0); + std::pair bitvector_extract_indices = + bitvector_extract_ot.getIndices>(); + TS_ASSERT((bitvector_extract_indices == std::pair{4, 0})); + + OpTerm floatingpoint_to_fp_ieee_bitvector_ot = + d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, 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})); + + OpTerm floatingpoint_to_fp_floatingpoint_ot = + d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, 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})); + + OpTerm floatingpoint_to_fp_real_ot = + d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_REAL_OP, 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})); + + OpTerm floatingpoint_to_fp_signed_bitvector_ot = + d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, 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})); + + OpTerm floatingpoint_to_fp_unsigned_bitvector_ot = + d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, 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})); + + OpTerm floatingpoint_to_fp_generic_ot = + d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_GENERIC_OP, 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/solver_black.h b/test/unit/api/solver_black.h index a82807b3b..3782b900a 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -451,6 +451,7 @@ void SolverBlack::testMkOpTerm() // 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"), CVC4ApiException&); -- 2.30.2