FP: Rename tester kinds. (#8037)

This renames FP tester kinds for consistency:
FLOATINGPOINT_ISINF -> FLOATINGPOINT_IS_INF
FLOATINGPOINT_ISN -> FLOATINGPOINT_IS_NORMAL
FLOATINGPOINT_ISNAN -> FLOATINGPOINT_IS_NAN
FLOATINGPOINT_ISNEG -> FLOATINGPOINT_IS_NEG
FLOATINGPOINT_ISPOS -> FLOATINGPOINT_IS_POS
FLOATINGPOINT_ISZ -> FLOATINGPOINT_IS_ZERO

diff --git a/examples/api/cpp/floating_point_arith.cpp b/examples/api/cpp/floating_point_arith.cpp
index 1448f7d1f77e5a1dfe817251fcf35922dfcbfa7e..4e44965d1e45476d94fea4c6efb017800f27da73 100644 (file)
--- a/examples/api/cpp/floating_point_arith.cpp
+++ b/examples/api/cpp/floating_point_arith.cpp
@@ -76,7 +76,7 @@ int main()
   Op op = solver.mkOp(FLOATINGPOINT_TO_SBV, 16);  // (_ fp.to_sbv 16)
   lhs = solver.mkTerm(op, rtp, d);
   rhs = solver.mkTerm(op, rtn, d);
-  solver.assertFormula(solver.mkTerm(FLOATINGPOINT_ISN, d));
+  solver.assertFormula(solver.mkTerm(FLOATINGPOINT_IS_NORMAL, d));
   solver.assertFormula(solver.mkTerm(NOT, solver.mkTerm(EQUAL, lhs, rhs)));
 
   r = solver.checkSat();  // result is sat

diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java
index 7f601eee8148f4f9edab90347a1ea6c34f67695b..92b03ec6cb5a068a98bba1e25aa8c59b017d40fd 100644 (file)
--- a/examples/api/java/FloatingPointArith.java
+++ b/examples/api/java/FloatingPointArith.java
@@ -75,7 +75,7 @@ public class FloatingPointArith
       Op op = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 16); // (_ fp.to_sbv 16)
       lhs = solver.mkTerm(op, rtp, d);
       rhs = solver.mkTerm(op, rtn, d);
-      solver.assertFormula(solver.mkTerm(Kind.FLOATINGPOINT_ISN, d));
+      solver.assertFormula(solver.mkTerm(Kind.FLOATINGPOINT_IS_NORMAL, d));
       solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, lhs, rhs)));
 
       r = solver.checkSat(); // result is sat

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 54174aec4c7738276c6da7096c7c6c1a5e0e733f..b246b7547bed19ff1bc2757baf44ed1a3a6e3b69 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -230,13 +230,13 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     {FLOATINGPOINT_LT, cvc5::Kind::FLOATINGPOINT_LT},
     {FLOATINGPOINT_GEQ, cvc5::Kind::FLOATINGPOINT_GEQ},
     {FLOATINGPOINT_GT, cvc5::Kind::FLOATINGPOINT_GT},
