From c95d4c5473e8c26832fef89a9a42275517a42613 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 27 May 2021 12:08:24 -0700 Subject: [PATCH] FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628) This is to make it consistent with the name of the SMT-LIB operator (fp.add). --- examples/api/java/FloatingPointArith.java | 8 ++++---- examples/api/python/floating_point.py | 6 +++--- src/api/cpp/cvc5.cpp | 4 ++-- src/api/cpp/cvc5_kind.h | 2 +- src/parser/smt2/smt2.cpp | 2 +- src/printer/smt2/smt2_printer.cpp | 4 ++-- src/theory/fp/fp_converter.cpp | 4 ++-- src/theory/fp/kinds | 4 ++-- src/theory/fp/theory_fp.cpp | 2 +- src/theory/fp/theory_fp_rewriter.cpp | 20 +++++++++---------- .../quantifiers/sygus/sygus_grammar_cons.cpp | 2 +- src/util/floatingpoint.cpp | 4 ++-- src/util/floatingpoint.h | 2 +- 13 files changed, 32 insertions(+), 32 deletions(-) diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java index bf8d3a238..61ab18148 100644 --- a/examples/api/java/FloatingPointArith.java +++ b/examples/api/java/FloatingPointArith.java @@ -51,13 +51,13 @@ public class FloatingPointArith { // Assert that floating-point addition is not associative: // (a + (b + c)) != ((a + b) + c) Expr rm = em.mkConst(RoundingMode.roundNearestTiesToEven); - Expr lhs = em.mkExpr(Kind.FLOATINGPOINT_PLUS, + Expr lhs = em.mkExpr(Kind.FLOATINGPOINT_ADD, rm, a, - em.mkExpr(Kind.FLOATINGPOINT_PLUS, rm, b, c)); - Expr rhs = em.mkExpr(Kind.FLOATINGPOINT_PLUS, + em.mkExpr(Kind.FLOATINGPOINT_ADD, rm, b, c)); + Expr rhs = em.mkExpr(Kind.FLOATINGPOINT_ADD, rm, - em.mkExpr(Kind.FLOATINGPOINT_PLUS, rm, a, b), + em.mkExpr(Kind.FLOATINGPOINT_ADD, rm, a, b), c); smt.assertFormula(em.mkExpr(Kind.NOT, em.mkExpr(Kind.EQUAL, a, b))); diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py index 44a3d66d2..66b18642d 100644 --- a/examples/api/python/floating_point.py +++ b/examples/api/python/floating_point.py @@ -43,7 +43,7 @@ if __name__ == "__main__": z = slv.mkConst(fp32, 'z') # check floating-point arithmetic is commutative, i.e. x + y == y + x - commutative = slv.mkTerm(kinds.FPEq, slv.mkTerm(kinds.FPPlus, rm, x, y), slv.mkTerm(kinds.FPPlus, rm, y, x)) + commutative = slv.mkTerm(kinds.FPEq, slv.mkTerm(kinds.FPAdd, rm, x, y), slv.mkTerm(kinds.FPAdd, rm, y, x)) slv.push() slv.assertFormula(slv.mkTerm(kinds.Not, commutative)) @@ -76,8 +76,8 @@ if __name__ == "__main__": slv.assertFormula(slv.mkTerm(kinds.And, slv.mkTerm(kinds.And, bounds_x, bounds_y), bounds_z)) # (x + y) + z == x + (y + z) - lhs = slv.mkTerm(kinds.FPPlus, rm, slv.mkTerm(kinds.FPPlus, rm, x, y), z) - rhs = slv.mkTerm(kinds.FPPlus, rm, x, slv.mkTerm(kinds.FPPlus, rm, y, z)) + lhs = slv.mkTerm(kinds.FPAdd, rm, slv.mkTerm(kinds.FPAdd, rm, x, y), z) + rhs = slv.mkTerm(kinds.FPAdd, rm, x, slv.mkTerm(kinds.FPAdd, rm, y, z)) associative = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.FPEq, lhs, rhs)) slv.assertFormula(associative) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 436ac9856..16366c3cf 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -216,7 +216,7 @@ const static std::unordered_map s_kinds{ {FLOATINGPOINT_EQ, cvc5::Kind::FLOATINGPOINT_EQ}, {FLOATINGPOINT_ABS, cvc5::Kind::FLOATINGPOINT_ABS}, {FLOATINGPOINT_NEG, cvc5::Kind::FLOATINGPOINT_NEG}, - {FLOATINGPOINT_PLUS, cvc5::Kind::FLOATINGPOINT_PLUS}, + {FLOATINGPOINT_ADD, cvc5::Kind::FLOATINGPOINT_ADD}, {FLOATINGPOINT_SUB, cvc5::Kind::FLOATINGPOINT_SUB}, {FLOATINGPOINT_MULT, cvc5::Kind::FLOATINGPOINT_MULT}, {FLOATINGPOINT_DIV, cvc5::Kind::FLOATINGPOINT_DIV}, @@ -502,7 +502,7 @@ const static std::unordered_map {cvc5::Kind::FLOATINGPOINT_EQ, FLOATINGPOINT_EQ}, {cvc5::Kind::FLOATINGPOINT_ABS, FLOATINGPOINT_ABS}, {cvc5::Kind::FLOATINGPOINT_NEG, FLOATINGPOINT_NEG}, - {cvc5::Kind::FLOATINGPOINT_PLUS, FLOATINGPOINT_PLUS}, + {cvc5::Kind::FLOATINGPOINT_ADD, FLOATINGPOINT_ADD}, {cvc5::Kind::FLOATINGPOINT_SUB, FLOATINGPOINT_SUB}, {cvc5::Kind::FLOATINGPOINT_MULT, FLOATINGPOINT_MULT}, {cvc5::Kind::FLOATINGPOINT_DIV, FLOATINGPOINT_DIV}, diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 2805f6203..6f6bf1d0e 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -1428,7 +1428,7 @@ enum CVC5_EXPORT Kind : int32_t * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - FLOATINGPOINT_PLUS, + FLOATINGPOINT_ADD, /** * Floating-point sutraction. * diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index f3fd5697d..88f4b4ef8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -205,7 +205,7 @@ void Smt2::addFloatingPointOperators() { addOperator(api::FLOATINGPOINT_EQ, "fp.eq"); addOperator(api::FLOATINGPOINT_ABS, "fp.abs"); addOperator(api::FLOATINGPOINT_NEG, "fp.neg"); - addOperator(api::FLOATINGPOINT_PLUS, "fp.add"); + addOperator(api::FLOATINGPOINT_ADD, "fp.add"); addOperator(api::FLOATINGPOINT_SUB, "fp.sub"); addOperator(api::FLOATINGPOINT_MULT, "fp.mul"); addOperator(api::FLOATINGPOINT_DIV, "fp.div"); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 2163167a6..6258834c4 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -875,7 +875,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::FLOATINGPOINT_EQ: case kind::FLOATINGPOINT_ABS: case kind::FLOATINGPOINT_NEG: - case kind::FLOATINGPOINT_PLUS: + case kind::FLOATINGPOINT_ADD: case kind::FLOATINGPOINT_SUB: case kind::FLOATINGPOINT_MULT: case kind::FLOATINGPOINT_DIV: @@ -1253,7 +1253,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) case kind::FLOATINGPOINT_EQ: return "fp.eq"; case kind::FLOATINGPOINT_ABS: return "fp.abs"; case kind::FLOATINGPOINT_NEG: return "fp.neg"; - case kind::FLOATINGPOINT_PLUS: return "fp.add"; + case kind::FLOATINGPOINT_ADD: return "fp.add"; case kind::FLOATINGPOINT_SUB: return "fp.sub"; case kind::FLOATINGPOINT_MULT: return "fp.mul"; case kind::FLOATINGPOINT_DIV: return "fp.div"; diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp index c767014cb..0d1b25549 100644 --- a/src/theory/fp/fp_converter.cpp +++ b/src/theory/fp/fp_converter.cpp @@ -1102,7 +1102,7 @@ Node FpConverter::convert(TNode node) } break; - case kind::FLOATINGPOINT_PLUS: + case kind::FLOATINGPOINT_ADD: case kind::FLOATINGPOINT_SUB: case kind::FLOATINGPOINT_MULT: case kind::FLOATINGPOINT_DIV: @@ -1134,7 +1134,7 @@ Node FpConverter::convert(TNode node) switch (current.getKind()) { - case kind::FLOATINGPOINT_PLUS: + case kind::FLOATINGPOINT_ADD: d_fpMap.insert(current, symfpu::add(fpt(current.getType()), (*mode).second, diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds index c07e54463..fca5363fc 100644 --- a/src/theory/fp/kinds +++ b/src/theory/fp/kinds @@ -83,8 +83,8 @@ typerule FLOATINGPOINT_ABS ::cvc5::theory::fp::FloatingPointOperationTypeRule operator FLOATINGPOINT_NEG 1 "floating-point negation" typerule FLOATINGPOINT_NEG ::cvc5::theory::fp::FloatingPointOperationTypeRule -operator FLOATINGPOINT_PLUS 3 "floating-point addition" -typerule FLOATINGPOINT_PLUS ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule +operator FLOATINGPOINT_ADD 3 "floating-point addition" +typerule FLOATINGPOINT_ADD ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule operator FLOATINGPOINT_SUB 3 "floating-point sutraction" typerule FLOATINGPOINT_SUB ::cvc5::theory::fp::FloatingPointRoundingOperationTypeRule diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index a48f62c6d..3d81a2995 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -101,7 +101,7 @@ void TheoryFp::finishInit() d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ABS); d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_NEG); - d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_PLUS); + d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ADD); // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_SUB); // Removed d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_MULT); d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_DIV); diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp index c52100209..76f7d55cf 100644 --- a/src/theory/fp/theory_fp_rewriter.cpp +++ b/src/theory/fp/theory_fp_rewriter.cpp @@ -146,7 +146,8 @@ namespace rewrite { { Assert(node.getKind() == kind::FLOATINGPOINT_SUB); Node negation = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_NEG,node[2]); - Node addition = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_PLUS,node[0],node[1],negation); + Node addition = NodeManager::currentNM()->mkNode( + kind::FLOATINGPOINT_ADD, node[0], node[1], negation); return RewriteResponse(REWRITE_DONE, addition); } @@ -275,7 +276,7 @@ namespace rewrite { RewriteResponse reorderBinaryOperation (TNode node, bool isPreRewrite) { Kind k = node.getKind(); - Assert((k == kind::FLOATINGPOINT_PLUS) || (k == kind::FLOATINGPOINT_MULT)); + Assert((k == kind::FLOATINGPOINT_ADD) || (k == kind::FLOATINGPOINT_MULT)); Assert(!isPreRewrite); // Likely redundant in pre-rewrite if (node[1] > node[2]) { @@ -440,9 +441,9 @@ RewriteResponse neg(TNode node, bool isPreRewrite) node[0].getConst().negate())); } -RewriteResponse plus(TNode node, bool isPreRewrite) +RewriteResponse add(TNode node, bool isPreRewrite) { - Assert(node.getKind() == kind::FLOATINGPOINT_PLUS); + Assert(node.getKind() == kind::FLOATINGPOINT_ADD); Assert(node.getNumChildren() == 3); RoundingMode rm(node[0].getConst()); @@ -451,8 +452,8 @@ RewriteResponse plus(TNode node, bool isPreRewrite) Assert(arg1.getSize() == arg2.getSize()); - return RewriteResponse( - REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.plus(rm, arg2))); + return RewriteResponse(REWRITE_DONE, + NodeManager::currentNM()->mkConst(arg1.add(rm, arg2))); } RewriteResponse mult(TNode node, bool isPreRewrite) @@ -1143,7 +1144,7 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_preRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity; d_preRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs; d_preRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation; - d_preRewriteTable[kind::FLOATINGPOINT_PLUS] = rewrite::identity; + d_preRewriteTable[kind::FLOATINGPOINT_ADD] = rewrite::identity; d_preRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::convertSubtractionToAddition; d_preRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::identity; @@ -1234,8 +1235,7 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_postRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity; d_postRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs; d_postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation; - d_postRewriteTable[kind::FLOATINGPOINT_PLUS] = - rewrite::reorderBinaryOperation; + d_postRewriteTable[kind::FLOATINGPOINT_ADD] = rewrite::reorderBinaryOperation; d_postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::identity; d_postRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::reorderBinaryOperation; @@ -1326,7 +1326,7 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) d_constantFoldTable[kind::FLOATINGPOINT_FP] = constantFold::fpLiteral; d_constantFoldTable[kind::FLOATINGPOINT_ABS] = constantFold::abs; d_constantFoldTable[kind::FLOATINGPOINT_NEG] = constantFold::neg; - d_constantFoldTable[kind::FLOATINGPOINT_PLUS] = constantFold::plus; + d_constantFoldTable[kind::FLOATINGPOINT_ADD] = constantFold::add; d_constantFoldTable[kind::FLOATINGPOINT_MULT] = constantFold::mult; d_constantFoldTable[kind::FLOATINGPOINT_DIV] = constantFold::div; d_constantFoldTable[kind::FLOATINGPOINT_FMA] = constantFold::fma; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 1ed386485..7072b77e1 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -868,7 +868,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( } // ternary ops with RM std::vector ternary_rm_kinds = { - FLOATINGPOINT_PLUS, + FLOATINGPOINT_ADD, FLOATINGPOINT_SUB, FLOATINGPOINT_MULT, FLOATINGPOINT_DIV, diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index 0df9488c5..64ce22f9f 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -265,8 +265,8 @@ FloatingPoint FloatingPoint::negate(void) const return FloatingPoint(new FloatingPointLiteral(d_fpl->negate())); } -FloatingPoint FloatingPoint::plus(const RoundingMode& rm, - const FloatingPoint& arg) const +FloatingPoint FloatingPoint::add(const RoundingMode& rm, + const FloatingPoint& arg) const { return FloatingPoint(new FloatingPointLiteral(d_fpl->add(rm, *arg.d_fpl))); } diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index b7ec46e60..fb2c3f29f 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -155,7 +155,7 @@ class FloatingPoint /** Floating-point negation. */ FloatingPoint negate(void) const; /** Floating-point addition. */ - FloatingPoint plus(const RoundingMode& rm, const FloatingPoint& arg) const; + FloatingPoint add(const RoundingMode& rm, const FloatingPoint& arg) const; /** Floating-point subtraction. */ FloatingPoint sub(const RoundingMode& rm, const FloatingPoint& arg) const; /** Floating-point multiplication. */ -- 2.30.2