FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)

This is to make it consistent with the name of the SMT-LIB operator
(fp.add).

diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java
index bf8d3a2388627f25ded007d0a6a78a7f6181782f..61ab18148b8c5080aac019128fb9ba5637a4780f 100644 (file)
--- 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 44a3d66d26e54fce964f1da77adad11abaaa7e19..66b18642d085f937c984e0096fed07f2b2e3ed96 100644 (file)
--- 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 436ac985674297253d2022ab805bac65bc942490..16366c3cfee9bbf51c479085f8e1c815bd883390 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -216,7 +216,7 @@ const static std::unordered_map<Kind, cvc5::Kind> 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, Kind, cvc5::kind::KindHashFunction>
         {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 2805f6203ceb0b37d2fa70afa1bd25e05f17d7f2..6f6bf1d0ee37bee94227b8f18879f2e616d3f9c0 100644 (file)
--- 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<Term>& children) const`
    */
-  FLOATINGPOINT_PLUS,
+  FLOATINGPOINT_ADD,
   /**
    * Floating-point sutraction.
    *

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index f3fd5697d854c530d0ae12f7d59afdf5162d8361..88f4b4ef8739e3d4b984f27b453a303f7ab65332 100644 (file)
--- 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 2163167a6c867547634a7ea8c8dc4ec0ee0937a7..6258834c43b09aa929070bdeebbe7a606ce60bd0 100644 (file)
--- 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 c767014cb3df16420609719609c8e1db0061e5bb..0d1b25549eb97ee73bcbb622a649bda92b112e7e 100644 (file)
--- 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<traits>(fpt(current.getType()),
                                                      (*mode).second,

diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds
index c07e54463697b3fe493faeae7b8d651d33e0caaa..fca5363fc9a5c3f7c67bc95ad32d1a753a0f50de 100644 (file)
--- 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 a48f62c6d71a0a47ef970c49a24d1dedf6288f17..3d81a2995340dfe8b2e2632dbadc9e8b82c81cd8 100644 (file)
--- 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 c521002097ea08ddb5f106cb392fca2f0bfc6e35..76f7d55cf9676d52da0202eb2b4e02ea5bcc8746 100644 (file)
--- 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<FloatingPoint>().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<RoundingMode>());
@@ -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 1ed3864858fd1812fe5a6dfd0dd7c868fb60afaf..7072b77e1e711f3fab8fd67f820c75da5704b8a3 100644 (file)
--- 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<Kind> 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 0df9488c508687744e437bfc65d09404fec468ac..64ce22f9f7260ccbb500aa7fb1e28ee5449bae5f 100644 (file)
--- 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 b7ec46e6061d73d6d9d22d3c7ecae54204b1d454..fb2c3f29f2079d52d19b0a16c98b225713421c13 100644 (file)
--- 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. */