-    {FLOATINGPOINT_ISN, cvc5::Kind::FLOATINGPOINT_ISN},
-    {FLOATINGPOINT_ISSN, cvc5::Kind::FLOATINGPOINT_ISSN},
-    {FLOATINGPOINT_ISZ, cvc5::Kind::FLOATINGPOINT_ISZ},
-    {FLOATINGPOINT_ISINF, cvc5::Kind::FLOATINGPOINT_ISINF},
-    {FLOATINGPOINT_ISNAN, cvc5::Kind::FLOATINGPOINT_ISNAN},
-    {FLOATINGPOINT_ISNEG, cvc5::Kind::FLOATINGPOINT_ISNEG},
-    {FLOATINGPOINT_ISPOS, cvc5::Kind::FLOATINGPOINT_ISPOS},
+    {FLOATINGPOINT_IS_NORMAL, cvc5::Kind::FLOATINGPOINT_IS_NORMAL},
+    {FLOATINGPOINT_IS_SUBNORMAL, cvc5::Kind::FLOATINGPOINT_IS_SUBNORMAL},
+    {FLOATINGPOINT_IS_ZERO, cvc5::Kind::FLOATINGPOINT_IS_ZERO},
+    {FLOATINGPOINT_IS_INF, cvc5::Kind::FLOATINGPOINT_IS_INF},
+    {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,
@@ -525,13 +525,13 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         {cvc5::Kind::FLOATINGPOINT_LT, FLOATINGPOINT_LT},
         {cvc5::Kind::FLOATINGPOINT_GEQ, FLOATINGPOINT_GEQ},
         {cvc5::Kind::FLOATINGPOINT_GT, FLOATINGPOINT_GT},
-        {cvc5::Kind::FLOATINGPOINT_ISN, FLOATINGPOINT_ISN},
-        {cvc5::Kind::FLOATINGPOINT_ISSN, FLOATINGPOINT_ISSN},
-        {cvc5::Kind::FLOATINGPOINT_ISZ, FLOATINGPOINT_ISZ},
-        {cvc5::Kind::FLOATINGPOINT_ISINF, FLOATINGPOINT_ISINF},
-        {cvc5::Kind::FLOATINGPOINT_ISNAN, FLOATINGPOINT_ISNAN},
-        {cvc5::Kind::FLOATINGPOINT_ISNEG, FLOATINGPOINT_ISNEG},
-        {cvc5::Kind::FLOATINGPOINT_ISPOS, FLOATINGPOINT_ISPOS},
+        {cvc5::Kind::FLOATINGPOINT_IS_NORMAL, FLOATINGPOINT_IS_NORMAL},
+        {cvc5::Kind::FLOATINGPOINT_IS_SUBNORMAL, FLOATINGPOINT_IS_SUBNORMAL},
+        {cvc5::Kind::FLOATINGPOINT_IS_ZERO, FLOATINGPOINT_IS_ZERO},
+        {cvc5::Kind::FLOATINGPOINT_IS_INF, FLOATINGPOINT_IS_INF},
+        {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,

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 112b53eb7124e82ae9a69b232a00bafe4aea7fa5..e97adf53b32e66d302a374314598cfdf8082e40e 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -1569,7 +1569,7 @@ enum Kind : int32_t
    * Create with:
    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
    */
-  FLOATINGPOINT_ISN,
+  FLOATINGPOINT_IS_NORMAL,
   /**
    * Floating-point is sub-normal.
    *
@@ -1579,7 +1579,7 @@ enum Kind : int32_t
    * Create with:
    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
    */
-  FLOATINGPOINT_ISSN,
+  FLOATINGPOINT_IS_SUBNORMAL,
   /**
    * Floating-point is zero.
    *
@@ -1589,7 +1589,7 @@ enum Kind : int32_t
    * Create with:
    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
    */
-  FLOATINGPOINT_ISZ,
+  FLOATINGPOINT_IS_ZERO,
   /**
    * Floating-point is infinite.
    *
@@ -1599,7 +1599,7 @@ enum Kind : int32_t
    * Create with:
    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
    */
-  FLOATINGPOINT_ISINF,
+  FLOATINGPOINT_IS_INF,
   /**
    * Floating-point is NaN.
    *
@@ -1609,7 +1609,7 @@ enum Kind : int32_t
    * Create with:
    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
    */
-  FLOATINGPOINT_ISNAN,
+  FLOATINGPOINT_IS_NAN,
   /**
    * Floating-point is negative.
    *
@@ -1619,7 +1619,7 @@ enum Kind : int32_t
    * Create with:
    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
    */
-  FLOATINGPOINT_ISNEG,
+  FLOATINGPOINT_IS_NEG,
   /**
    * Floating-point is positive.
    *
@@ -1629,7 +1629,7 @@ enum Kind : int32_t
    * Create with:
    *   - `Solver::mkTerm(Kind kind, const Term& child) const`
    */
-  FLOATINGPOINT_ISPOS,
+  FLOATINGPOINT_IS_POS,
   /**
    * Operator for to_fp from bit vector.
    *

diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py
index db72b20c9be8f771c9d8c6fdb0e8c17905031f71..84d154f36a7320539d6d27657fe447246a1bf0b0 100644 (file)
--- a/src/api/parsekinds.py
+++ b/src/api/parsekinds.py
@@ -96,7 +96,7 @@ class KindsParser:
            4. replace Bitvector with BV
 
         There is one exception:
-           FLOATINGPOINT_ISNAN  --> FPIsNan
+           FLOATINGPOINT_IS_NAN  --> FPIsNan
 
         For every "_IS" in the name, there's an underscore added before step 1,
            so that the word after "Is" is capitalized
@@ -104,7 +104,7 @@ class KindsParser:
         Examples:
            BITVECTOR_ADD       -->  BVAdd
            APPLY_SELECTOR      -->  ApplySelector
-           FLOATINGPOINT_ISNAN -->  FPIsNan
+           FLOATINGPOINT_IS_NAN -->  FPIsNan
            SET_MINUS            -->  Setminus
 
         See the generated .pxi file for an explicit mapping

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 3352bde1ba065dbec770db29abf950cb16eeca09..0f0e3060c6a0c4fa640a65eda03a9aa4394d23de 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -225,13 +225,13 @@ void Smt2::addFloatingPointOperators() {
   addOperator(api::FLOATINGPOINT_LT, "fp.lt");
   addOperator(api::FLOATINGPOINT_GEQ, "fp.geq");
   addOperator(api::FLOATINGPOINT_GT, "fp.gt");
-  addOperator(api::FLOATINGPOINT_ISN, "fp.isNormal");
-  addOperator(api::FLOATINGPOINT_ISSN, "fp.isSubnormal");
-  addOperator(api::FLOATINGPOINT_ISZ, "fp.isZero");
-  addOperator(api::FLOATINGPOINT_ISINF, "fp.isInfinite");
-  addOperator(api::FLOATINGPOINT_ISNAN, "fp.isNaN");
-  addOperator(api::FLOATINGPOINT_ISNEG, "fp.isNegative");
-  addOperator(api::FLOATINGPOINT_ISPOS, "fp.isPositive");
+  addOperator(api::FLOATINGPOINT_IS_NORMAL, "fp.isNormal");
+  addOperator(api::FLOATINGPOINT_IS_SUBNORMAL, "fp.isSubnormal");
+  addOperator(api::FLOATINGPOINT_IS_ZERO, "fp.isZero");
+  addOperator(api::FLOATINGPOINT_IS_INF, "fp.isInfinite");
+  addOperator(api::FLOATINGPOINT_IS_NAN, "fp.isNaN");
+  addOperator(api::FLOATINGPOINT_IS_NEG, "fp.isNegative");
+  addOperator(api::FLOATINGPOINT_IS_POS, "fp.isPositive");
   addOperator(api::FLOATINGPOINT_TO_REAL, "fp.to_real");
 
   addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC,

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 420c176f71a26a02842d0f19afbebcae5911279e..05252b2913116add913d75e3d8fcb62ab0193f55 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1150,13 +1150,13 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   case kind::FLOATINGPOINT_GEQ: return "fp.geq";
   case kind::FLOATINGPOINT_GT: return "fp.gt";
 
-  case kind::FLOATINGPOINT_ISN: return "fp.isNormal";
-  case kind::FLOATINGPOINT_ISSN: return "fp.isSubnormal";
-  case kind::FLOATINGPOINT_ISZ: return "fp.isZero";
-  case kind::FLOATINGPOINT_ISINF: return "fp.isInfinite";
-  case kind::FLOATINGPOINT_ISNAN: return "fp.isNaN";
-  case kind::FLOATINGPOINT_ISNEG: return "fp.isNegative";
-  case kind::FLOATINGPOINT_ISPOS: return "fp.isPositive";
+  case kind::FLOATINGPOINT_IS_NORMAL: return "fp.isNormal";
+  case kind::FLOATINGPOINT_IS_SUBNORMAL: return "fp.isSubnormal";
+  case kind::FLOATINGPOINT_IS_ZERO: return "fp.isZero";
+  case kind::FLOATINGPOINT_IS_INF: return "fp.isInfinite";
+  case kind::FLOATINGPOINT_IS_NAN: return "fp.isNaN";
+  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";

diff --git a/src/theory/fp/fp_word_blaster.cpp b/src/theory/fp/fp_word_blaster.cpp
index 70d77abedce1b6f0db8b25eb3d3782fb0b085065..2ff2ec4aaced5b2c1f6f0369627e8f87de282e25 100644 (file)
--- a/src/theory/fp/fp_word_blaster.cpp
+++ b/src/theory/fp/fp_word_blaster.cpp
@@ -1156,7 +1156,7 @@ Node FpWordBlaster::wordBlast(TNode node)
             break;
 
           /* ---- Tester -------------------------------------------- */
-          case kind::FLOATINGPOINT_ISN:
+          case kind::FLOATINGPOINT_IS_NORMAL:
             Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
             d_boolMap.insert(
                 cur,
@@ -1164,7 +1164,7 @@ Node FpWordBlaster::wordBlast(TNode node)
                                          (*d_fpMap.find(cur[0])).second));
             break;
 
-          case kind::FLOATINGPOINT_ISSN:
+          case kind::FLOATINGPOINT_IS_SUBNORMAL:
             Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
             d_boolMap.insert(
                 cur,
@@ -1172,7 +1172,7 @@ Node FpWordBlaster::wordBlast(TNode node)
                                             (*d_fpMap.find(cur[0])).second));
             break;
 
