From d2f0f6d468473cffee92d9835d9b4d0c88550253 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 14 Mar 2022 17:18:52 -0700 Subject: [PATCH] Rename TO_FP operator kinds. (#8285) FLOATINGPOINT_TO_FP_FP -> FLOATINGPOINT_TO_FP_FROM_FP FLOATINGPOINT_TO_FP_IEEE_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_IEEE_BV FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_SBV FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_UBV FLOATINGPOINT_TO_FP_REAL -> FLOATINGPOINT_TO_FP_FROM_REAL --- src/api/cpp/cvc5.cpp | 102 ++++++++++---------- src/api/cpp/cvc5.h | 10 +- src/api/cpp/cvc5_kind.h | 20 ++-- src/api/java/io/github/cvc5/api/Solver.java | 10 +- src/parser/smt2/smt2.cpp | 20 ++-- src/printer/smt2/smt2_printer.cpp | 30 +++--- src/proof/lfsc/lfsc_node_converter.cpp | 27 +++--- src/theory/fp/fp_word_blaster.cpp | 12 +-- src/theory/fp/kinds | 42 ++++---- src/theory/fp/theory_fp.cpp | 21 ++-- src/theory/fp/theory_fp_rewriter.cpp | 48 ++++----- src/theory/fp/theory_fp_type_rules.cpp | 6 +- test/unit/api/cpp/op_black.cpp | 32 +++--- test/unit/api/java/OpTest.java | 12 +-- test/unit/api/python/test_op.py | 77 +++++++-------- 15 files changed, 229 insertions(+), 240 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 1dffd5776..d1e0dc12e 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -238,15 +238,12 @@ const static std::unordered_map s_kinds{ {FLOATINGPOINT_IS_NAN, cvc5::Kind::FLOATINGPOINT_IS_NAN}, {FLOATINGPOINT_IS_NEG, cvc5::Kind::FLOATINGPOINT_IS_NEG}, {FLOATINGPOINT_IS_POS, cvc5::Kind::FLOATINGPOINT_IS_POS}, - {FLOATINGPOINT_TO_FP_FLOATINGPOINT, - cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT}, - {FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, - cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR}, - {FLOATINGPOINT_TO_FP_REAL, cvc5::Kind::FLOATINGPOINT_TO_FP_REAL}, - {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, - cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR}, - {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, - cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR}, + {FLOATINGPOINT_TO_FP_FROM_FP, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_FP}, + {FLOATINGPOINT_TO_FP_FROM_IEEE_BV, + cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV}, + {FLOATINGPOINT_TO_FP_FROM_REAL, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_REAL}, + {FLOATINGPOINT_TO_FP_FROM_SBV, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_SBV}, + {FLOATINGPOINT_TO_FP_FROM_UBV, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_UBV}, {FLOATINGPOINT_TO_FP_GENERIC, cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC}, {FLOATINGPOINT_TO_UBV, cvc5::Kind::FLOATINGPOINT_TO_UBV}, {FLOATINGPOINT_TO_SBV, cvc5::Kind::FLOATINGPOINT_TO_SBV}, @@ -534,24 +531,25 @@ const static std::unordered_map {cvc5::Kind::FLOATINGPOINT_IS_NAN, FLOATINGPOINT_IS_NAN}, {cvc5::Kind::FLOATINGPOINT_IS_NEG, FLOATINGPOINT_IS_NEG}, {cvc5::Kind::FLOATINGPOINT_IS_POS, FLOATINGPOINT_IS_POS}, - {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR}, - {cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR}, - {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, - FLOATINGPOINT_TO_FP_FLOATINGPOINT}, - {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT, - FLOATINGPOINT_TO_FP_FLOATINGPOINT}, - {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL}, - {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL, FLOATINGPOINT_TO_FP_REAL}, - {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR}, - {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR}, - {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR}, - {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR}, + {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP, + FLOATINGPOINT_TO_FP_FROM_IEEE_BV}, + {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV, + FLOATINGPOINT_TO_FP_FROM_IEEE_BV}, + {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_FP_OP, + FLOATINGPOINT_TO_FP_FROM_FP}, + {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_FP, FLOATINGPOINT_TO_FP_FROM_FP}, + {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_REAL_OP, + FLOATINGPOINT_TO_FP_FROM_REAL}, + {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_REAL, + FLOATINGPOINT_TO_FP_FROM_REAL}, + {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_SBV_OP, + FLOATINGPOINT_TO_FP_FROM_SBV}, + {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_SBV, + FLOATINGPOINT_TO_FP_FROM_SBV}, + {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_UBV_OP, + FLOATINGPOINT_TO_FP_FROM_UBV}, + {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_UBV, + FLOATINGPOINT_TO_FP_FROM_UBV}, {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP, FLOATINGPOINT_TO_FP_GENERIC}, {cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC, FLOATINGPOINT_TO_FP_GENERIC}, @@ -705,11 +703,11 @@ const static std::unordered_set s_indexed_kinds( FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_SBV, BITVECTOR_EXTRACT, - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, - FLOATINGPOINT_TO_FP_FLOATINGPOINT, - FLOATINGPOINT_TO_FP_REAL, - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, + FLOATINGPOINT_TO_FP_FROM_IEEE_BV, + FLOATINGPOINT_TO_FP_FROM_FP, + FLOATINGPOINT_TO_FP_FROM_REAL, + FLOATINGPOINT_TO_FP_FROM_SBV, + FLOATINGPOINT_TO_FP_FROM_UBV, FLOATINGPOINT_TO_FP_GENERIC}); namespace { @@ -1877,11 +1875,11 @@ size_t Op::getNumIndicesHelper() const case FLOATINGPOINT_TO_SBV: size = 1; break; case REGEXP_REPEAT: size = 1; break; case BITVECTOR_EXTRACT: size = 2; break; - case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: size = 2; break; - case FLOATINGPOINT_TO_FP_FLOATINGPOINT: size = 2; break; - case FLOATINGPOINT_TO_FP_REAL: size = 2; break; - case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: size = 2; break; - case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: size = 2; break; + case FLOATINGPOINT_TO_FP_FROM_IEEE_BV: size = 2; break; + case FLOATINGPOINT_TO_FP_FROM_FP: size = 2; break; + case FLOATINGPOINT_TO_FP_FROM_REAL: size = 2; break; + case FLOATINGPOINT_TO_FP_FROM_SBV: size = 2; break; + case FLOATINGPOINT_TO_FP_FROM_UBV: size = 2; break; case FLOATINGPOINT_TO_FP_GENERIC: size = 2; break; case REGEXP_LOOP: size = 2; break; case TUPLE_PROJECT: @@ -1980,7 +1978,7 @@ Term Op::getIndexHelper(size_t index) const : d_solver->mkRationalValHelper(ext.d_low); break; } - case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + case FLOATINGPOINT_TO_FP_FROM_IEEE_BV: { cvc5::FloatingPointToFPIEEEBitVector ext = d_node->getConst(); @@ -1990,7 +1988,7 @@ Term Op::getIndexHelper(size_t index) const : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); break; } - case FLOATINGPOINT_TO_FP_FLOATINGPOINT: + case FLOATINGPOINT_TO_FP_FROM_FP: { cvc5::FloatingPointToFPFloatingPoint ext = d_node->getConst(); @@ -1999,7 +1997,7 @@ Term Op::getIndexHelper(size_t index) const : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); break; } - case FLOATINGPOINT_TO_FP_REAL: + case FLOATINGPOINT_TO_FP_FROM_REAL: { cvc5::FloatingPointToFPReal ext = d_node->getConst(); @@ -2009,7 +2007,7 @@ Term Op::getIndexHelper(size_t index) const : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); break; } - case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + case FLOATINGPOINT_TO_FP_FROM_SBV: { cvc5::FloatingPointToFPSignedBitVector ext = d_node->getConst(); @@ -2018,7 +2016,7 @@ Term Op::getIndexHelper(size_t index) const : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); break; } - case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + case FLOATINGPOINT_TO_FP_FROM_UBV: { cvc5::FloatingPointToFPUnsignedBitVector ext = d_node->getConst(); @@ -2147,34 +2145,34 @@ std::pair Op::getIndices() const cvc5::BitVectorExtract ext = d_node->getConst(); indices = std::make_pair(ext.d_high, ext.d_low); } - else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR) + else if (k == FLOATINGPOINT_TO_FP_FROM_IEEE_BV) { cvc5::FloatingPointToFPIEEEBitVector ext = d_node->getConst(); indices = std::make_pair(ext.getSize().exponentWidth(), ext.getSize().significandWidth()); } - else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) + else if (k == FLOATINGPOINT_TO_FP_FROM_FP) { cvc5::FloatingPointToFPFloatingPoint ext = d_node->getConst(); indices = std::make_pair(ext.getSize().exponentWidth(), ext.getSize().significandWidth()); } - else if (k == FLOATINGPOINT_TO_FP_REAL) + else if (k == FLOATINGPOINT_TO_FP_FROM_REAL) { cvc5::FloatingPointToFPReal ext = d_node->getConst(); indices = std::make_pair(ext.getSize().exponentWidth(), ext.getSize().significandWidth()); } - else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) + else if (k == FLOATINGPOINT_TO_FP_FROM_SBV) { cvc5::FloatingPointToFPSignedBitVector ext = d_node->getConst(); indices = std::make_pair(ext.getSize().exponentWidth(), ext.getSize().significandWidth()); } - else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR) + else if (k == FLOATINGPOINT_TO_FP_FROM_UBV) { cvc5::FloatingPointToFPUnsignedBitVector ext = d_node->getConst(); @@ -6512,35 +6510,35 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const cvc5::BitVectorExtract(arg1, arg2)) .d_node); break; - case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + case FLOATINGPOINT_TO_FP_FROM_IEEE_BV: res = Op(this, kind, *mkValHelper( cvc5::FloatingPointToFPIEEEBitVector(arg1, arg2)) .d_node); break; - case FLOATINGPOINT_TO_FP_FLOATINGPOINT: + case FLOATINGPOINT_TO_FP_FROM_FP: res = Op(this, kind, *mkValHelper( cvc5::FloatingPointToFPFloatingPoint(arg1, arg2)) .d_node); break; - case FLOATINGPOINT_TO_FP_REAL: + case FLOATINGPOINT_TO_FP_FROM_REAL: res = Op(this, kind, *mkValHelper( cvc5::FloatingPointToFPReal(arg1, arg2)) .d_node); break; - case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + case FLOATINGPOINT_TO_FP_FROM_SBV: res = Op(this, kind, *mkValHelper( cvc5::FloatingPointToFPSignedBitVector(arg1, arg2)) .d_node); break; - case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + case FLOATINGPOINT_TO_FP_FROM_UBV: res = Op(this, kind, *mkValHelper( diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 3a10aa0a6..037c14938 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3404,11 +3404,11 @@ class CVC5_EXPORT Solver /** * Create operator of Kind: * - BITVECTOR_EXTRACT - * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR - * - FLOATINGPOINT_TO_FP_FLOATINGPOINT - * - FLOATINGPOINT_TO_FP_REAL - * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR - * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR + * - FLOATINGPOINT_TO_FP_FROM_IEEE_BV + * - FLOATINGPOINT_TO_FP_FROM_FP + * - FLOATINGPOINT_TO_FP_FROM_REAL + * - FLOATINGPOINT_TO_FP_FROM_SBV + * - FLOATINGPOINT_TO_FP_FROM_UBV * - FLOATINGPOINT_TO_FP_GENERIC * See enum Kind for a description of the parameters. * @param kind the kind of the operator diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 24b1b5ed7..e4ddcaa00 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -1643,14 +1643,14 @@ enum Kind : int32_t * Conversion from an IEEE-754 bit vector to floating-point. * * Parameters: - * - 1: Op of kind FLOATINGPOINT_TO_FP_IEEE_BITVECTOR + * - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_IEEE_BV * - 2: Term of sort FloatingPoint * * Create with: * - `Solver::mkTerm(const Op& op, const Term& child) const` * - `Solver::mkTerm(const Op& op, const std::vector& children) const` */ - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, + FLOATINGPOINT_TO_FP_FROM_IEEE_BV, /** * Operator for to_fp from floating point. * @@ -1664,14 +1664,14 @@ enum Kind : int32_t * Conversion between floating-point sorts. * * Parameters: - * - 1: Op of kind FLOATINGPOINT_TO_FP_FLOATINGPOINT + * - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_FP * - 2: Term of sort FloatingPoint * * Create with: * - `Solver::mkTerm(const Op& op, const Term& child) const` * - `Solver::mkTerm(const Op& op, const std::vector& children) const` */ - FLOATINGPOINT_TO_FP_FLOATINGPOINT, + FLOATINGPOINT_TO_FP_FROM_FP, /** * Operator for to_fp from real. * @@ -1685,14 +1685,14 @@ enum Kind : int32_t * Conversion from a real to floating-point. * * Parameters: - * - 1: Op of kind FLOATINGPOINT_TO_FP_REAL + * - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_REAL * - 2: Term of sort FloatingPoint * * Create with: * - `Solver::mkTerm(const Op& op, const Term& child) const` * - `Solver::mkTerm(const Op& op, const std::vector& children) const` */ - FLOATINGPOINT_TO_FP_REAL, + FLOATINGPOINT_TO_FP_FROM_REAL, /** * Operator for to_fp from signed bit vector * @@ -1706,14 +1706,14 @@ enum Kind : int32_t * Conversion from a signed bit vector to floating-point. * * Parameters: - * - 1: Op of kind FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR + * - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_SBV * - 2: Term of sort FloatingPoint * * Create with: * - `Solver::mkTerm(const Op& op, const Term& child) const` * - `Solver::mkTerm(const Op& op, const std::vector& children) const` */ - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, + FLOATINGPOINT_TO_FP_FROM_SBV, /** * Operator for to_fp from unsigned bit vector. * @@ -1727,14 +1727,14 @@ enum Kind : int32_t * Converting an unsigned bit vector to floating-point. * * Parameters: - * - 1: Op of kind FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR + * - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_UBV * - 2: Term of sort FloatingPoint * * Create with: * - `Solver::mkTerm(const Op& op, const Term& child) const` * - `Solver::mkTerm(const Op& op, const std::vector& children) const` */ - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, + FLOATINGPOINT_TO_FP_FROM_UBV, /** * Operator for a generic to_fp. * diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 6e73b3300..6fd3444eb 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -732,11 +732,11 @@ public class Solver implements IPointer, AutoCloseable /** * Create operator of Kind: * - BITVECTOR_EXTRACT - * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR - * - FLOATINGPOINT_TO_FP_FLOATINGPOINT - * - FLOATINGPOINT_TO_FP_REAL - * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR - * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR + * - FLOATINGPOINT_TO_FP_FROM_IEEE_BV + * - FLOATINGPOINT_TO_FP_FROM_FP + * - FLOATINGPOINT_TO_FP_FROM_REAL + * - FLOATINGPOINT_TO_FP_FROM_SBV + * - FLOATINGPOINT_TO_FP_FROM_UBV * - FLOATINGPOINT_TO_FP_GENERIC * See enum Kind for a description of the parameters. * @param kind the kind of the operator diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index ec83dff0b..41389489f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -237,8 +237,8 @@ void Smt2::addFloatingPointOperators() { addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC, api::FLOATINGPOINT_TO_FP_GENERIC, "to_fp"); - addIndexedOperator(api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, - api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_UBV, + api::FLOATINGPOINT_TO_FP_FROM_UBV, "to_fp_unsigned"); addIndexedOperator( api::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv"); @@ -247,17 +247,17 @@ void Smt2::addFloatingPointOperators() { if (!strictModeEnabled()) { - addIndexedOperator(api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, - api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV, + api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV, "to_fp_bv"); - addIndexedOperator(api::FLOATINGPOINT_TO_FP_FLOATINGPOINT, - api::FLOATINGPOINT_TO_FP_FLOATINGPOINT, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_FP, + api::FLOATINGPOINT_TO_FP_FROM_FP, "to_fp_fp"); - addIndexedOperator(api::FLOATINGPOINT_TO_FP_REAL, - api::FLOATINGPOINT_TO_FP_REAL, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_REAL, + api::FLOATINGPOINT_TO_FP_FROM_REAL, "to_fp_real"); - addIndexedOperator(api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, - api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, + addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_SBV, + api::FLOATINGPOINT_TO_FP_FROM_SBV, "to_fp_signed"); } } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 72d303be8..cd37cd049 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -384,7 +384,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::INT_TO_BITVECTOR_OP: out << "(_ int2bv " << n.getConst().d_size << ")"; break; - case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP: + case kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP: out << "(_ to_fp " << n.getConst() .getSize() @@ -395,7 +395,7 @@ void Smt2Printer::toStream(std::ostream& out, .significandWidth() << ")"; break; - case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP: + case kind::FLOATINGPOINT_TO_FP_FROM_FP_OP: out << "(_ to_fp " << n.getConst() .getSize() @@ -406,14 +406,14 @@ void Smt2Printer::toStream(std::ostream& out, .significandWidth() << ")"; break; - case kind::FLOATINGPOINT_TO_FP_REAL_OP: + case kind::FLOATINGPOINT_TO_FP_FROM_REAL_OP: out << "(_ to_fp " << n.getConst().getSize().exponentWidth() << ' ' << n.getConst().getSize().significandWidth() << ")"; break; - case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP: + case kind::FLOATINGPOINT_TO_FP_FROM_SBV_OP: out << "(_ to_fp " << n.getConst() .getSize() @@ -424,7 +424,7 @@ void Smt2Printer::toStream(std::ostream& out, .significandWidth() << ")"; break; - case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP: + case kind::FLOATINGPOINT_TO_FP_FROM_UBV_OP: out << "(_ to_fp_unsigned " << n.getConst() .getSize() @@ -755,11 +755,11 @@ void Smt2Printer::toStream(std::ostream& out, } // fp theory - case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: - case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: - case kind::FLOATINGPOINT_TO_FP_REAL: - case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: - case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + case kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV: + case kind::FLOATINGPOINT_TO_FP_FROM_FP: + case kind::FLOATINGPOINT_TO_FP_FROM_REAL: + case kind::FLOATINGPOINT_TO_FP_FROM_SBV: + case kind::FLOATINGPOINT_TO_FP_FROM_UBV: case kind::FLOATINGPOINT_TO_FP_GENERIC: case kind::FLOATINGPOINT_TO_UBV: case kind::FLOATINGPOINT_TO_SBV: @@ -1196,11 +1196,11 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::FLOATINGPOINT_IS_NEG: return "fp.isNegative"; case kind::FLOATINGPOINT_IS_POS: return "fp.isPositive"; - case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: return "to_fp"; - case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: return "to_fp"; - case kind::FLOATINGPOINT_TO_FP_REAL: return "to_fp"; - case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return "to_fp"; - case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return "to_fp_unsigned"; + case kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV: return "to_fp"; + case kind::FLOATINGPOINT_TO_FP_FROM_FP: return "to_fp"; + case kind::FLOATINGPOINT_TO_FP_FROM_REAL: return "to_fp"; + case kind::FLOATINGPOINT_TO_FP_FROM_SBV: return "to_fp"; + case kind::FLOATINGPOINT_TO_FP_FROM_UBV: return "to_fp_unsigned"; case kind::FLOATINGPOINT_TO_FP_GENERIC: return "to_fp_unsigned"; case kind::FLOATINGPOINT_TO_UBV: return "fp.to_ubv"; case kind::FLOATINGPOINT_TO_UBV_TOTAL: return "fp.to_ubv_total"; diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index cbb945584..3a9e26d55 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -839,11 +839,12 @@ bool LfscNodeConverter::isIndexedOperatorKind(Kind k) || k == BITVECTOR_ZERO_EXTEND || k == BITVECTOR_SIGN_EXTEND || k == BITVECTOR_ROTATE_LEFT || k == BITVECTOR_ROTATE_RIGHT || k == INT_TO_BITVECTOR || k == IAND - || k == FLOATINGPOINT_TO_FP_FLOATINGPOINT - || k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR - || k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR - || k == FLOATINGPOINT_TO_FP_REAL || k == FLOATINGPOINT_TO_FP_GENERIC - || k == APPLY_UPDATER || k == APPLY_TESTER; + || k == FLOATINGPOINT_TO_FP_FROM_FP + || k == FLOATINGPOINT_TO_FP_FROM_IEEE_BV + || k == FLOATINGPOINT_TO_FP_FROM_SBV + || k == FLOATINGPOINT_TO_FP_FROM_REAL + || k == FLOATINGPOINT_TO_FP_GENERIC || k == APPLY_UPDATER + || k == APPLY_TESTER; } std::vector LfscNodeConverter::getOperatorIndices(Kind k, Node n) @@ -893,7 +894,7 @@ std::vector LfscNodeConverter::getOperatorIndices(Kind k, Node n) case IAND: indices.push_back(nm->mkConstInt(Rational(n.getConst().d_size))); break; - case FLOATINGPOINT_TO_FP_FLOATINGPOINT: + case FLOATINGPOINT_TO_FP_FROM_FP: { const FloatingPointToFPFloatingPoint& ffp = n.getConst(); @@ -901,7 +902,7 @@ std::vector LfscNodeConverter::getOperatorIndices(Kind k, Node n) indices.push_back(nm->mkConstInt(ffp.getSize().significandWidth())); } break; - case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + case FLOATINGPOINT_TO_FP_FROM_IEEE_BV: { const FloatingPointToFPIEEEBitVector& fbv = n.getConst(); @@ -909,7 +910,7 @@ std::vector LfscNodeConverter::getOperatorIndices(Kind k, Node n) indices.push_back(nm->mkConstInt(fbv.getSize().significandWidth())); } break; - case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + case FLOATINGPOINT_TO_FP_FROM_SBV: { const FloatingPointToFPSignedBitVector& fsbv = n.getConst(); @@ -917,7 +918,7 @@ std::vector LfscNodeConverter::getOperatorIndices(Kind k, Node n) indices.push_back(nm->mkConstInt(fsbv.getSize().significandWidth())); } break; - case FLOATINGPOINT_TO_FP_REAL: + case FLOATINGPOINT_TO_FP_FROM_REAL: { const FloatingPointToFPReal& fr = n.getConst(); indices.push_back(nm->mkConstInt(fr.getSize().exponentWidth())); @@ -1057,19 +1058,19 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply) } } // must avoid overloading for to_fp variants - if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT) + if (k == FLOATINGPOINT_TO_FP_FROM_FP) { opName << "to_fp_fp"; } - else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR) + else if (k == FLOATINGPOINT_TO_FP_FROM_IEEE_BV) { opName << "to_fp_ieee_bv"; } - else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR) + else if (k == FLOATINGPOINT_TO_FP_FROM_SBV) { opName << "to_fp_sbv"; } - else if (k == FLOATINGPOINT_TO_FP_REAL) + else if (k == FLOATINGPOINT_TO_FP_FROM_REAL) { opName << "to_fp_real"; } diff --git a/src/theory/fp/fp_word_blaster.cpp b/src/theory/fp/fp_word_blaster.cpp index 2ff2ec4aa..41d78b44d 100644 --- a/src/theory/fp/fp_word_blaster.cpp +++ b/src/theory/fp/fp_word_blaster.cpp @@ -803,7 +803,7 @@ Node FpWordBlaster::sbvToNode(const sbv& s) const { return s; } FpWordBlaster::uf FpWordBlaster::buildComponents(TNode current) { Assert(Theory::isLeafOf(current, THEORY_FP) - || current.getKind() == kind::FLOATINGPOINT_TO_FP_REAL); + || current.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_REAL); NodeManager* nm = NodeManager::currentNM(); uf tmp(nm->mkNode(kind::FLOATINGPOINT_COMPONENT_NAN, current), @@ -1050,7 +1050,7 @@ Node FpWordBlaster::wordBlast(TNode node) break; /* ---- Conversions ---- */ - case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT: + case kind::FLOATINGPOINT_TO_FP_FROM_FP: Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); Assert(d_fpMap.find(cur[1]) != d_fpMap.end()); d_fpMap.insert(cur, @@ -1073,12 +1073,12 @@ Node FpWordBlaster::wordBlast(TNode node) } break; - case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: + case kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV: Assert(cur[0].getType().isBitVector()); d_fpMap.insert(cur, symfpu::unpack(fpt(t), ubv(cur[0]))); break; - case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: + case kind::FLOATINGPOINT_TO_FP_FROM_SBV: Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); d_fpMap.insert( cur, @@ -1086,7 +1086,7 @@ Node FpWordBlaster::wordBlast(TNode node) fpt(t), (*d_rmMap.find(cur[0])).second, sbv(cur[1]))); break; - case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: + case kind::FLOATINGPOINT_TO_FP_FROM_UBV: Assert(d_rmMap.find(cur[0]) != d_rmMap.end()); d_fpMap.insert( cur, @@ -1094,7 +1094,7 @@ Node FpWordBlaster::wordBlast(TNode node) fpt(t), (*d_rmMap.find(cur[0])).second, ubv(cur[1]))); break; - case kind::FLOATINGPOINT_TO_FP_REAL: + case kind::FLOATINGPOINT_TO_FP_FROM_REAL: d_fpMap.insert(cur, buildComponents(cur)); // Rely on the real theory and theory combination // to handle the value diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index 08ccde2f5..204459496 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -27,7 +27,7 @@ constant CONST_ROUNDINGMODE \ RoundingMode \ ::cvc5::RoundingModeHashFunction \ "util/roundingmode.h" \ - "a floating-point rounding mode" + "a floating-point rounding mode" typerule CONST_ROUNDINGMODE ::cvc5::theory::fp::RoundingModeConstantTypeRule @@ -157,70 +157,70 @@ typerule FLOATINGPOINT_IS_POS ::cvc5::theory::fp::FloatingPointTestTypeRule -constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \ +constant FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP \ class \ FloatingPointToFPIEEEBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x1>" \ "util/floatingpoint.h" \ "operator for to_fp from bit vector" -typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule -parameterized FLOATINGPOINT_TO_FP_IEEE_BITVECTOR FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP 1 "convert an IEEE-754 bit vector to floating-point" -typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR ::cvc5::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule +parameterized FLOATINGPOINT_TO_FP_FROM_IEEE_BV FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP 1 "convert an IEEE-754 bit vector to floating-point" +typerule FLOATINGPOINT_TO_FP_FROM_IEEE_BV ::cvc5::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule -constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \ +constant FLOATINGPOINT_TO_FP_FROM_FP_OP \ class \ FloatingPointToFPFloatingPoint \ "::cvc5::FloatingPointConvertSortHashFunction<0x2>" \ "util/floatingpoint.h" \ "operator for to_fp from floating point" -typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_FP_FROM_FP_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule -parameterized FLOATINGPOINT_TO_FP_FLOATINGPOINT FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP 2 "convert between floating-point sorts" -typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT ::cvc5::theory::fp::FloatingPointToFPFloatingPointTypeRule +parameterized FLOATINGPOINT_TO_FP_FROM_FP FLOATINGPOINT_TO_FP_FROM_FP_OP 2 "convert between floating-point sorts" +typerule FLOATINGPOINT_TO_FP_FROM_FP ::cvc5::theory::fp::FloatingPointToFPFloatingPointTypeRule -constant FLOATINGPOINT_TO_FP_REAL_OP \ +constant FLOATINGPOINT_TO_FP_FROM_REAL_OP \ class \ FloatingPointToFPReal \ "::cvc5::FloatingPointConvertSortHashFunction<0x4>" \ "util/floatingpoint.h" \ "operator for to_fp from real" -typerule FLOATINGPOINT_TO_FP_REAL_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_FP_FROM_REAL_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule -parameterized FLOATINGPOINT_TO_FP_REAL FLOATINGPOINT_TO_FP_REAL_OP 2 "convert a real to floating-point" -typerule FLOATINGPOINT_TO_FP_REAL ::cvc5::theory::fp::FloatingPointToFPRealTypeRule +parameterized FLOATINGPOINT_TO_FP_FROM_REAL FLOATINGPOINT_TO_FP_FROM_REAL_OP 2 "convert a real to floating-point" +typerule FLOATINGPOINT_TO_FP_FROM_REAL ::cvc5::theory::fp::FloatingPointToFPRealTypeRule -constant FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP \ +constant FLOATINGPOINT_TO_FP_FROM_SBV_OP \ class \ FloatingPointToFPSignedBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x8>" \ "util/floatingpoint.h" \ "operator for to_fp from signed bit vector" -typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_FP_FROM_SBV_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule -parameterized FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP 2 "convert a signed bit vector to floating-point" -typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR ::cvc5::theory::fp::FloatingPointToFPSignedBitVectorTypeRule +parameterized FLOATINGPOINT_TO_FP_FROM_SBV FLOATINGPOINT_TO_FP_FROM_SBV_OP 2 "convert a signed bit vector to floating-point" +typerule FLOATINGPOINT_TO_FP_FROM_SBV ::cvc5::theory::fp::FloatingPointToFPSignedBitVectorTypeRule -constant FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP \ +constant FLOATINGPOINT_TO_FP_FROM_UBV_OP \ class \ FloatingPointToFPUnsignedBitVector \ "::cvc5::FloatingPointConvertSortHashFunction<0x10>" \ "util/floatingpoint.h" \ "operator for to_fp from unsigned bit vector" -typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule +typerule FLOATINGPOINT_TO_FP_FROM_UBV_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule -parameterized FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP 2 "convert an unsigned bit vector to floating-point" -typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR ::cvc5::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule +parameterized FLOATINGPOINT_TO_FP_FROM_UBV FLOATINGPOINT_TO_FP_FROM_UBV_OP 2 "convert an unsigned bit vector to floating-point" +typerule FLOATINGPOINT_TO_FP_FROM_UBV ::cvc5::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 1817e53ff..d5f665d1e 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -122,12 +122,11 @@ void TheoryFp::finishInit() d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_NEG); d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_POS); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_REAL); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR); - d_equalityEngine->addFunctionKind( - kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FROM_FP); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FROM_REAL); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FROM_SBV); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FROM_UBV); // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_GENERIC); // // Needed in parsing, should be rewritten away @@ -245,7 +244,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) // Then the backwards constraints Node floatAboveAbstract = rewrite( - nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, + nm->mkNode(kind::FLOATINGPOINT_TO_FP_FROM_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst())), nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE), @@ -262,7 +261,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) handleLemma(bg, InferenceId::FP_PREPROCESS); Node floatBelowAbstract = rewrite( - nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, + nm->mkNode(kind::FLOATINGPOINT_TO_FP_FROM_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst())), nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE), @@ -287,7 +286,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) return false; } } - else if (k == kind::FLOATINGPOINT_TO_FP_REAL) + else if (k == kind::FLOATINGPOINT_TO_FP_FROM_REAL) { // Get the values Assert(m->hasTerm(abstract)) << "Term " << abstract << " not in model"; @@ -313,7 +312,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) NodeManager *nm = NodeManager::currentNM(); Node evaluate = - nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, + nm->mkNode(kind::FLOATINGPOINT_TO_FP_FROM_REAL, nm->mkConst(FloatingPointToFPReal( concrete.getType().getConst())), rmValue, @@ -576,7 +575,7 @@ void TheoryFp::registerTerm(TNode node) // TODO : bounds on the output from largest floats, #1914 } - else if (k == kind::FLOATINGPOINT_TO_FP_REAL) + else if (k == kind::FLOATINGPOINT_TO_FP_FROM_REAL) { // Purify ((_ to_fp eb sb) rm x) NodeManager* nm = NodeManager::currentNM(); diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index 0fddbe9b4..655299af9 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -389,7 +389,7 @@ namespace rewrite { RewriteResponse toFPSignedBV(TNode node, bool isPreRewrite) { Assert(!isPreRewrite); - Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR); + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_SBV); /* symFPU does not allow conversions from signed bit-vector of size 1 */ if (node[1].getType().getBitVectorSize() == 1) @@ -778,7 +778,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse convertFromIEEEBitVectorLiteral(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR); + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV); TNode op = node.getOperator(); const FloatingPointToFPIEEEBitVector ¶m = op.getConst(); @@ -794,7 +794,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse constantConvert(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT); + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_FP); Assert(node.getNumChildren() == 2); RoundingMode rm(node[0].getConst()); @@ -808,7 +808,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse convertFromRealLiteral(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL); + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_REAL); TNode op = node.getOperator(); const FloatingPointSize& size = @@ -826,7 +826,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse convertFromSBV(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR); + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_SBV); TNode op = node.getOperator(); const FloatingPointSize& size = @@ -854,7 +854,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite) RewriteResponse convertFromUBV(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR); + Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_UBV); TNode op = node.getOperator(); const FloatingPointSize& size = @@ -1174,15 +1174,11 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_preRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity; /******** Conversions ********/ - d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = - rewrite::identity; - d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = - rewrite::identity; - d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::identity; - d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = - rewrite::identity; - d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = - rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity; d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::identity; d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity; d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity; @@ -1265,15 +1261,13 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_postRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity; /******** Conversions ********/ - d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = - rewrite::identity; - d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = + d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] = rewrite::identity; - d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::identity; - d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = + d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity; + d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity; + d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] = rewrite::toFPSignedBV; - d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = - rewrite::identity; + d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = rewrite::identity; d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::removeToFPGeneric; d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity; @@ -1352,15 +1346,15 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_constantFoldTable[kind::FLOATINGPOINT_IS_POS] = constantFold::isPositive; /******** Conversions ********/ - d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = + d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] = constantFold::convertFromIEEEBitVectorLiteral; - d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = + d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = constantFold::constantConvert; - d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_REAL] = + d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = constantFold::convertFromRealLiteral; - d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = + d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] = constantFold::convertFromSBV; - d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = + d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] = constantFold::convertFromUBV; d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV] = constantFold::convertToUBV; d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV] = constantFold::convertToSBV; diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp index 77c1ef8f0..9a492b6c2 100644 --- a/src/theory/fp/theory_fp_type_rules.cpp +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -688,7 +688,7 @@ TypeNode FloatingPointComponentBit::computeType(NodeManager* nodeManager, "sort"); } if (!(Theory::isLeafOf(n[0], THEORY_FP) - || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) + || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_FROM_REAL)) { throw TypeCheckingExceptionPrivate(n, "floating-point bit component " @@ -718,7 +718,7 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager, "sort"); } if (!(Theory::isLeafOf(n[0], THEORY_FP) - || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) + || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_FROM_REAL)) { throw TypeCheckingExceptionPrivate(n, "floating-point exponent component " @@ -754,7 +754,7 @@ TypeNode FloatingPointComponentSignificand::computeType( "floating-point sort"); } if (!(Theory::isLeafOf(n[0], THEORY_FP) - || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL)) + || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_FROM_REAL)) { throw TypeCheckingExceptionPrivate(n, "floating-point significand " diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp index 9af3e9072..81501763c 100644 --- a/test/unit/api/cpp/op_black.cpp +++ b/test/unit/api/cpp/op_black.cpp @@ -60,14 +60,15 @@ TEST_F(TestApiBlackOp, getNumIndices) 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); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 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); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 25); + Op floatingpoint_to_fp_real = + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25); Op floatingpoint_to_fp_signed_bitvector = - d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25); Op floatingpoint_to_fp_unsigned_bitvector = - d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 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); @@ -106,14 +107,15 @@ TEST_F(TestApiBlackOp, subscriptOperator) 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); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 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); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 5); + Op floatingpoint_to_fp_real = + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 5); Op floatingpoint_to_fp_signed_bitvector = - d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 5); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 5); Op floatingpoint_to_fp_unsigned_bitvector = - d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 5); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 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); @@ -204,7 +206,7 @@ TEST_F(TestApiBlackOp, getIndicesPairUint) (bitvector_extract_indices == std::pair{4, 0})); Op floatingpoint_to_fp_ieee_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 25); std::pair floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot .getIndices>(); @@ -212,7 +214,7 @@ TEST_F(TestApiBlackOp, getIndicesPairUint) == std::pair{4, 25})); Op floatingpoint_to_fp_floatingpoint_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 25); std::pair floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot .getIndices>(); @@ -220,14 +222,14 @@ TEST_F(TestApiBlackOp, getIndicesPairUint) == std::pair{4, 25})); Op floatingpoint_to_fp_real_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25); std::pair floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices>(); ASSERT_TRUE((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); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25); std::pair floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot .getIndices>(); @@ -235,7 +237,7 @@ TEST_F(TestApiBlackOp, getIndicesPairUint) == std::pair{4, 25})); Op floatingpoint_to_fp_unsigned_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 4, 25); std::pair floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot .getIndices>(); diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java index 2de478b58..393f658c5 100644 --- a/test/unit/api/java/OpTest.java +++ b/test/unit/api/java/OpTest.java @@ -118,29 +118,27 @@ class OpTest assertArrayEquals(bitvector_extract_indices, new int[] {4, 0}); Op floatingpoint_to_fp_ieee_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 25); int[] floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot.getIntegerIndices(); assertArrayEquals(floatingpoint_to_fp_ieee_bitvector_indices, new int[] {4, 25}); - Op floatingpoint_to_fp_floatingpoint_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25); + Op floatingpoint_to_fp_floatingpoint_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 25); int[] floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot.getIntegerIndices(); assertArrayEquals(floatingpoint_to_fp_floatingpoint_indices, new int[] {4, 25}); - Op floatingpoint_to_fp_real_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25); + Op floatingpoint_to_fp_real_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25); int[] floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIntegerIndices(); assertArrayEquals(floatingpoint_to_fp_real_indices, new int[] {4, 25}); - Op floatingpoint_to_fp_signed_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25); + Op floatingpoint_to_fp_signed_bitvector_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25); int[] floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot.getIntegerIndices(); assertArrayEquals(floatingpoint_to_fp_signed_bitvector_indices, new int[] {4, 25}); Op floatingpoint_to_fp_unsigned_bitvector_ot = - d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25); + d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 4, 25); int[] floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot.getIntegerIndices(); assertArrayEquals(floatingpoint_to_fp_unsigned_bitvector_indices, new int[] {4, 25}); diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py index 4059a4fb0..141c9d4e2 100644 --- a/test/unit/api/python/test_op.py +++ b/test/unit/api/python/test_op.py @@ -57,13 +57,11 @@ def test_get_num_indices(solver): iand = solver.mkOp(Kind.Iand, 3) floatingpoint_to_ubv = solver.mkOp(Kind.FPToUbv, 11) floatingopint_to_sbv = solver.mkOp(Kind.FPToSbv, 13) - floatingpoint_to_fp_ieee_bitvector = solver.mkOp(Kind.FPToFpIeeeBV, 4, 25) - floatingpoint_to_fp_floatingpoint = solver.mkOp(Kind.FPToFpFP, 4, 25) - floatingpoint_to_fp_real = solver.mkOp(Kind.FPToFpReal, 4, 25) - floatingpoint_to_fp_signed_bitvector = solver.mkOp(Kind.FPToFpSignedBV, 4, - 25) - floatingpoint_to_fp_unsigned_bitvector = solver.mkOp( - Kind.FPToFpUnsignedBV, 4, 25) + floatingpoint_to_fp_from_ieee_bv = solver.mkOp(Kind.FPToFpFromIeeeBv, 4, 25) + floatingpoint_to_fp_from_fp = solver.mkOp(Kind.FPToFpFromFp, 4, 25) + floatingpoint_to_fp_from_real = solver.mkOp(Kind.FPToFpFromReal, 4, 25) + floatingpoint_to_fp_from_sbv = solver.mkOp(Kind.FPToFpFromSbv, 4, 25) + floatingpoint_to_fp_from_ubv = solver.mkOp(Kind.FPToFpFromUbv, 4, 25) floatingpoint_to_fp_generic = solver.mkOp(Kind.FPToFpGeneric, 4, 25) regexp_loop = solver.mkOp(Kind.RegexpLoop, 2, 3) @@ -78,11 +76,11 @@ def test_get_num_indices(solver): assert 1 == iand.getNumIndices() assert 1 == floatingpoint_to_ubv.getNumIndices() assert 1 == floatingopint_to_sbv.getNumIndices() - assert 2 == floatingpoint_to_fp_ieee_bitvector.getNumIndices() - assert 2 == floatingpoint_to_fp_floatingpoint.getNumIndices() - assert 2 == floatingpoint_to_fp_real.getNumIndices() - assert 2 == floatingpoint_to_fp_signed_bitvector.getNumIndices() - assert 2 == floatingpoint_to_fp_unsigned_bitvector.getNumIndices() + assert 2 == floatingpoint_to_fp_from_ieee_bv.getNumIndices() + assert 2 == floatingpoint_to_fp_from_fp.getNumIndices() + assert 2 == floatingpoint_to_fp_from_real.getNumIndices() + assert 2 == floatingpoint_to_fp_from_sbv.getNumIndices() + assert 2 == floatingpoint_to_fp_from_ubv.getNumIndices() assert 2 == floatingpoint_to_fp_generic.getNumIndices() assert 2 == regexp_loop.getNumIndices() @@ -142,36 +140,35 @@ def test_get_indices_pair_uint(solver): bitvector_extract_indices = bitvector_extract_ot.getIndices() assert bitvector_extract_indices == (4, 0) - floatingpoint_to_fp_ieee_bitvector_ot = solver.mkOp( - Kind.FPToFpIeeeBV, 4, 25) - floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot.getIndices( - ) - assert floatingpoint_to_fp_ieee_bitvector_indices == (4, 25) - - floatingpoint_to_fp_floatingpoint_ot = solver.mkOp(Kind.FPToFpFP, 4, 25) - floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot.getIndices( - ) - assert floatingpoint_to_fp_floatingpoint_indices == (4, 25) - - floatingpoint_to_fp_real_ot = solver.mkOp(Kind.FPToFpReal, 4, 25) - floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices() - assert floatingpoint_to_fp_real_indices == (4, 25) - - floatingpoint_to_fp_signed_bitvector_ot = solver.mkOp( - Kind.FPToFpSignedBV, 4, 25) - floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot.getIndices( - ) - assert floatingpoint_to_fp_signed_bitvector_indices == (4, 25) - - floatingpoint_to_fp_unsigned_bitvector_ot = solver.mkOp( - Kind.FPToFpUnsignedBV, 4, 25) - floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot.getIndices( - ) - assert floatingpoint_to_fp_unsigned_bitvector_indices == (4, 25) + floatingpoint_to_fp_from_ieee_bv_ot = \ + solver.mkOp(Kind.FPToFpFromIeeeBv, 4, 25) + floatingpoint_to_fp_from_ieee_bv_indices = \ + floatingpoint_to_fp_from_ieee_bv_ot.getIndices() + assert floatingpoint_to_fp_from_ieee_bv_indices == (4, 25) + + floatingpoint_to_fp_from_fp_ot = solver.mkOp(Kind.FPToFpFromFp, 4, 25) + floatingpoint_to_fp_from_fp_indices = \ + floatingpoint_to_fp_from_fp_ot.getIndices() + assert floatingpoint_to_fp_from_fp_indices == (4, 25) + + floatingpoint_to_fp_from_real_ot = solver.mkOp(Kind.FPToFpFromReal, 4, 25) + floatingpoint_to_fp_from_real_indices = \ + floatingpoint_to_fp_from_real_ot.getIndices() + assert floatingpoint_to_fp_from_real_indices == (4, 25) + + floatingpoint_to_fp_from_sbv_ot = solver.mkOp(Kind.FPToFpFromSbv, 4, 25) + floatingpoint_to_fp_from_sbv_indices = \ + floatingpoint_to_fp_from_sbv_ot.getIndices() + assert floatingpoint_to_fp_from_sbv_indices == (4, 25) + + floatingpoint_to_fp_from_ubv_ot = solver.mkOp(Kind.FPToFpFromUbv, 4, 25) + floatingpoint_to_fp_from_ubv_indices = \ + floatingpoint_to_fp_from_ubv_ot.getIndices() + assert floatingpoint_to_fp_from_ubv_indices == (4, 25) floatingpoint_to_fp_generic_ot = solver.mkOp(Kind.FPToFpGeneric, 4, 25) - floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot.getIndices( - ) + floatingpoint_to_fp_generic_indices = \ + floatingpoint_to_fp_generic_ot.getIndices() assert floatingpoint_to_fp_generic_indices == (4, 25) -- 2.30.2