From: Aina Niemetz Date: Fri, 20 Nov 2020 23:11:39 +0000 (-0800) Subject: RoundingMode: Rename enum values to conform to code style guidelines. (#5494) X-Git-Tag: cvc5-1.0.0~2567 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a02b2e28ee8d0560c923eaf0073c2fdce8fbfa2;p=cvc5.git RoundingMode: Rename enum values to conform to code style guidelines. (#5494) --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 16ec0935c..9b79b5c45 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -3060,24 +3060,24 @@ const static std:: unordered_map s_rmodes{ {ROUND_NEAREST_TIES_TO_EVEN, - CVC4::RoundingMode::roundNearestTiesToEven}, - {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::roundTowardPositive}, - {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::roundTowardNegative}, - {ROUND_TOWARD_ZERO, CVC4::RoundingMode::roundTowardZero}, + CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN}, + {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::ROUND_TOWARD_POSITIVE}, + {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::ROUND_TOWARD_POSITIVE}, + {ROUND_TOWARD_ZERO, CVC4::RoundingMode::ROUND_TOWARD_ZERO}, {ROUND_NEAREST_TIES_TO_AWAY, - CVC4::RoundingMode::roundNearestTiesToAway}, + CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY}, }; const static std::unordered_map s_rmodes_internal{ - {CVC4::RoundingMode::roundNearestTiesToEven, + {CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN, ROUND_NEAREST_TIES_TO_EVEN}, - {CVC4::RoundingMode::roundTowardPositive, ROUND_TOWARD_POSITIVE}, - {CVC4::RoundingMode::roundTowardNegative, ROUND_TOWARD_NEGATIVE}, - {CVC4::RoundingMode::roundTowardZero, ROUND_TOWARD_ZERO}, - {CVC4::RoundingMode::roundNearestTiesToAway, + {CVC4::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_POSITIVE}, + {CVC4::RoundingMode::ROUND_TOWARD_POSITIVE, ROUND_TOWARD_NEGATIVE}, + {CVC4::RoundingMode::ROUND_TOWARD_ZERO, ROUND_TOWARD_ZERO}, + {CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY, ROUND_NEAREST_TIES_TO_AWAY}, }; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 03b04469c..747873bee 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -209,14 +209,14 @@ void Smt2Printer::toStream(std::ostream& out, } case kind::CONST_ROUNDINGMODE: switch (n.getConst()) { - case roundNearestTiesToEven : out << "roundNearestTiesToEven"; break; - case roundNearestTiesToAway : out << "roundNearestTiesToAway"; break; - case roundTowardPositive : out << "roundTowardPositive"; break; - case roundTowardNegative : out << "roundTowardNegative"; break; - case roundTowardZero : out << "roundTowardZero"; break; - default : - Unreachable() << "Invalid value of rounding mode constant (" - << n.getConst() << ")"; + case ROUND_NEAREST_TIES_TO_EVEN: out << "roundNearestTiesToEven"; break; + case ROUND_NEAREST_TIES_TO_AWAY: out << "roundNearestTiesToAway"; break; + case ROUND_TOWARD_POSITIVE: out << "roundTowardPositive"; break; + case ROUND_TOWARD_NEGATIVE: out << "roundTowardNegative"; break; + case ROUND_TOWARD_ZERO: out << "roundTowardZero"; break; + default: + Unreachable() << "Invalid value of rounding mode constant (" + << n.getConst() << ")"; } break; case kind::CONST_BOOLEAN: diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index f7c58af7b..b8e6f381c 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -799,17 +799,17 @@ Node FpConverter::rmToNode(const rm &r) const Node value = nm->mkNode( kind::ITE, nm->mkNode(kind::EQUAL, transVar, RNE), - nm->mkConst(roundNearestTiesToEven), + nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN), nm->mkNode(kind::ITE, nm->mkNode(kind::EQUAL, transVar, RNA), - nm->mkConst(roundNearestTiesToAway), + nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY), nm->mkNode(kind::ITE, nm->mkNode(kind::EQUAL, transVar, RTP), - nm->mkConst(roundTowardPositive), + nm->mkConst(ROUND_TOWARD_POSITIVE), nm->mkNode(kind::ITE, nm->mkNode(kind::EQUAL, transVar, RTN), - nm->mkConst(roundTowardNegative), - nm->mkConst(roundTowardZero))))); + nm->mkConst(ROUND_TOWARD_NEGATIVE), + nm->mkConst(ROUND_TOWARD_ZERO))))); return value; } @@ -877,19 +877,19 @@ Node FpConverter::convert(TNode node) /******** Constants ********/ switch (current.getConst()) { - case roundNearestTiesToEven: + case ROUND_NEAREST_TIES_TO_EVEN: d_rmMap.insert(current, traits::RNE()); break; - case roundNearestTiesToAway: + case ROUND_NEAREST_TIES_TO_AWAY: d_rmMap.insert(current, traits::RNA()); break; - case roundTowardPositive: + case ROUND_TOWARD_POSITIVE: d_rmMap.insert(current, traits::RTP()); break; - case roundTowardNegative: + case ROUND_TOWARD_NEGATIVE: d_rmMap.insert(current, traits::RTN()); break; - case roundTowardZero: + case ROUND_TOWARD_ZERO: d_rmMap.insert(current, traits::RTZ()); break; default: Unreachable() << "Unknown rounding mode"; break; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 037b083f4..0b15486e2 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -589,7 +589,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst())), - nm->mkConst(roundTowardPositive), + nm->mkConst(ROUND_TOWARD_POSITIVE), abstractValue)); Node bg = nm->mkNode( @@ -606,7 +606,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete) nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL, nm->mkConst(FloatingPointToFPReal( concrete[0].getType().getConst())), - nm->mkConst(roundTowardNegative), + nm->mkConst(ROUND_TOWARD_NEGATIVE), abstractValue)); Node bl = nm->mkNode( diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index b56fa259c..78aba415b 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -946,23 +946,23 @@ namespace constantFold { RoundingMode arg0(node[0].getConst()); switch (arg0) { - case roundNearestTiesToEven: + case ROUND_NEAREST_TIES_TO_EVEN: value = symfpuSymbolic::traits::RNE().getConst(); break; - case roundNearestTiesToAway: + case ROUND_NEAREST_TIES_TO_AWAY: value = symfpuSymbolic::traits::RNA().getConst(); break; - case roundTowardPositive: + case ROUND_TOWARD_POSITIVE: value = symfpuSymbolic::traits::RTP().getConst(); break; - case roundTowardNegative: + case ROUND_TOWARD_NEGATIVE: value = symfpuSymbolic::traits::RTN().getConst(); break; - case roundTowardZero: + case ROUND_TOWARD_ZERO: value = symfpuSymbolic::traits::RTZ().getConst(); break; @@ -1343,58 +1343,65 @@ TheoryFpRewriter::TheoryFpRewriter() } } - if (allChildrenConst) { - RewriteStatus rs = REWRITE_DONE; // This is a bit messy because - Node rn = res.d_node; // RewriteResponse is too functional.. + if (allChildrenConst) + { + RewriteStatus rs = REWRITE_DONE; // This is a bit messy because + Node rn = res.d_node; // RewriteResponse is too functional.. - if (apartFromRoundingMode) { + if (apartFromRoundingMode) + { if (!(res.d_node.getKind() == kind::EQUAL) && // Avoid infinite recursion... !(res.d_node.getKind() == kind::ROUNDINGMODE_BITBLAST)) - { // Don't eliminate the bit-blast + { + // Don't eliminate the bit-blast // We are close to being able to constant fold this // and in many cases the rounding mode really doesn't matter. // So we can try brute forcing our way through them. - NodeManager *nm = NodeManager::currentNM(); + NodeManager* nm = NodeManager::currentNM(); - Node RNE(nm->mkConst(roundNearestTiesToEven)); - Node RNA(nm->mkConst(roundNearestTiesToAway)); - Node RTZ(nm->mkConst(roundTowardPositive)); - Node RTN(nm->mkConst(roundTowardNegative)); - Node RTP(nm->mkConst(roundTowardZero)); + Node rne(nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN)); + Node rna(nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY)); + Node rtz(nm->mkConst(ROUND_TOWARD_POSITIVE)); + Node rtn(nm->mkConst(ROUND_TOWARD_NEGATIVE)); + Node rtp(nm->mkConst(ROUND_TOWARD_ZERO)); - TNode RM(res.d_node[0]); + TNode rm(res.d_node[0]); - Node wRNE(res.d_node.substitute(RM, TNode(RNE))); - Node wRNA(res.d_node.substitute(RM, TNode(RNA))); - Node wRTZ(res.d_node.substitute(RM, TNode(RTZ))); - Node wRTN(res.d_node.substitute(RM, TNode(RTN))); - Node wRTP(res.d_node.substitute(RM, TNode(RTP))); + Node w_rne(res.d_node.substitute(rm, TNode(rne))); + Node w_rna(res.d_node.substitute(rm, TNode(rna))); + Node w_rtz(res.d_node.substitute(rm, TNode(rtz))); + Node w_rtn(res.d_node.substitute(rm, TNode(rtn))); + Node w_rtp(res.d_node.substitute(rm, TNode(rtp))); rs = REWRITE_AGAIN_FULL; - rn = nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, RM, RNE), - wRNE, - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, RM, RNA), - wRNA, - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, RM, RTZ), - wRTZ, - nm->mkNode(kind::ITE, - nm->mkNode(kind::EQUAL, RM, RTN), - wRTN, - wRTP)))); - } - } else { + rn = nm->mkNode( + kind::ITE, + nm->mkNode(kind::EQUAL, rm, rne), + w_rne, + nm->mkNode( + kind::ITE, + nm->mkNode(kind::EQUAL, rm, rna), + w_rna, + nm->mkNode(kind::ITE, + nm->mkNode(kind::EQUAL, rm, rtz), + w_rtz, + nm->mkNode(kind::ITE, + nm->mkNode(kind::EQUAL, rm, rtn), + w_rtn, + w_rtp)))); + } + } + else + { RewriteResponse tmp = d_constantFoldTable[res.d_node.getKind()](res.d_node, false); rs = tmp.d_status; rn = tmp.d_node; } - RewriteResponse constRes(rs,rn); + RewriteResponse constRes(rs, rn); if (constRes.d_node != res.d_node) { diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h index 59f643b95..47266eda8 100644 --- a/src/theory/fp/type_enumerator.h +++ b/src/theory/fp/type_enumerator.h @@ -86,8 +86,10 @@ class RoundingModeEnumerator public: RoundingModeEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) : TypeEnumeratorBase(type), - d_rm(roundNearestTiesToEven), - d_enumerationComplete(false) {} + d_rm(ROUND_NEAREST_TIES_TO_EVEN), + d_enumerationComplete(false) + { + } /** Throws NoMoreValuesException if the enumeration is complete. */ Node operator*() override { @@ -99,21 +101,11 @@ class RoundingModeEnumerator RoundingModeEnumerator& operator++() override { switch (d_rm) { - case roundNearestTiesToEven: - d_rm = roundTowardPositive; - break; - case roundTowardPositive: - d_rm = roundTowardNegative; - break; - case roundTowardNegative: - d_rm = roundTowardZero; - break; - case roundTowardZero: - d_rm = roundNearestTiesToAway; - break; - case roundNearestTiesToAway: - d_enumerationComplete = true; - break; + case ROUND_NEAREST_TIES_TO_EVEN: d_rm = ROUND_TOWARD_POSITIVE; break; + case ROUND_TOWARD_POSITIVE: d_rm = ROUND_TOWARD_NEGATIVE; break; + case ROUND_TOWARD_NEGATIVE: d_rm = ROUND_TOWARD_ZERO; break; + case ROUND_TOWARD_ZERO: d_rm = ROUND_NEAREST_TIES_TO_AWAY; break; + case ROUND_NEAREST_TIES_TO_AWAY: d_enumerationComplete = true; break; default: Unreachable() << "Unknown rounding mode?"; break; } return *this; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index e5cc5460d..79fc1a36e 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -423,11 +423,11 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, } else if (type.isRoundingMode()) { - ops.push_back(nm->mkConst(RoundingMode::roundNearestTiesToAway)); - ops.push_back(nm->mkConst(RoundingMode::roundNearestTiesToEven)); - ops.push_back(nm->mkConst(RoundingMode::roundTowardNegative)); - ops.push_back(nm->mkConst(RoundingMode::roundTowardPositive)); - ops.push_back(nm->mkConst(RoundingMode::roundTowardZero)); + ops.push_back(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY)); + ops.push_back(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN)); + ops.push_back(nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE)); + ops.push_back(nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE)); + ops.push_back(nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO)); } else if (type.isFloatingPoint()) { diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h index 245654a53..a1bda2988 100644 --- a/src/util/roundingmode.h +++ b/src/util/roundingmode.h @@ -27,13 +27,14 @@ namespace CVC4 { */ enum CVC4_PUBLIC RoundingMode { - roundNearestTiesToEven = FE_TONEAREST, - roundTowardPositive = FE_UPWARD, - roundTowardNegative = FE_DOWNWARD, - roundTowardZero = FE_TOWARDZERO, + ROUND_NEAREST_TIES_TO_EVEN = FE_TONEAREST, + ROUND_TOWARD_POSITIVE = FE_UPWARD, + ROUND_TOWARD_NEGATIVE = FE_DOWNWARD, + ROUND_TOWARD_ZERO = FE_TOWARDZERO, // Initializes this to the diagonalization of the 4 other values. - roundNearestTiesToAway = (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2) - | ((~FE_DOWNWARD) & 0x4) | ((~FE_TOWARDZERO) & 0x8)) + ROUND_NEAREST_TIES_TO_AWAY = + (((~FE_TONEAREST) & 0x1) | ((~FE_UPWARD) & 0x2) | ((~FE_DOWNWARD) & 0x4) + | ((~FE_TOWARDZERO) & 0x8)) }; /* enum RoundingMode */ /** diff --git a/src/util/symfpu_literal.cpp b/src/util/symfpu_literal.cpp index 46d3cbe40..b916d62f9 100644 --- a/src/util/symfpu_literal.cpp +++ b/src/util/symfpu_literal.cpp @@ -400,11 +400,11 @@ wrappedBitVector wrappedBitVector::extract( template class wrappedBitVector; template class wrappedBitVector; -traits::rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; }; -traits::rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; }; -traits::rm traits::RTP(void) { return ::CVC4::roundTowardPositive; }; -traits::rm traits::RTN(void) { return ::CVC4::roundTowardNegative; }; -traits::rm traits::RTZ(void) { return ::CVC4::roundTowardZero; }; +traits::rm traits::RNE(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_EVEN; }; +traits::rm traits::RNA(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_AWAY; }; +traits::rm traits::RTP(void) { return ::CVC4::ROUND_TOWARD_POSITIVE; }; +traits::rm traits::RTN(void) { return ::CVC4::ROUND_TOWARD_NEGATIVE; }; +traits::rm traits::RTZ(void) { return ::CVC4::ROUND_TOWARD_ZERO; }; // This is a literal back-end so props are actually bools // so these can be handled in the same way as the internal assertions above