-          case kind::FLOATINGPOINT_ISZ:
+          case kind::FLOATINGPOINT_IS_ZERO:
             Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
             d_boolMap.insert(
                 cur,
@@ -1180,7 +1180,7 @@ Node FpWordBlaster::wordBlast(TNode node)
                                        (*d_fpMap.find(cur[0])).second));
             break;
 
-          case kind::FLOATINGPOINT_ISINF:
+          case kind::FLOATINGPOINT_IS_INF:
             Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
             d_boolMap.insert(
                 cur,
@@ -1188,7 +1188,7 @@ Node FpWordBlaster::wordBlast(TNode node)
                                            (*d_fpMap.find(cur[0])).second));
             break;
 
-          case kind::FLOATINGPOINT_ISNAN:
+          case kind::FLOATINGPOINT_IS_NAN:
             Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
             d_boolMap.insert(
                 cur,
@@ -1196,7 +1196,7 @@ Node FpWordBlaster::wordBlast(TNode node)
                                       (*d_fpMap.find(cur[0])).second));
             break;
 
-          case kind::FLOATINGPOINT_ISNEG:
+          case kind::FLOATINGPOINT_IS_NEG:
             Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
             d_boolMap.insert(
                 cur,
@@ -1204,7 +1204,7 @@ Node FpWordBlaster::wordBlast(TNode node)
                                            (*d_fpMap.find(cur[0])).second));
             break;
 
