From 3a97480ffab492f8272ad9c7c192d04b43eeea60 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 22 Mar 2022 01:36:54 -0700 Subject: [PATCH] [FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334) This commit removes the `FLOATINGPOINT_TO_FP_GENERIC` kind, which was only used in the parser and immediately rewritten by the floating-point arithmetic solver. It extends the `ParseOp` class to handle indexed operators of which we do not know the kind (`to_fp` in this case) by storing the name and the indices. The name is then resolved later when we have parsed the arguments. --- src/api/cpp/cvc5.cpp | 25 +--------- src/api/cpp/cvc5.h | 1 - src/api/cpp/cvc5_kind.h | 39 --------------- src/api/java/io/github/cvc5/api/Solver.java | 1 - src/parser/parse_op.cpp | 15 ++++++ src/parser/parse_op.h | 10 +++- src/parser/smt2/Smt2.g | 13 ++++- src/parser/smt2/smt2.cpp | 55 ++++++++++++++++++++- src/parser/smt2/smt2.h | 13 ++++- src/printer/smt2/smt2_printer.cpp | 9 ---- src/proof/lfsc/lfsc_node_converter.cpp | 15 +----- src/theory/fp/kinds | 16 ------ src/theory/fp/theory_fp.cpp | 7 +-- src/theory/fp/theory_fp_rewriter.cpp | 43 ---------------- src/theory/fp/theory_fp_type_rules.cpp | 39 --------------- src/theory/fp/theory_fp_type_rules.h | 7 --- src/util/floatingpoint.h | 14 ------ test/unit/api/cpp/op_black.cpp | 5 -- test/unit/api/java/OpTest.java | 5 -- test/unit/api/python/test_op.py | 5 -- 20 files changed, 106 insertions(+), 231 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index d92774743..95d3815d6 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -256,8 +256,6 @@ const static std::unordered_map> cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_SBV), KIND_ENUM(FLOATINGPOINT_TO_FP_FROM_UBV, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_UBV), - KIND_ENUM(FLOATINGPOINT_TO_FP_GENERIC, - cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC), KIND_ENUM(FLOATINGPOINT_TO_UBV, cvc5::Kind::FLOATINGPOINT_TO_UBV), KIND_ENUM(FLOATINGPOINT_TO_SBV, cvc5::Kind::FLOATINGPOINT_TO_SBV), KIND_ENUM(FLOATINGPOINT_TO_REAL, cvc5::Kind::FLOATINGPOINT_TO_REAL), @@ -563,9 +561,6 @@ const static std::unordered_map 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}, {cvc5::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV}, {cvc5::Kind::FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_UBV}, {cvc5::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, INTERNAL_KIND}, @@ -720,8 +715,7 @@ const static std::unordered_set s_indexed_kinds( FLOATINGPOINT_TO_FP_FROM_FP, FLOATINGPOINT_TO_FP_FROM_REAL, FLOATINGPOINT_TO_FP_FROM_SBV, - FLOATINGPOINT_TO_FP_FROM_UBV, - FLOATINGPOINT_TO_FP_GENERIC}); + FLOATINGPOINT_TO_FP_FROM_UBV}); namespace { @@ -1877,7 +1871,6 @@ size_t Op::getNumIndicesHelper() const 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: size = d_node->getConst().getIndices().size(); @@ -2022,15 +2015,6 @@ Term Op::getIndexHelper(size_t index) const : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); break; } - case FLOATINGPOINT_TO_FP_GENERIC: - { - cvc5::FloatingPointToFPGeneric ext = - d_node->getConst(); - t = index == 0 - ? d_solver->mkRationalValHelper(ext.getSize().exponentWidth()) - : d_solver->mkRationalValHelper(ext.getSize().significandWidth()); - break; - } case REGEXP_LOOP: { cvc5::RegExpLoop ext = d_node->getConst(); @@ -6286,13 +6270,6 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const cvc5::FloatingPointToFPUnsignedBitVector(arg1, arg2)) .d_node); break; - case FLOATINGPOINT_TO_FP_GENERIC: - res = Op(this, - kind, - *mkValHelper( - cvc5::FloatingPointToFPGeneric(arg1, arg2)) - .d_node); - break; case REGEXP_LOOP: res = Op( this, diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 5083bec38..6480a7b75 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3309,7 +3309,6 @@ class CVC5_EXPORT Solver * - 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 * @param arg1 the first uint32_t argument to this operator diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 3068f57d8..c9d10b297 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -1736,45 +1736,6 @@ enum Kind : int32_t * - `Solver::mkTerm(const Op& op, const std::vector& children) const` */ FLOATINGPOINT_TO_FP_FROM_UBV, - /** - * Operator for a generic to_fp. - * - * Parameters: - * - 1: exponent size - * - 2: Significand size - * - * Create with: - * - `Solver::mkOp(Kind kind, uint32_t param1, uint32_t param2) const` - * - * Generic conversion to floating-point, used in parsing only. - * - * Parameters: - * - * For conversion from IEEE bit-vector: - * - 1: Op of kind FLOATINGPOINT_TO_FP_GENERIC - * - 2: Term of bit-vector sort - * - * For conversion from floating-point: - * - 1: Op of kind FLOATINGPOINT_TO_FP_GENERIC - * - 2: Term of sort RoundingMode - * - 3: Term of floating-point sort - * - * For conversion from Real: - * - 1: Op of kind FLOATINGPOINT_TO_FP_GENERIC - * - 2: Term of sort RoundingMode - * - 3: Term of sort Real - * - * For conversion from (un)signed bit-vector: - * - 1: Op of kind FLOATINGPOINT_TO_FP_GENERIC - * - 2: Term of sort RoundingMode - * - 3: Term of bit-vector sort - * - * Create with: - * - `Solver::mkTerm(const Op& op, const Term& child) const` - * - `Solver::mkTerm(const Op& op, const Term& child1, const Term& child2) const` - * - `Solver::mkTerm(const Op& op, const std::vector& children) const` - */ - FLOATINGPOINT_TO_FP_GENERIC, /** * Operator for to_ubv. * diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 6fd3444eb..d0cc01232 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -737,7 +737,6 @@ public class Solver implements IPointer, AutoCloseable * - 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 * @param arg1 the first unsigned int argument to this operator diff --git a/src/parser/parse_op.cpp b/src/parser/parse_op.cpp index 772b73b1e..3471d9fb0 100644 --- a/src/parser/parse_op.cpp +++ b/src/parser/parse_op.cpp @@ -41,6 +41,21 @@ std::ostream& operator<<(std::ostream& os, const ParseOp& p) { out << " :name " << p.d_name; } + if (!p.d_indices.empty()) + { + out << " :indices ["; + bool first = true; + for (uint32_t index : p.d_indices) + { + if (!first) + { + out << ", "; + } + first = false; + out << index; + } + out << "]"; + } out << ")"; return os << out.str(); } diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h index 60e2bf6e2..1484c3e90 100644 --- a/src/parser/parse_op.h +++ b/src/parser/parse_op.h @@ -19,6 +19,7 @@ #define CVC5__PARSER__PARSE_OP_H #include +#include #include "api/cpp/cvc5.h" @@ -69,12 +70,19 @@ struct ParseOp api::Sort d_type; /** The operator associated with the parsed operator, if it exists */ api::Op d_op; + /** + * The indices if the operator is indexed, but api::Op is the null operator. + * This is the case for operator symbols that cannot be resolved to a kind + * without parsing the arguments. This is currently only the case for + * `to_fp`. + */ + std::vector d_indices; /* Return true if this is equal to 'p'. */ bool operator==(const ParseOp& p) const { return d_kind == p.d_kind && d_name == p.d_name && d_expr == p.d_expr - && d_type == p.d_type && d_op == p.d_op; + && d_type == p.d_type && d_op == p.d_op && d_indices == p.d_indices; } }; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 5985d4f8f..8edb39107 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1656,7 +1656,18 @@ identifier[cvc5::ParseOp& p] { std::string opName = AntlrInput::tokenText($sym); api::Kind k = PARSER_STATE->getIndexedOpKind(opName); - if (k == api::APPLY_SELECTOR || k == api::APPLY_UPDATER) + if (k == api::UNDEFINED_KIND) + { + // We don't know which kind to use until we know the type of the + // arguments + p.d_name = opName; + // convert uint64_t to uint32_t + for(uint32_t numeral : numerals) + { + p.d_indices.push_back(numeral); + } + } + else if (k == api::APPLY_SELECTOR || k == api::APPLY_UPDATER) { // we adopt a special syntax (_ tuple_select n) and (_ tuple_update n) // for tuple selectors and updaters diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index cb979d463..031210cab 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -229,7 +229,7 @@ void Smt2::addFloatingPointOperators() { addOperator(api::FLOATINGPOINT_IS_POS, "fp.isPositive"); addOperator(api::FLOATINGPOINT_TO_REAL, "fp.to_real"); - addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC, "to_fp"); + addIndexedOperator(api::UNDEFINED_KIND, "to_fp"); addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_UBV, "to_fp_unsigned"); addIndexedOperator(api::FLOATINGPOINT_TO_UBV, "fp.to_ubv"); addIndexedOperator(api::FLOATINGPOINT_TO_SBV, "fp.to_sbv"); @@ -286,6 +286,11 @@ void Smt2::addIndexedOperator(api::Kind tKind, d_indexedOpKindMap[name] = tKind; } +bool Smt2::isIndexedOperatorEnabled(const std::string& name) const +{ + return d_indexedOpKindMap.find(name) != d_indexedOpKindMap.end(); +} + api::Kind Smt2::getOperatorKind(const std::string& name) const { // precondition: isOperatorEnabled(name) @@ -922,6 +927,54 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) // it was given an operator op = p.d_op; } + else if (isIndexedOperatorEnabled(p.d_name)) + { + // Resolve indexed symbols that cannot be resolved without knowing the type + // of the arguments. This is currently limited to `to_fp`. + Assert(p.d_name == "to_fp"); + size_t nchildren = args.size(); + if (nchildren == 1) + { + op = d_solver->mkOp(api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV, + p.d_indices[0], + p.d_indices[1]); + } + else if (nchildren > 2) + { + std::stringstream ss; + ss << "Wrong number of arguments for indexed operator to_fp, expected " + "1 or 2, got " + << nchildren; + parseError(ss.str()); + } + else if (!args[0].getSort().isRoundingMode()) + { + std::stringstream ss; + ss << "Expected a rounding mode as the first argument, got " + << args[0].getSort(); + parseError(ss.str()); + } + else + { + api::Sort t = args[1].getSort(); + + if (t.isFloatingPoint()) + { + op = d_solver->mkOp( + api::FLOATINGPOINT_TO_FP_FROM_FP, p.d_indices[0], p.d_indices[1]); + } + else if (t.isInteger() || t.isReal()) + { + op = d_solver->mkOp( + api::FLOATINGPOINT_TO_FP_FROM_REAL, p.d_indices[0], p.d_indices[1]); + } + else + { + op = d_solver->mkOp( + api::FLOATINGPOINT_TO_FP_FROM_SBV, p.d_indices[0], p.d_indices[1]); + } + } + } else { isBuiltinOperator = isOperatorEnabled(p.d_name); diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index e53dc2048..a03384aba 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -83,11 +83,22 @@ class Smt2 : public Parser * Registers an indexed function symbol. * * @param tKind The kind of the term that uses the operator kind (e.g. - * BITVECTOR_EXTRACT). + * BITVECTOR_EXTRACT). If an indexed function symbol is + * overloaded (e.g., `to_fp`), this argument should + * be`UNDEFINED_KIND`. * @param name The name of the symbol (e.g. "extract") */ void addIndexedOperator(api::Kind tKind, const std::string& name); + /** + * Checks whether an indexed operator is enabled. All indexed operators in + * the current logic are considered to be enabled. This includes operators + * such as `to_fp`, which do not correspond to a single kind. + * + * @param name The name of the indexed operator. + * @return true if the indexed operator is enabled. + */ + bool isIndexedOperatorEnabled(const std::string& name) const; api::Kind getOperatorKind(const std::string& name) const; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index cd37cd049..c9125df3d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -435,13 +435,6 @@ void Smt2Printer::toStream(std::ostream& out, .significandWidth() << ")"; break; - case kind::FLOATINGPOINT_TO_FP_GENERIC_OP: - out << "(_ to_fp " - << n.getConst().getSize().exponentWidth() - << ' ' - << n.getConst().getSize().significandWidth() - << ")"; - break; case kind::FLOATINGPOINT_TO_UBV_OP: out << "(_ fp.to_ubv " << n.getConst().d_bv_size.d_size << ")"; @@ -760,7 +753,6 @@ void Smt2Printer::toStream(std::ostream& out, 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: out << n.getOperator() << ' '; @@ -1201,7 +1193,6 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) 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"; case kind::FLOATINGPOINT_TO_SBV: return "fp.to_sbv"; diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 506bb4440..047cc1f36 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -843,8 +843,7 @@ bool LfscNodeConverter::isIndexedOperatorKind(Kind k) || 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 == FLOATINGPOINT_TO_FP_FROM_REAL || k == APPLY_UPDATER || k == APPLY_TESTER; } @@ -926,14 +925,6 @@ std::vector LfscNodeConverter::getOperatorIndices(Kind k, Node n) indices.push_back(nm->mkConstInt(fr.getSize().significandWidth())); } break; - case FLOATINGPOINT_TO_FP_GENERIC: - { - const FloatingPointToFPGeneric& fg = - n.getConst(); - indices.push_back(nm->mkConstInt(fg.getSize().exponentWidth())); - indices.push_back(nm->mkConstInt(fg.getSize().significandWidth())); - } - break; case APPLY_TESTER: { unsigned index = DType::indexOf(n); @@ -1075,10 +1066,6 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply) { opName << "to_fp_real"; } - else if (k == FLOATINGPOINT_TO_FP_GENERIC) - { - opName << "to_fp_generic"; - } else { opName << printer::smt2::Smt2Printer::smtKindString(k); diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index 204459496..e059b30d6 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -224,22 +224,6 @@ typerule FLOATINGPOINT_TO_FP_FROM_UBV ::cvc5::theory::fp::FloatingPointToFPUns -constant FLOATINGPOINT_TO_FP_GENERIC_OP \ - class \ - FloatingPointToFPGeneric \ - "::cvc5::FloatingPointConvertSortHashFunction<0x11>" \ - "util/floatingpoint.h" \ - "operator for a generic to_fp" -typerule FLOATINGPOINT_TO_FP_GENERIC_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule - - -parameterized FLOATINGPOINT_TO_FP_GENERIC FLOATINGPOINT_TO_FP_GENERIC_OP 1:2 "a generic conversion to floating-point, used in parsing only" -typerule FLOATINGPOINT_TO_FP_GENERIC ::cvc5::theory::fp::FloatingPointToFPGenericTypeRule - - - - - constant FLOATINGPOINT_TO_UBV_OP \ class \ FloatingPointToUBV \ diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 2080b2db7..e112b32f7 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -127,8 +127,6 @@ void TheoryFp::finishInit() 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 // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_UBV); // Removed // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_SBV); // Removed @@ -481,9 +479,8 @@ void TheoryFp::registerTerm(TNode node) Trace("fp-registerTerm") << "TheoryFp::registerTerm(): " << node << std::endl; Kind k = node.getKind(); - Assert(k != kind::FLOATINGPOINT_TO_FP_GENERIC && k != kind::FLOATINGPOINT_SUB - && k != kind::FLOATINGPOINT_EQ && k != kind::FLOATINGPOINT_GEQ - && k != kind::FLOATINGPOINT_GT); + Assert(k != kind::FLOATINGPOINT_SUB && k != kind::FLOATINGPOINT_EQ + && k != kind::FLOATINGPOINT_GEQ && k != kind::FLOATINGPOINT_GT); // Add to the equality engine, always. This is required to ensure // getEqualityStatus works as expected when theory combination is enabled. diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index ff455ff31..6949a53fb 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -80,46 +80,6 @@ namespace rewrite { << ") found in expression?"; } - RewriteResponse removeToFPGeneric(TNode node, bool isPreRewrite) - { - Assert(!isPreRewrite); - Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC); - - FloatingPointToFPGeneric info = - node.getOperator().getConst(); - - uint32_t children = node.getNumChildren(); - - Node op; - NodeManager* nm = NodeManager::currentNM(); - - if (children == 1) - { - op = nm->mkConst(FloatingPointToFPIEEEBitVector(info)); - return RewriteResponse(REWRITE_AGAIN, nm->mkNode(op, node[0])); - } - Assert(children == 2); - Assert(node[0].getType().isRoundingMode()); - - TypeNode t = node[1].getType(); - - if (t.isFloatingPoint()) - { - op = nm->mkConst(FloatingPointToFPFloatingPoint(info)); - } - else if (t.isReal()) - { - op = nm->mkConst(FloatingPointToFPReal(info)); - } - else - { - Assert(t.isBitVector()); - op = nm->mkConst(FloatingPointToFPSignedBitVector(info)); - } - - return RewriteResponse(REWRITE_AGAIN, nm->mkNode(op, node[0], node[1])); - } - RewriteResponse removeDoubleNegation(TNode node, bool isPreRewrite) { Assert(node.getKind() == kind::FLOATINGPOINT_NEG); @@ -1179,7 +1139,6 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) 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; d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity; @@ -1268,8 +1227,6 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] = rewrite::toFPSignedBV; 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; d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity; d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity; diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp index 9a492b6c2..861829a4c 100644 --- a/src/theory/fp/theory_fp_type_rules.cpp +++ b/src/theory/fp/theory_fp_type_rules.cpp @@ -422,45 +422,6 @@ TypeNode FloatingPointToFPUnsignedBitVectorTypeRule::computeType( return nodeManager->mkFloatingPointType(info.getSize()); } -TypeNode FloatingPointToFPGenericTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) -{ - TRACE("FloatingPointToFPGenericTypeRule"); - - FloatingPointToFPGeneric info = - n.getOperator().getConst(); - - if (check) - { - uint32_t nchildren = n.getNumChildren(); - if (nchildren == 1) - { - if (!n[0].getType(check).isBitVector()) - { - throw TypeCheckingExceptionPrivate( - n, "first argument must be a bit-vector"); - } - } - else - { - Assert(nchildren == 2); - if (!n[0].getType(check).isRoundingMode()) - { - throw TypeCheckingExceptionPrivate( - n, "first argument must be a roundingmode"); - } - TypeNode tn = n[1].getType(check); - if (!tn.isBitVector() && !tn.isFloatingPoint() && !tn.isReal()) - { - throw TypeCheckingExceptionPrivate( - n, "second argument must be a bit-vector, floating-point or Real"); - } - } - } - return nodeManager->mkFloatingPointType(info.getSize()); -} - TypeNode FloatingPointToUBVTypeRule::computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h index 023d9dc17..a1723d89a 100644 --- a/src/theory/fp/theory_fp_type_rules.h +++ b/src/theory/fp/theory_fp_type_rules.h @@ -138,13 +138,6 @@ class FloatingPointToFPUnsignedBitVectorTypeRule static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); }; -/** Generic type rule for floating-point to_fp conversion. */ -class FloatingPointToFPGenericTypeRule -{ - public: - static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); -}; - /** Type rule for conversion from floating-point to unsigned bit-vector. */ class FloatingPointToUBVTypeRule { diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index def94d62a..2056f37ca 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -438,20 +438,6 @@ class FloatingPointToFPUnsignedBitVector : public FloatingPointConvertSort } }; -class FloatingPointToFPGeneric : public FloatingPointConvertSort -{ - public: - /** Constructors. */ - FloatingPointToFPGeneric(uint32_t _e, uint32_t _s) - : FloatingPointConvertSort(_e, _s) - { - } - FloatingPointToFPGeneric(const FloatingPointConvertSort& old) - : FloatingPointConvertSort(old) - { - } -}; - /** * Base type for floating-point to bit-vector conversion. */ diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp index 0dfe9cdb5..60137c56f 100644 --- a/test/unit/api/cpp/op_black.cpp +++ b/test/unit/api/cpp/op_black.cpp @@ -83,7 +83,6 @@ TEST_F(TestApiBlackOp, getNumIndices) Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6); Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8); Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10); - Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12); Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14); ASSERT_EQ(2, bvExtract.getNumIndices()); @@ -92,7 +91,6 @@ TEST_F(TestApiBlackOp, getNumIndices) ASSERT_EQ(2, toFpFromReal.getNumIndices()); ASSERT_EQ(2, toFpFromSbv.getNumIndices()); ASSERT_EQ(2, toFpFromUbv.getNumIndices()); - ASSERT_EQ(2, toFpGen.getNumIndices()); ASSERT_EQ(2, regexpLoop.getNumIndices()); // Operators with n indices @@ -138,7 +136,6 @@ TEST_F(TestApiBlackOp, subscriptOperator) Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6); Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8); Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10); - Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12); Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14); ASSERT_EQ(1, bvExtract[0].getUInt32Value()); @@ -153,8 +150,6 @@ TEST_F(TestApiBlackOp, subscriptOperator) ASSERT_EQ(8, toFpFromSbv[1].getUInt32Value()); ASSERT_EQ(11, toFpFromUbv[0].getUInt32Value()); ASSERT_EQ(10, toFpFromUbv[1].getUInt32Value()); - ASSERT_EQ(13, toFpGen[0].getUInt32Value()); - ASSERT_EQ(12, toFpGen[1].getUInt32Value()); ASSERT_EQ(15, regexpLoop[0].getUInt32Value()); ASSERT_EQ(14, regexpLoop[1].getUInt32Value()); diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java index 47793aa63..9f93c54b0 100644 --- a/test/unit/api/java/OpTest.java +++ b/test/unit/api/java/OpTest.java @@ -98,7 +98,6 @@ class OpTest Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6); Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8); Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10); - Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12); Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14); assertEquals(2, bvExtract.getNumIndices()); @@ -107,7 +106,6 @@ class OpTest assertEquals(2, toFpFromReal.getNumIndices()); assertEquals(2, toFpFromSbv.getNumIndices()); assertEquals(2, toFpFromUbv.getNumIndices()); - assertEquals(2, toFpGen.getNumIndices()); assertEquals(2, regexpLoop.getNumIndices()); // Operators with n indices @@ -153,7 +151,6 @@ class OpTest Op toFpFromReal = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 7, 6); Op toFpFromSbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 9, 8); Op toFpFromUbv = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 11, 10); - Op toFpGen = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 13, 12); Op regexpLoop = d_solver.mkOp(REGEXP_LOOP, 15, 14); assertEquals(1, bvExtract.get(0).getIntegerValue().intValue()); @@ -168,8 +165,6 @@ class OpTest assertEquals(8, toFpFromSbv.get(1).getIntegerValue().intValue()); assertEquals(11, toFpFromUbv.get(0).getIntegerValue().intValue()); assertEquals(10, toFpFromUbv.get(1).getIntegerValue().intValue()); - assertEquals(13, toFpGen.get(0).getIntegerValue().intValue()); - assertEquals(12, toFpGen.get(1).getIntegerValue().intValue()); assertEquals(15, regexpLoop.get(0).getIntegerValue().intValue()); assertEquals(14, regexpLoop.get(1).getIntegerValue().intValue()); diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py index 5a5d2ea86..2ce712689 100644 --- a/test/unit/api/python/test_op.py +++ b/test/unit/api/python/test_op.py @@ -82,7 +82,6 @@ def test_get_num_indices(solver): 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) assert 2 == bitvector_extract.getNumIndices() @@ -91,7 +90,6 @@ def test_get_num_indices(solver): 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() # Operators with n indices @@ -137,7 +135,6 @@ def test_subscript_operator(solver): floatingpoint_to_fp_from_real = solver.mkOp(Kind.FPToFpFromReal, 7, 6) floatingpoint_to_fp_from_sbv = solver.mkOp(Kind.FPToFpFromSbv, 9, 8) floatingpoint_to_fp_from_ubv = solver.mkOp(Kind.FPToFpFromUbv, 11, 10) - floatingpoint_to_fp_generic = solver.mkOp(Kind.FPToFpGeneric, 13, 12) regexp_loop = solver.mkOp(Kind.RegexpLoop, 15, 14) assert 1 == bitvector_extract[0].getIntegerValue() @@ -152,8 +149,6 @@ def test_subscript_operator(solver): assert 8 == floatingpoint_to_fp_from_sbv[1].getIntegerValue() assert 11 == floatingpoint_to_fp_from_ubv[0].getIntegerValue() assert 10 == floatingpoint_to_fp_from_ubv[1].getIntegerValue() - assert 13 == floatingpoint_to_fp_generic[0].getIntegerValue() - assert 12 == floatingpoint_to_fp_generic[1].getIntegerValue() assert 15 == regexp_loop[0].getIntegerValue() assert 14 == regexp_loop[1].getIntegerValue() -- 2.30.2