-          case kind::FLOATINGPOINT_ISPOS:
+          case kind::FLOATINGPOINT_IS_POS:
             Assert(d_fpMap.find(cur[0]) != d_fpMap.end());
             d_boolMap.insert(
                 cur,

diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds
index fca5363fc9a5c3f7c67bc95ad32d1a753a0f50de..08ccde2f5d680b7c79f71876abd927f047b5cee8 100644 (file)
--- a/src/theory/fp/kinds
+++ b/src/theory/fp/kinds
@@ -134,26 +134,26 @@ typerule FLOATINGPOINT_GT   ::cvc5::theory::fp::FloatingPointTestTypeRule
 
 
 
-operator FLOATINGPOINT_ISN 1 "floating-point is normal"
-typerule FLOATINGPOINT_ISN   ::cvc5::theory::fp::FloatingPointTestTypeRule
+operator FLOATINGPOINT_IS_NORMAL 1 "floating-point is normal"
+typerule FLOATINGPOINT_IS_NORMAL   ::cvc5::theory::fp::FloatingPointTestTypeRule
 
-operator FLOATINGPOINT_ISSN 1 "floating-point is sub-normal"
-typerule FLOATINGPOINT_ISSN   ::cvc5::theory::fp::FloatingPointTestTypeRule
+operator FLOATINGPOINT_IS_SUBNORMAL 1 "floating-point is sub-normal"
+typerule FLOATINGPOINT_IS_SUBNORMAL   ::cvc5::theory::fp::FloatingPointTestTypeRule
 
-operator FLOATINGPOINT_ISZ 1 "floating-point is zero"
-typerule FLOATINGPOINT_ISZ   ::cvc5::theory::fp::FloatingPointTestTypeRule
+operator FLOATINGPOINT_IS_ZERO 1 "floating-point is zero"
+typerule FLOATINGPOINT_IS_ZERO   ::cvc5::theory::fp::FloatingPointTestTypeRule
 
-operator FLOATINGPOINT_ISINF 1 "floating-point is infinite"
-typerule FLOATINGPOINT_ISINF   ::cvc5::theory::fp::FloatingPointTestTypeRule
+operator FLOATINGPOINT_IS_INF 1 "floating-point is infinite"
+typerule FLOATINGPOINT_IS_INF   ::cvc5::theory::fp::FloatingPointTestTypeRule
 
-operator FLOATINGPOINT_ISNAN 1 "floating-point is NaN"
-typerule FLOATINGPOINT_ISNAN   ::cvc5::theory::fp::FloatingPointTestTypeRule
+operator FLOATINGPOINT_IS_NAN 1 "floating-point is NaN"
+typerule FLOATINGPOINT_IS_NAN   ::cvc5::theory::fp::FloatingPointTestTypeRule
 
-operator FLOATINGPOINT_ISNEG 1 "floating-point is negative"
-typerule FLOATINGPOINT_ISNEG   ::cvc5::theory::fp::FloatingPointTestTypeRule
+operator FLOATINGPOINT_IS_NEG 1 "floating-point is negative"
+typerule FLOATINGPOINT_IS_NEG   ::cvc5::theory::fp::FloatingPointTestTypeRule
 
-operator FLOATINGPOINT_ISPOS 1 "floating-point is positive"
-typerule FLOATINGPOINT_ISPOS   ::cvc5::theory::fp::FloatingPointTestTypeRule
+operator FLOATINGPOINT_IS_POS 1 "floating-point is positive"
+typerule FLOATINGPOINT_IS_POS   ::cvc5::theory::fp::FloatingPointTestTypeRule
 
 
 

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 547e525031fe70e3e32007c1a51f72ebd7855ad5..1817e53ff6f2fdb9937629b1f8a0a76f7a44060b 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -114,13 +114,13 @@ void TheoryFp::finishInit()
   d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_LT);
   // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_GEQ); // Removed
   // d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_GT); // Removed
-  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISN);
-  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISSN);
-  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISZ);
-  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISINF);
-  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISNAN);
-  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISNEG);
-  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_ISPOS);
+  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_NORMAL);
+  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_SUBNORMAL);
+  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_ZERO);
+  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_INF);
+  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_IS_NAN);
+  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);
@@ -221,9 +221,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
       Node defined = nm->mkNode(
           kind::AND,
           nm->mkNode(kind::NOT,
-                     nm->mkNode(kind::FLOATINGPOINT_ISNAN, concrete[0])),
+                     nm->mkNode(kind::FLOATINGPOINT_IS_NAN, concrete[0])),
           nm->mkNode(kind::NOT,
-                     nm->mkNode(kind::FLOATINGPOINT_ISINF, concrete[0])));
+                     nm->mkNode(kind::FLOATINGPOINT_IS_INF, concrete[0])));
       // First the "forward" constraints
       Node fg = nm->mkNode(
           kind::IMPLIES,
@@ -508,19 +508,19 @@ void TheoryFp::registerTerm(TNode node)
 
   // Give the expansion of classifications in terms of equalities
   // This should make equality reasoning slightly more powerful.
-  if ((k == kind::FLOATINGPOINT_ISNAN) || (k == kind::FLOATINGPOINT_ISZ)
-      || (k == kind::FLOATINGPOINT_ISINF))
+  if ((k == kind::FLOATINGPOINT_IS_NAN) || (k == kind::FLOATINGPOINT_IS_ZERO)
+      || (k == kind::FLOATINGPOINT_IS_INF))
   {
     NodeManager* nm = NodeManager::currentNM();
     FloatingPointSize s = node[0].getType().getConst<FloatingPointSize>();
     Node equalityAlias = Node::null();
 
-    if (k == kind::FLOATINGPOINT_ISNAN)
+    if (k == kind::FLOATINGPOINT_IS_NAN)
     {
       equalityAlias = nm->mkNode(
           kind::EQUAL, node[0], nm->mkConst(FloatingPoint::makeNaN(s)));
     }
-    else if (k == kind::FLOATINGPOINT_ISZ)
+    else if (k == kind::FLOATINGPOINT_IS_ZERO)
     {
       equalityAlias = nm->mkNode(
           kind::OR,
@@ -531,7 +531,7 @@ void TheoryFp::registerTerm(TNode node)
                      node[0],
                      nm->mkConst(FloatingPoint::makeZero(s, false))));
     }
-    else if (k == kind::FLOATINGPOINT_ISINF)
+    else if (k == kind::FLOATINGPOINT_IS_INF)
     {
       equalityAlias =
           nm->mkNode(kind::OR,
@@ -562,14 +562,14 @@ void TheoryFp::registerTerm(TNode node)
     Node pd =
         nm->mkNode(kind::IMPLIES,
                    nm->mkNode(kind::OR,
-                              nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]),
-                              nm->mkNode(kind::FLOATINGPOINT_ISINF, node[0])),
+                              nm->mkNode(kind::FLOATINGPOINT_IS_NAN, node[0]),
+                              nm->mkNode(kind::FLOATINGPOINT_IS_INF, node[0])),
                    nm->mkNode(kind::EQUAL, node, node[1]));
     handleLemma(pd, InferenceId::FP_REGISTER_TERM);
 
     Node z = nm->mkNode(
         kind::IMPLIES,
-        nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
+        nm->mkNode(kind::FLOATINGPOINT_IS_ZERO, node[0]),
         nm->mkNode(kind::EQUAL, node, nm->mkConstReal(Rational(0U))));
     handleLemma(z, InferenceId::FP_REGISTER_TERM);
     return;
@@ -586,7 +586,7 @@ void TheoryFp::registerTerm(TNode node)
     d_abstractionMap.insert(sk, node);
 
     Node nnan =
-        nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node));
+        nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_IS_NAN, node));
     handleLemma(nnan, InferenceId::FP_REGISTER_TERM);
 
     Node z = nm->mkNode(

diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 779d02ab379ef1fa8f33f250ca9736adaaaf50f7..0fddbe9b4afeb7669d489071cf09989c0a024171 100644 (file)
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -186,16 +186,22 @@ namespace rewrite {
     Assert(node.getKind() == kind::FLOATINGPOINT_EQ);
     NodeManager *nm = NodeManager::currentNM();
 
-    return RewriteResponse(REWRITE_DONE,
-                          nm->mkNode(kind::AND,
-                                     nm->mkNode(kind::AND,
-                                                nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0])),
-                                                nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[1]))),
-                                     nm->mkNode(kind::OR,
-                                                nm->mkNode(kind::EQUAL, node[0], node[1]),
-                                                nm->mkNode(kind::AND,
-                                                           nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]),
-                                                           nm->mkNode(kind::FLOATINGPOINT_ISZ, node[1])))));
+    return RewriteResponse(
+        REWRITE_DONE,
+        nm->mkNode(
+            kind::AND,
+            nm->mkNode(
+                kind::AND,
+                nm->mkNode(kind::NOT,
+                           nm->mkNode(kind::FLOATINGPOINT_IS_NAN, node[0])),
+                nm->mkNode(kind::NOT,
+                           nm->mkNode(kind::FLOATINGPOINT_IS_NAN, node[1]))),
+            nm->mkNode(
+                kind::OR,
+                nm->mkNode(kind::EQUAL, node[0], node[1]),
+                nm->mkNode(kind::AND,
+                           nm->mkNode(kind::FLOATINGPOINT_IS_ZERO, node[0]),
+                           nm->mkNode(kind::FLOATINGPOINT_IS_ZERO, node[1])))));
   }
 
   RewriteResponse geqToleq(TNode node, bool isPreRewrite)
@@ -303,11 +309,11 @@ namespace rewrite {
   }
 
   RewriteResponse removeSignOperations (TNode node, bool isPreRewrite) {
-    Assert(node.getKind() == kind::FLOATINGPOINT_ISN
-           || node.getKind() == kind::FLOATINGPOINT_ISSN
-           || node.getKind() == kind::FLOATINGPOINT_ISZ
-           || node.getKind() == kind::FLOATINGPOINT_ISINF
-           || node.getKind() == kind::FLOATINGPOINT_ISNAN);
+    Assert(node.getKind() == kind::FLOATINGPOINT_IS_NORMAL
+           || node.getKind() == kind::FLOATINGPOINT_IS_SUBNORMAL
+           || node.getKind() == kind::FLOATINGPOINT_IS_ZERO
+           || node.getKind() == kind::FLOATINGPOINT_IS_INF
+           || node.getKind() == kind::FLOATINGPOINT_IS_NAN);
     Assert(node.getNumChildren() == 1);
 
     Kind childKind(node[0].getKind());
@@ -363,7 +369,7 @@ namespace rewrite {
       return RewriteResponse(
           isPreRewrite ? REWRITE_DONE : REWRITE_AGAIN_FULL,
           nm->mkNode(kind::NOT,
-                     nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0])));
+                     nm->mkNode(kind::FLOATINGPOINT_IS_NAN, node[0])));
     }
     return RewriteResponse(REWRITE_DONE, node);
   }
@@ -716,7 +722,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse isNormal(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_ISN);
+    Assert(node.getKind() == kind::FLOATINGPOINT_IS_NORMAL);
     Assert(node.getNumChildren() == 1);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isNormal()));
@@ -724,7 +730,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse isSubnormal(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_ISSN);
+    Assert(node.getKind() == kind::FLOATINGPOINT_IS_SUBNORMAL);
     Assert(node.getNumChildren() == 1);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isSubnormal()));
@@ -732,7 +738,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse isZero(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_ISZ);
+    Assert(node.getKind() == kind::FLOATINGPOINT_IS_ZERO);
     Assert(node.getNumChildren() == 1);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isZero()));
@@ -740,7 +746,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse isInfinite(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_ISINF);
+    Assert(node.getKind() == kind::FLOATINGPOINT_IS_INF);
     Assert(node.getNumChildren() == 1);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isInfinite()));
@@ -748,7 +754,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse isNaN(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_ISNAN);
+    Assert(node.getKind() == kind::FLOATINGPOINT_IS_NAN);
     Assert(node.getNumChildren() == 1);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isNaN()));
@@ -756,7 +762,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse isNegative(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_ISNEG);
+    Assert(node.getKind() == kind::FLOATINGPOINT_IS_NEG);
     Assert(node.getNumChildren() == 1);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isNegative()));
@@ -764,7 +770,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse isPositive(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_ISPOS);
+    Assert(node.getKind() == kind::FLOATINGPOINT_IS_POS);
     Assert(node.getNumChildren() == 1);
 
     return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isPositive()));
@@ -1159,13 +1165,13 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
       rewrite::then<rewrite::breakChain, rewrite::gtTolt>;
 
   /******** Classifications ********/
-  d_preRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity;
+  d_preRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] = rewrite::identity;
+  d_preRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] = rewrite::identity;
+  d_preRewriteTable[kind::FLOATINGPOINT_IS_ZERO] = rewrite::identity;
+  d_preRewriteTable[kind::FLOATINGPOINT_IS_INF] = rewrite::identity;
+  d_preRewriteTable[kind::FLOATINGPOINT_IS_NAN] = rewrite::identity;
+  d_preRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity;
+  d_preRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
 
   /******** Conversions ********/
   d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] =
@@ -1245,13 +1251,18 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
   d_postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::identity;
 
   /******** Classifications ********/
-  d_postRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::removeSignOperations;
-  d_postRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::removeSignOperations;
-  d_postRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::removeSignOperations;
-  d_postRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::removeSignOperations;
-  d_postRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::removeSignOperations;
-  d_postRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity;
+  d_postRewriteTable[kind::FLOATINGPOINT_IS_NORMAL] =
+      rewrite::removeSignOperations;
+  d_postRewriteTable[kind::FLOATINGPOINT_IS_SUBNORMAL] =
+      rewrite::removeSignOperations;
+  d_postRewriteTable[kind::FLOATINGPOINT_IS_ZERO] =
+      rewrite::removeSignOperations;
+  d_postRewriteTable[kind::FLOATINGPOINT_IS_INF] =
+      rewrite::removeSignOperations;
+  d_postRewriteTable[kind::FLOATINGPOINT_IS_NAN] =
+      rewrite::removeSignOperations;
+  d_postRewriteTable[kind::FLOATINGPOINT_IS_NEG] = rewrite::identity;
+  d_postRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
 
   /******** Conversions ********/
   d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] =
@@ -1331,13 +1342,14 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
   d_constantFoldTable[kind::FLOATINGPOINT_LT] = constantFold::lt;
 
   /******** Classifications ********/
-  d_constantFoldTable[kind::FLOATINGPOINT_ISN] = constantFold::isNormal;
-  d_constantFoldTable[kind::FLOATINGPOINT_ISSN] = constantFold::isSubnormal;
-  d_constantFoldTable[kind::FLOATINGPOINT_ISZ] = constantFold::isZero;
-  d_constantFoldTable[kind::FLOATINGPOINT_ISINF] = constantFold::isInfinite;
-  d_constantFoldTable[kind::FLOATINGPOINT_ISNAN] = constantFold::isNaN;
-  d_constantFoldTable[kind::FLOATINGPOINT_ISNEG] = constantFold::isNegative;
-  d_constantFoldTable[kind::FLOATINGPOINT_ISPOS] = constantFold::isPositive;
+  d_constantFoldTable[kind::FLOATINGPOINT_IS_NORMAL] = constantFold::isNormal;
+  d_constantFoldTable[kind::FLOATINGPOINT_IS_SUBNORMAL] =
+      constantFold::isSubnormal;
+  d_constantFoldTable[kind::FLOATINGPOINT_IS_ZERO] = constantFold::isZero;
+  d_constantFoldTable[kind::FLOATINGPOINT_IS_INF] = constantFold::isInfinite;
+  d_constantFoldTable[kind::FLOATINGPOINT_IS_NAN] = constantFold::isNaN;
+  d_constantFoldTable[kind::FLOATINGPOINT_IS_NEG] = constantFold::isNegative;
+  d_constantFoldTable[kind::FLOATINGPOINT_IS_POS] = constantFold::isPositive;
 
   /******** Conversions ********/
   d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] =

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index c2a589565c0366246277c0a4b6ee9db621cad3ac..1eb722372cc4f115673733466117ba190169c4ee 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -1412,13 +1412,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     else if (types[i].isFloatingPoint())
     {
       Trace("sygus-grammar-def") << "...add FP predicates" << std::endl;
-      std::vector<Kind> fp_unary_predicates = {FLOATINGPOINT_ISN,
-                                               FLOATINGPOINT_ISSN,
-                                               FLOATINGPOINT_ISZ,
-                                               FLOATINGPOINT_ISINF,
-                                               FLOATINGPOINT_ISNAN,
-                                               FLOATINGPOINT_ISNEG,
-                                               FLOATINGPOINT_ISPOS};
+      std::vector<Kind> fp_unary_predicates = {FLOATINGPOINT_IS_NORMAL,
+                                               FLOATINGPOINT_IS_SUBNORMAL,
+                                               FLOATINGPOINT_IS_ZERO,
+                                               FLOATINGPOINT_IS_INF,
+                                               FLOATINGPOINT_IS_NAN,
+                                               FLOATINGPOINT_IS_NEG,
+                                               FLOATINGPOINT_IS_POS};
       for (const Kind kind : fp_unary_predicates)
       {
         sdtBool.addConstructor(kind, cargs);

diff --git a/test/api/cpp/issue4889.cpp b/test/api/cpp/issue4889.cpp
index 8e0853682e44e0ab995df483962ac3e56d581001..373aa6d006f14be45a44b1368105a1aedf802e6e 100644 (file)
--- a/test/api/cpp/issue4889.cpp
+++ b/test/api/cpp/issue4889.cpp
@@ -30,7 +30,7 @@ int main()
   Term const2 = slv.mkConst(sort_bool, "_c4");
   Term ite = slv.mkTerm(ITE, const2, const1, const0);
   Term rem = slv.mkTerm(FLOATINGPOINT_REM, ite, const1);
-  Term isnan = slv.mkTerm(FLOATINGPOINT_ISNAN, rem);
+  Term isnan = slv.mkTerm(FLOATINGPOINT_IS_NAN, rem);
   slv.checkSatAssuming(isnan);
   return 0;
 }