Rename TO_FP operator kinds. (#8285)

FLOATINGPOINT_TO_FP_FP -> FLOATINGPOINT_TO_FP_FROM_FP
FLOATINGPOINT_TO_FP_IEEE_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_IEEE_BV
FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_SBV
FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR -> FLOATINGPOINT_TO_FP_FROM_UBV
FLOATINGPOINT_TO_FP_REAL -> FLOATINGPOINT_TO_FP_FROM_REAL

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 1dffd5776a63ba8884631c644ffcac179441a911..d1e0dc12ea8f5944cbfbd07c3fca8f7727295a30 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -238,15 +238,12 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
     {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,
-     cvc5::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
-    {FLOATINGPOINT_TO_FP_REAL, cvc5::Kind::FLOATINGPOINT_TO_FP_REAL},
-    {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
-     cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
-    {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
-     cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
+    {FLOATINGPOINT_TO_FP_FROM_FP, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_FP},
+    {FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
+     cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV},
+    {FLOATINGPOINT_TO_FP_FROM_REAL, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_REAL},
+    {FLOATINGPOINT_TO_FP_FROM_SBV, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_SBV},
+    {FLOATINGPOINT_TO_FP_FROM_UBV, cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_UBV},
     {FLOATINGPOINT_TO_FP_GENERIC, cvc5::Kind::FLOATINGPOINT_TO_FP_GENERIC},
     {FLOATINGPOINT_TO_UBV, cvc5::Kind::FLOATINGPOINT_TO_UBV},
     {FLOATINGPOINT_TO_SBV, cvc5::Kind::FLOATINGPOINT_TO_SBV},
@@ -534,24 +531,25 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
         {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,
-         FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
-        {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
-         FLOATINGPOINT_TO_FP_FLOATINGPOINT},
-        {cvc5::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
-         FLOATINGPOINT_TO_FP_FLOATINGPOINT},
-        {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL},
-        {cvc5::Kind::FLOATINGPOINT_TO_FP_REAL, FLOATINGPOINT_TO_FP_REAL},
-        {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
-         FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
-        {cvc5::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
-         FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
-        {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
-         FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
-        {cvc5::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
-         FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
+        {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP,
+         FLOATINGPOINT_TO_FP_FROM_IEEE_BV},
+        {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
+         FLOATINGPOINT_TO_FP_FROM_IEEE_BV},
+        {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_FP_OP,
+         FLOATINGPOINT_TO_FP_FROM_FP},
+        {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_FP, FLOATINGPOINT_TO_FP_FROM_FP},
+        {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_REAL_OP,
+         FLOATINGPOINT_TO_FP_FROM_REAL},
+        {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_REAL,
+         FLOATINGPOINT_TO_FP_FROM_REAL},
+        {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_SBV_OP,
+         FLOATINGPOINT_TO_FP_FROM_SBV},
+        {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_SBV,
+         FLOATINGPOINT_TO_FP_FROM_SBV},
+        {cvc5::Kind::FLOATINGPOINT_TO_FP_FROM_UBV_OP,
+         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},
@@ -705,11 +703,11 @@ const static std::unordered_set<Kind> s_indexed_kinds(
      FLOATINGPOINT_TO_UBV,
      FLOATINGPOINT_TO_SBV,
      BITVECTOR_EXTRACT,
-     FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
-     FLOATINGPOINT_TO_FP_FLOATINGPOINT,
-     FLOATINGPOINT_TO_FP_REAL,
-     FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
-     FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
+     FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
+     FLOATINGPOINT_TO_FP_FROM_FP,
+     FLOATINGPOINT_TO_FP_FROM_REAL,
+     FLOATINGPOINT_TO_FP_FROM_SBV,
+     FLOATINGPOINT_TO_FP_FROM_UBV,
      FLOATINGPOINT_TO_FP_GENERIC});
 
 namespace {
@@ -1877,11 +1875,11 @@ size_t Op::getNumIndicesHelper() const
     case FLOATINGPOINT_TO_SBV: size = 1; break;
     case REGEXP_REPEAT: size = 1; break;
     case BITVECTOR_EXTRACT: size = 2; break;
-    case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR: size = 2; break;
-    case FLOATINGPOINT_TO_FP_FLOATINGPOINT: size = 2; break;
-    case FLOATINGPOINT_TO_FP_REAL: size = 2; break;
-    case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: size = 2; break;
-    case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: size = 2; break;
+    case FLOATINGPOINT_TO_FP_FROM_IEEE_BV: size = 2; break;
+    case FLOATINGPOINT_TO_FP_FROM_FP: size = 2; break;
+    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:
@@ -1980,7 +1978,7 @@ Term Op::getIndexHelper(size_t index) const
                      : d_solver->mkRationalValHelper(ext.d_low);
       break;
     }
-    case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+    case FLOATINGPOINT_TO_FP_FROM_IEEE_BV:
     {
       cvc5::FloatingPointToFPIEEEBitVector ext =
           d_node->getConst<FloatingPointToFPIEEEBitVector>();
@@ -1990,7 +1988,7 @@ Term Op::getIndexHelper(size_t index) const
               : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
       break;
     }
-    case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+    case FLOATINGPOINT_TO_FP_FROM_FP:
     {
       cvc5::FloatingPointToFPFloatingPoint ext =
           d_node->getConst<FloatingPointToFPFloatingPoint>();
@@ -1999,7 +1997,7 @@ Term Op::getIndexHelper(size_t index) const
               : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
       break;
     }
-    case FLOATINGPOINT_TO_FP_REAL:
+    case FLOATINGPOINT_TO_FP_FROM_REAL:
     {
       cvc5::FloatingPointToFPReal ext =
           d_node->getConst<FloatingPointToFPReal>();
@@ -2009,7 +2007,7 @@ Term Op::getIndexHelper(size_t index) const
               : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
       break;
     }
-    case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+    case FLOATINGPOINT_TO_FP_FROM_SBV:
     {
       cvc5::FloatingPointToFPSignedBitVector ext =
           d_node->getConst<FloatingPointToFPSignedBitVector>();
@@ -2018,7 +2016,7 @@ Term Op::getIndexHelper(size_t index) const
               : d_solver->mkRationalValHelper(ext.getSize().significandWidth());
       break;
     }
-    case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+    case FLOATINGPOINT_TO_FP_FROM_UBV:
     {
       cvc5::FloatingPointToFPUnsignedBitVector ext =
           d_node->getConst<FloatingPointToFPUnsignedBitVector>();
@@ -2147,34 +2145,34 @@ std::pair<uint32_t, uint32_t> Op::getIndices() const
     cvc5::BitVectorExtract ext = d_node->getConst<BitVectorExtract>();
     indices = std::make_pair(ext.d_high, ext.d_low);
   }
-  else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR)
+  else if (k == FLOATINGPOINT_TO_FP_FROM_IEEE_BV)
   {
     cvc5::FloatingPointToFPIEEEBitVector ext =
         d_node->getConst<FloatingPointToFPIEEEBitVector>();
     indices = std::make_pair(ext.getSize().exponentWidth(),
                              ext.getSize().significandWidth());
   }
-  else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
+  else if (k == FLOATINGPOINT_TO_FP_FROM_FP)
   {
     cvc5::FloatingPointToFPFloatingPoint ext =
         d_node->getConst<FloatingPointToFPFloatingPoint>();
     indices = std::make_pair(ext.getSize().exponentWidth(),
                              ext.getSize().significandWidth());
   }
-  else if (k == FLOATINGPOINT_TO_FP_REAL)
+  else if (k == FLOATINGPOINT_TO_FP_FROM_REAL)
   {
     cvc5::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>();
     indices = std::make_pair(ext.getSize().exponentWidth(),
                              ext.getSize().significandWidth());
   }
-  else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
+  else if (k == FLOATINGPOINT_TO_FP_FROM_SBV)
   {
     cvc5::FloatingPointToFPSignedBitVector ext =
         d_node->getConst<FloatingPointToFPSignedBitVector>();
     indices = std::make_pair(ext.getSize().exponentWidth(),
                              ext.getSize().significandWidth());
   }
-  else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR)
+  else if (k == FLOATINGPOINT_TO_FP_FROM_UBV)
   {
     cvc5::FloatingPointToFPUnsignedBitVector ext =
         d_node->getConst<FloatingPointToFPUnsignedBitVector>();
@@ -6512,35 +6510,35 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
                     cvc5::BitVectorExtract(arg1, arg2))
                     .d_node);
       break;
-    case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+    case FLOATINGPOINT_TO_FP_FROM_IEEE_BV:
       res = Op(this,
                kind,
                *mkValHelper<cvc5::FloatingPointToFPIEEEBitVector>(
                     cvc5::FloatingPointToFPIEEEBitVector(arg1, arg2))
                     .d_node);
       break;
-    case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+    case FLOATINGPOINT_TO_FP_FROM_FP:
       res = Op(this,
                kind,
                *mkValHelper<cvc5::FloatingPointToFPFloatingPoint>(
                     cvc5::FloatingPointToFPFloatingPoint(arg1, arg2))
                     .d_node);
       break;
-    case FLOATINGPOINT_TO_FP_REAL:
+    case FLOATINGPOINT_TO_FP_FROM_REAL:
       res = Op(this,
                kind,
                *mkValHelper<cvc5::FloatingPointToFPReal>(
                     cvc5::FloatingPointToFPReal(arg1, arg2))
                     .d_node);
       break;
-    case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+    case FLOATINGPOINT_TO_FP_FROM_SBV:
       res = Op(this,
                kind,
                *mkValHelper<cvc5::FloatingPointToFPSignedBitVector>(
                     cvc5::FloatingPointToFPSignedBitVector(arg1, arg2))
                     .d_node);
       break;
-    case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+    case FLOATINGPOINT_TO_FP_FROM_UBV:
       res = Op(this,
                kind,
                *mkValHelper<cvc5::FloatingPointToFPUnsignedBitVector>(

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 3a10aa0a650c474bb98f91df3cea68b2ffa338f3..037c149382f8dac99fc5a00403aa95b7bb5149b9 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3404,11 +3404,11 @@ class CVC5_EXPORT Solver
   /**
    * Create operator of Kind:
    *   - BITVECTOR_EXTRACT
-   *   - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
-   *   - FLOATINGPOINT_TO_FP_FLOATINGPOINT
-   *   - FLOATINGPOINT_TO_FP_REAL
-   *   - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
-   *   - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
+   *   - FLOATINGPOINT_TO_FP_FROM_IEEE_BV
+   *   - FLOATINGPOINT_TO_FP_FROM_FP
+   *   - 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

diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 24b1b5ed75e13a289642d186f6618794fc45dc65..e4ddcaa0031c7fb3c2e6300619aaa372ec639537 100644 (file)
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -1643,14 +1643,14 @@ enum Kind : int32_t
    * Conversion from an IEEE-754 bit vector to floating-point.
    *
    * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
+   *   - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_IEEE_BV
    *   - 2: Term of sort FloatingPoint
    *
    * Create with:
    *   - `Solver::mkTerm(const Op& op, const Term& child) const`
    *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
    */
-  FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
+  FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
   /**
    * Operator for to_fp from floating point.
    *
@@ -1664,14 +1664,14 @@ enum Kind : int32_t
    * Conversion between floating-point sorts.
    *
    * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_FLOATINGPOINT
+   *   - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_FP
    *   - 2: Term of sort FloatingPoint
    *
    * Create with:
    *   - `Solver::mkTerm(const Op& op, const Term& child) const`
    *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
    */
-  FLOATINGPOINT_TO_FP_FLOATINGPOINT,
+  FLOATINGPOINT_TO_FP_FROM_FP,
   /**
    * Operator for to_fp from real.
    *
@@ -1685,14 +1685,14 @@ enum Kind : int32_t
    * Conversion from a real to floating-point.
    *
    * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_REAL
+   *   - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_REAL
    *   - 2: Term of sort FloatingPoint
    *
    * Create with:
    *   - `Solver::mkTerm(const Op& op, const Term& child) const`
    *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
    */
-  FLOATINGPOINT_TO_FP_REAL,
+  FLOATINGPOINT_TO_FP_FROM_REAL,
   /**
    * Operator for to_fp from signed bit vector
    *
@@ -1706,14 +1706,14 @@ enum Kind : int32_t
    * Conversion from a signed bit vector to floating-point.
    *
    * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
+   *   - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_SBV
    *   - 2: Term of sort FloatingPoint
    *
    * Create with:
    *   - `Solver::mkTerm(const Op& op, const Term& child) const`
    *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
    */
-  FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
+  FLOATINGPOINT_TO_FP_FROM_SBV,
   /**
    * Operator for to_fp from unsigned bit vector.
    *
@@ -1727,14 +1727,14 @@ enum Kind : int32_t
    * Converting an unsigned bit vector to floating-point.
    *
    * Parameters:
-   *   - 1: Op of kind FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
+   *   - 1: Op of kind FLOATINGPOINT_TO_FP_FROM_UBV
    *   - 2: Term of sort FloatingPoint
    *
    * Create with:
    *   - `Solver::mkTerm(const Op& op, const Term& child) const`
    *   - `Solver::mkTerm(const Op& op, const std::vector<Term>& children) const`
    */
-  FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
+  FLOATINGPOINT_TO_FP_FROM_UBV,
   /**
    * Operator for a generic to_fp.
    *

diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 6e73b3300873d532e192ac2c037f7ffcde13a38b..6fd3444ebdb1e050ce4221baee095a3e43cced33 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -732,11 +732,11 @@ public class Solver implements IPointer, AutoCloseable
   /**
    * Create operator of Kind:
    *   - BITVECTOR_EXTRACT
-   *   - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
-   *   - FLOATINGPOINT_TO_FP_FLOATINGPOINT
-   *   - FLOATINGPOINT_TO_FP_REAL
-   *   - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
-   *   - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
+   *   - FLOATINGPOINT_TO_FP_FROM_IEEE_BV
+   *   - FLOATINGPOINT_TO_FP_FROM_FP
+   *   - 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

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index ec83dff0b1d864307a848b2a36df2670613837d2..41389489f5daab6e9c70608aa81f64d3ba26799e 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -237,8 +237,8 @@ void Smt2::addFloatingPointOperators() {
   addIndexedOperator(api::FLOATINGPOINT_TO_FP_GENERIC,
                      api::FLOATINGPOINT_TO_FP_GENERIC,
                      "to_fp");
-  addIndexedOperator(api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
-                     api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
+  addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_UBV,
+                     api::FLOATINGPOINT_TO_FP_FROM_UBV,
                      "to_fp_unsigned");
   addIndexedOperator(
       api::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV, "fp.to_ubv");
@@ -247,17 +247,17 @@ void Smt2::addFloatingPointOperators() {
 
   if (!strictModeEnabled())
   {
-    addIndexedOperator(api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
-                       api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
+    addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
+                       api::FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
                        "to_fp_bv");
-    addIndexedOperator(api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
-                       api::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
+    addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_FP,
+                       api::FLOATINGPOINT_TO_FP_FROM_FP,
                        "to_fp_fp");
-    addIndexedOperator(api::FLOATINGPOINT_TO_FP_REAL,
-                       api::FLOATINGPOINT_TO_FP_REAL,
+    addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_REAL,
+                       api::FLOATINGPOINT_TO_FP_FROM_REAL,
                        "to_fp_real");
-    addIndexedOperator(api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
-                       api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
+    addIndexedOperator(api::FLOATINGPOINT_TO_FP_FROM_SBV,
+                       api::FLOATINGPOINT_TO_FP_FROM_SBV,
                        "to_fp_signed");
   }
 }

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 72d303be870e3a28f4e11210c5185c27cb84920c..cd37cd049986f4d0b41fbfb2bfb01b37b9f32aaf 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -384,7 +384,7 @@ void Smt2Printer::toStream(std::ostream& out,
     case kind::INT_TO_BITVECTOR_OP:
       out << "(_ int2bv " << n.getConst<IntToBitVector>().d_size << ")";
       break;
-    case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP:
+    case kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP:
       out << "(_ to_fp "
           << n.getConst<FloatingPointToFPIEEEBitVector>()
                  .getSize()
@@ -395,7 +395,7 @@ void Smt2Printer::toStream(std::ostream& out,
                  .significandWidth()
           << ")";
       break;
-    case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP:
+    case kind::FLOATINGPOINT_TO_FP_FROM_FP_OP:
       out << "(_ to_fp "
           << n.getConst<FloatingPointToFPFloatingPoint>()
                  .getSize()
@@ -406,14 +406,14 @@ void Smt2Printer::toStream(std::ostream& out,
                  .significandWidth()
           << ")";
       break;
-    case kind::FLOATINGPOINT_TO_FP_REAL_OP:
+    case kind::FLOATINGPOINT_TO_FP_FROM_REAL_OP:
       out << "(_ to_fp "
           << n.getConst<FloatingPointToFPReal>().getSize().exponentWidth()
           << ' '
           << n.getConst<FloatingPointToFPReal>().getSize().significandWidth()
           << ")";
       break;
-    case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP:
+    case kind::FLOATINGPOINT_TO_FP_FROM_SBV_OP:
       out << "(_ to_fp "
           << n.getConst<FloatingPointToFPSignedBitVector>()
                  .getSize()
@@ -424,7 +424,7 @@ void Smt2Printer::toStream(std::ostream& out,
                  .significandWidth()
           << ")";
       break;
-    case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP:
+    case kind::FLOATINGPOINT_TO_FP_FROM_UBV_OP:
       out << "(_ to_fp_unsigned "
           << n.getConst<FloatingPointToFPUnsignedBitVector>()
                  .getSize()
@@ -755,11 +755,11 @@ void Smt2Printer::toStream(std::ostream& out,
   }
 
   // fp theory
-  case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
-  case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
-  case kind::FLOATINGPOINT_TO_FP_REAL:
-  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
-  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+  case kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV:
+  case kind::FLOATINGPOINT_TO_FP_FROM_FP:
+  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:
@@ -1196,11 +1196,11 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v)
   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";
-  case kind::FLOATINGPOINT_TO_FP_REAL: return "to_fp";
-  case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR: return "to_fp";
-  case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR: return "to_fp_unsigned";
+  case kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV: return "to_fp";
+  case kind::FLOATINGPOINT_TO_FP_FROM_FP: return "to_fp";
+  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";

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index cbb94558457a3e373cf62452987b12f943e13d96..3a9e26d559d02cba3deaf928073a5fb7486daeb6 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -839,11 +839,12 @@ bool LfscNodeConverter::isIndexedOperatorKind(Kind k)
          || k == BITVECTOR_ZERO_EXTEND || k == BITVECTOR_SIGN_EXTEND
          || k == BITVECTOR_ROTATE_LEFT || k == BITVECTOR_ROTATE_RIGHT
          || k == INT_TO_BITVECTOR || k == IAND
-         || k == FLOATINGPOINT_TO_FP_FLOATINGPOINT
-         || k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
-         || k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
-         || k == FLOATINGPOINT_TO_FP_REAL || k == FLOATINGPOINT_TO_FP_GENERIC
-         || k == APPLY_UPDATER || k == APPLY_TESTER;
+         || 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 == APPLY_TESTER;
 }
 
 std::vector<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n)
@@ -893,7 +894,7 @@ std::vector<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n)
     case IAND:
       indices.push_back(nm->mkConstInt(Rational(n.getConst<IntAnd>().d_size)));
       break;
-    case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+    case FLOATINGPOINT_TO_FP_FROM_FP:
     {
       const FloatingPointToFPFloatingPoint& ffp =
           n.getConst<FloatingPointToFPFloatingPoint>();
@@ -901,7 +902,7 @@ std::vector<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n)
       indices.push_back(nm->mkConstInt(ffp.getSize().significandWidth()));
     }
     break;
-    case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+    case FLOATINGPOINT_TO_FP_FROM_IEEE_BV:
     {
       const FloatingPointToFPIEEEBitVector& fbv =
           n.getConst<FloatingPointToFPIEEEBitVector>();
@@ -909,7 +910,7 @@ std::vector<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n)
       indices.push_back(nm->mkConstInt(fbv.getSize().significandWidth()));
     }
     break;
-    case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+    case FLOATINGPOINT_TO_FP_FROM_SBV:
     {
       const FloatingPointToFPSignedBitVector& fsbv =
           n.getConst<FloatingPointToFPSignedBitVector>();
@@ -917,7 +918,7 @@ std::vector<Node> LfscNodeConverter::getOperatorIndices(Kind k, Node n)
       indices.push_back(nm->mkConstInt(fsbv.getSize().significandWidth()));
     }
     break;
-    case FLOATINGPOINT_TO_FP_REAL:
+    case FLOATINGPOINT_TO_FP_FROM_REAL:
     {
       const FloatingPointToFPReal& fr = n.getConst<FloatingPointToFPReal>();
       indices.push_back(nm->mkConstInt(fr.getSize().exponentWidth()));
@@ -1057,19 +1058,19 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply)
         }
       }
       // must avoid overloading for to_fp variants
-      if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
+      if (k == FLOATINGPOINT_TO_FP_FROM_FP)
       {
         opName << "to_fp_fp";
       }
-      else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR)
+      else if (k == FLOATINGPOINT_TO_FP_FROM_IEEE_BV)
       {
         opName << "to_fp_ieee_bv";
       }
-      else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
+      else if (k == FLOATINGPOINT_TO_FP_FROM_SBV)
       {
         opName << "to_fp_sbv";
       }
-      else if (k == FLOATINGPOINT_TO_FP_REAL)
+      else if (k == FLOATINGPOINT_TO_FP_FROM_REAL)
       {
         opName << "to_fp_real";
       }

diff --git a/src/theory/fp/fp_word_blaster.cpp b/src/theory/fp/fp_word_blaster.cpp
index 2ff2ec4aaced5b2c1f6f0369627e8f87de282e25..41d78b44d3b7c525592b92cc661da8c2fb267aad 100644 (file)
--- a/src/theory/fp/fp_word_blaster.cpp
+++ b/src/theory/fp/fp_word_blaster.cpp
@@ -803,7 +803,7 @@ Node FpWordBlaster::sbvToNode(const sbv& s) const { return s; }
 FpWordBlaster::uf FpWordBlaster::buildComponents(TNode current)
 {
   Assert(Theory::isLeafOf(current, THEORY_FP)
-         || current.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
+         || current.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_REAL);
 
   NodeManager* nm = NodeManager::currentNM();
   uf tmp(nm->mkNode(kind::FLOATINGPOINT_COMPONENT_NAN, current),
@@ -1050,7 +1050,7 @@ Node FpWordBlaster::wordBlast(TNode node)
               break;
 
             /* ---- Conversions ---- */
-            case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
+            case kind::FLOATINGPOINT_TO_FP_FROM_FP:
               Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
               Assert(d_fpMap.find(cur[1]) != d_fpMap.end());
               d_fpMap.insert(cur,
@@ -1073,12 +1073,12 @@ Node FpWordBlaster::wordBlast(TNode node)
             }
             break;
 
-            case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
+            case kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV:
               Assert(cur[0].getType().isBitVector());
               d_fpMap.insert(cur, symfpu::unpack<traits>(fpt(t), ubv(cur[0])));
               break;
 
-            case kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
+            case kind::FLOATINGPOINT_TO_FP_FROM_SBV:
               Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
               d_fpMap.insert(
                   cur,
@@ -1086,7 +1086,7 @@ Node FpWordBlaster::wordBlast(TNode node)
                       fpt(t), (*d_rmMap.find(cur[0])).second, sbv(cur[1])));
               break;
 
-            case kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
+            case kind::FLOATINGPOINT_TO_FP_FROM_UBV:
               Assert(d_rmMap.find(cur[0]) != d_rmMap.end());
               d_fpMap.insert(
                   cur,
@@ -1094,7 +1094,7 @@ Node FpWordBlaster::wordBlast(TNode node)
                       fpt(t), (*d_rmMap.find(cur[0])).second, ubv(cur[1])));
               break;
 
-            case kind::FLOATINGPOINT_TO_FP_REAL:
+            case kind::FLOATINGPOINT_TO_FP_FROM_REAL:
               d_fpMap.insert(cur, buildComponents(cur));
               // Rely on the real theory and theory combination
               // to handle the value

diff --git a/src/theory/fp/kinds b/src/theory/fp/kinds
index 08ccde2f5d680b7c79f71876abd927f047b5cee8..2044594969f5c6334b13cdf6089137d65491ebab 100644 (file)
--- a/src/theory/fp/kinds
+++ b/src/theory/fp/kinds
@@ -27,7 +27,7 @@ constant CONST_ROUNDINGMODE \
     RoundingMode \
     ::cvc5::RoundingModeHashFunction \
     "util/roundingmode.h" \
-    "a floating-point rounding mode"    
+    "a floating-point rounding mode"
 typerule CONST_ROUNDINGMODE    ::cvc5::theory::fp::RoundingModeConstantTypeRule
 
 
@@ -157,70 +157,70 @@ typerule FLOATINGPOINT_IS_POS   ::cvc5::theory::fp::FloatingPointTestTypeRule
 
 
 
-constant FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP \
+constant FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP \
     class \
     FloatingPointToFPIEEEBitVector \
     "::cvc5::FloatingPointConvertSortHashFunction<0x1>" \
     "util/floatingpoint.h" \
     "operator for to_fp from bit vector"
-typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule
+typerule FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule
 
-parameterized FLOATINGPOINT_TO_FP_IEEE_BITVECTOR FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP 1 "convert an IEEE-754 bit vector to floating-point"
-typerule FLOATINGPOINT_TO_FP_IEEE_BITVECTOR   ::cvc5::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule
+parameterized FLOATINGPOINT_TO_FP_FROM_IEEE_BV FLOATINGPOINT_TO_FP_FROM_IEEE_BV_OP 1 "convert an IEEE-754 bit vector to floating-point"
+typerule FLOATINGPOINT_TO_FP_FROM_IEEE_BV ::cvc5::theory::fp::FloatingPointToFPIEEEBitVectorTypeRule
 
 
 
-constant FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP \
+constant FLOATINGPOINT_TO_FP_FROM_FP_OP \
     class \
     FloatingPointToFPFloatingPoint \
     "::cvc5::FloatingPointConvertSortHashFunction<0x2>" \
     "util/floatingpoint.h" \
     "operator for to_fp from floating point"
-typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule
+typerule FLOATINGPOINT_TO_FP_FROM_FP_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule
 
-parameterized FLOATINGPOINT_TO_FP_FLOATINGPOINT FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP 2 "convert between floating-point sorts"
-typerule FLOATINGPOINT_TO_FP_FLOATINGPOINT   ::cvc5::theory::fp::FloatingPointToFPFloatingPointTypeRule
+parameterized FLOATINGPOINT_TO_FP_FROM_FP FLOATINGPOINT_TO_FP_FROM_FP_OP 2 "convert between floating-point sorts"
+typerule FLOATINGPOINT_TO_FP_FROM_FP   ::cvc5::theory::fp::FloatingPointToFPFloatingPointTypeRule
 
 
 
 
-constant FLOATINGPOINT_TO_FP_REAL_OP \
+constant FLOATINGPOINT_TO_FP_FROM_REAL_OP \
     class \
     FloatingPointToFPReal \
     "::cvc5::FloatingPointConvertSortHashFunction<0x4>" \
     "util/floatingpoint.h" \
     "operator for to_fp from real"
-typerule FLOATINGPOINT_TO_FP_REAL_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule
+typerule FLOATINGPOINT_TO_FP_FROM_REAL_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule
 
-parameterized FLOATINGPOINT_TO_FP_REAL FLOATINGPOINT_TO_FP_REAL_OP 2 "convert a real to floating-point"
-typerule FLOATINGPOINT_TO_FP_REAL   ::cvc5::theory::fp::FloatingPointToFPRealTypeRule
+parameterized FLOATINGPOINT_TO_FP_FROM_REAL FLOATINGPOINT_TO_FP_FROM_REAL_OP 2 "convert a real to floating-point"
+typerule FLOATINGPOINT_TO_FP_FROM_REAL   ::cvc5::theory::fp::FloatingPointToFPRealTypeRule
 
 
 
-constant FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP \
+constant FLOATINGPOINT_TO_FP_FROM_SBV_OP \
     class \
     FloatingPointToFPSignedBitVector \
     "::cvc5::FloatingPointConvertSortHashFunction<0x8>" \
     "util/floatingpoint.h" \
     "operator for to_fp from signed bit vector"
-typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule
+typerule FLOATINGPOINT_TO_FP_FROM_SBV_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule
 
-parameterized FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP 2 "convert a signed bit vector to floating-point"
-typerule FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR   ::cvc5::theory::fp::FloatingPointToFPSignedBitVectorTypeRule
+parameterized FLOATINGPOINT_TO_FP_FROM_SBV FLOATINGPOINT_TO_FP_FROM_SBV_OP 2 "convert a signed bit vector to floating-point"
+typerule FLOATINGPOINT_TO_FP_FROM_SBV   ::cvc5::theory::fp::FloatingPointToFPSignedBitVectorTypeRule
 
 
 
-constant FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP \
+constant FLOATINGPOINT_TO_FP_FROM_UBV_OP \
     class \
     FloatingPointToFPUnsignedBitVector \
     "::cvc5::FloatingPointConvertSortHashFunction<0x10>" \
     "util/floatingpoint.h" \
     "operator for to_fp from unsigned bit vector"
-typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule
+typerule FLOATINGPOINT_TO_FP_FROM_UBV_OP ::cvc5::theory::fp::FloatingPointParametricOpTypeRule
 
 
-parameterized FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP 2 "convert an unsigned bit vector to floating-point"
-typerule FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR   ::cvc5::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule
+parameterized FLOATINGPOINT_TO_FP_FROM_UBV FLOATINGPOINT_TO_FP_FROM_UBV_OP 2 "convert an unsigned bit vector to floating-point"
+typerule FLOATINGPOINT_TO_FP_FROM_UBV   ::cvc5::theory::fp::FloatingPointToFPUnsignedBitVectorTypeRule
 
 
 

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 1817e53ff6f2fdb9937629b1f8a0a76f7a44060b..d5f665d1e863f1cc476039fb429101f98f975d3d 100644 (file)
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -122,12 +122,11 @@ void TheoryFp::finishInit()
   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);
-  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_REAL);
-  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
-  d_equalityEngine->addFunctionKind(
-      kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
+  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV);
+  d_equalityEngine->addFunctionKind(kind::FLOATINGPOINT_TO_FP_FROM_FP);
+  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
 
@@ -245,7 +244,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
 
       // Then the backwards constraints
       Node floatAboveAbstract = rewrite(
-          nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
+          nm->mkNode(kind::FLOATINGPOINT_TO_FP_FROM_REAL,
                      nm->mkConst(FloatingPointToFPReal(
                          concrete[0].getType().getConst<FloatingPointSize>())),
                      nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE),
@@ -262,7 +261,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
       handleLemma(bg, InferenceId::FP_PREPROCESS);
 
       Node floatBelowAbstract = rewrite(
-          nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
+          nm->mkNode(kind::FLOATINGPOINT_TO_FP_FROM_REAL,
                      nm->mkConst(FloatingPointToFPReal(
                          concrete[0].getType().getConst<FloatingPointSize>())),
                      nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE),
@@ -287,7 +286,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
       return false;
     }
   }
-  else if (k == kind::FLOATINGPOINT_TO_FP_REAL)
+  else if (k == kind::FLOATINGPOINT_TO_FP_FROM_REAL)
   {
     // Get the values
     Assert(m->hasTerm(abstract)) << "Term " << abstract << " not in model";
@@ -313,7 +312,7 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
     NodeManager *nm = NodeManager::currentNM();
 
     Node evaluate =
-        nm->mkNode(kind::FLOATINGPOINT_TO_FP_REAL,
+        nm->mkNode(kind::FLOATINGPOINT_TO_FP_FROM_REAL,
                    nm->mkConst(FloatingPointToFPReal(
                        concrete.getType().getConst<FloatingPointSize>())),
                    rmValue,
@@ -576,7 +575,7 @@ void TheoryFp::registerTerm(TNode node)
 
     // TODO : bounds on the output from largest floats, #1914
   }
-  else if (k == kind::FLOATINGPOINT_TO_FP_REAL)
+  else if (k == kind::FLOATINGPOINT_TO_FP_FROM_REAL)
   {
     // Purify ((_ to_fp eb sb) rm x)
     NodeManager* nm = NodeManager::currentNM();

diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 0fddbe9b4afeb7669d489071cf09989c0a024171..655299af9dac2850dc99e2f054cb959a273382fe 100644 (file)
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -389,7 +389,7 @@ namespace rewrite {
   RewriteResponse toFPSignedBV(TNode node, bool isPreRewrite)
   {
     Assert(!isPreRewrite);
-    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
+    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_SBV);
 
     /* symFPU does not allow conversions from signed bit-vector of size 1 */
     if (node[1].getType().getBitVectorSize() == 1)
@@ -778,7 +778,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse convertFromIEEEBitVectorLiteral(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
+    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV);
 
     TNode op = node.getOperator();
     const FloatingPointToFPIEEEBitVector &param = op.getConst<FloatingPointToFPIEEEBitVector>();
@@ -794,7 +794,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse constantConvert(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
+    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_FP);
     Assert(node.getNumChildren() == 2);
 
     RoundingMode rm(node[0].getConst<RoundingMode>());
@@ -808,7 +808,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse convertFromRealLiteral(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL);
+    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_REAL);
 
     TNode op = node.getOperator();
     const FloatingPointSize& size =
@@ -826,7 +826,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse convertFromSBV(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
+    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_SBV);
 
     TNode op = node.getOperator();
     const FloatingPointSize& size =
@@ -854,7 +854,7 @@ RewriteResponse maxTotal(TNode node, bool isPreRewrite)
 
   RewriteResponse convertFromUBV(TNode node, bool isPreRewrite)
   {
-    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
+    Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FROM_UBV);
 
     TNode op = node.getOperator();
     const FloatingPointSize& size =
@@ -1174,15 +1174,11 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
   d_preRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
 
   /******** Conversions ********/
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] =
-      rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] =
-      rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] =
-      rewrite::identity;
-  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] =
-      rewrite::identity;
+  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] = rewrite::identity;
+  d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity;
+  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;
@@ -1265,15 +1261,13 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
   d_postRewriteTable[kind::FLOATINGPOINT_IS_POS] = rewrite::identity;
 
   /******** Conversions ********/
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] =
-      rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] =
+  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
       rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::identity;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] =
+  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] = rewrite::identity;
+  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] = rewrite::identity;
+  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] =
       rewrite::toFPSignedBV;
-  d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] =
-      rewrite::identity;
+  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;
@@ -1352,15 +1346,15 @@ TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u)
   d_constantFoldTable[kind::FLOATINGPOINT_IS_POS] = constantFold::isPositive;
 
   /******** Conversions ********/
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] =
+  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_IEEE_BV] =
       constantFold::convertFromIEEEBitVectorLiteral;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] =
+  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_FP] =
       constantFold::constantConvert;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_REAL] =
+  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_REAL] =
       constantFold::convertFromRealLiteral;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] =
+  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_SBV] =
       constantFold::convertFromSBV;
-  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] =
+  d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FROM_UBV] =
       constantFold::convertFromUBV;
   d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV] = constantFold::convertToUBV;
   d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV] = constantFold::convertToSBV;

diff --git a/src/theory/fp/theory_fp_type_rules.cpp b/src/theory/fp/theory_fp_type_rules.cpp
index 77c1ef8f027e746d6c9292cd5b341bde65f6615e..9a492b6c2ab8fadf99290415dae21cd8e2552d9b 100644 (file)
--- a/src/theory/fp/theory_fp_type_rules.cpp
+++ b/src/theory/fp/theory_fp_type_rules.cpp
@@ -688,7 +688,7 @@ TypeNode FloatingPointComponentBit::computeType(NodeManager* nodeManager,
                                          "sort");
     }
     if (!(Theory::isLeafOf(n[0], THEORY_FP)
-          || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+          || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_FROM_REAL))
     {
       throw TypeCheckingExceptionPrivate(n,
                                          "floating-point bit component "
@@ -718,7 +718,7 @@ TypeNode FloatingPointComponentExponent::computeType(NodeManager* nodeManager,
                                          "sort");
     }
     if (!(Theory::isLeafOf(n[0], THEORY_FP)
-          || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+          || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_FROM_REAL))
     {
       throw TypeCheckingExceptionPrivate(n,
                                          "floating-point exponent component "
@@ -754,7 +754,7 @@ TypeNode FloatingPointComponentSignificand::computeType(
                                          "floating-point sort");
     }
     if (!(Theory::isLeafOf(n[0], THEORY_FP)
-          || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
+          || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_FROM_REAL))
     {
       throw TypeCheckingExceptionPrivate(n,
                                          "floating-point significand "

diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp
index 9af3e90726eb2be4494faf0f71b6c4b03a98e71a..81501763cc8d1db86e4316f2f1ad201d8793beaf 100644 (file)
--- a/test/unit/api/cpp/op_black.cpp
+++ b/test/unit/api/cpp/op_black.cpp
@@ -60,14 +60,15 @@ TEST_F(TestApiBlackOp, getNumIndices)
   Op floatingpoint_to_ubv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11);
   Op floatingopint_to_sbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
   Op floatingpoint_to_fp_ieee_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 25);
   Op floatingpoint_to_fp_floatingpoint =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25);
-  Op floatingpoint_to_fp_real = d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 25);
+  Op floatingpoint_to_fp_real =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25);
   Op floatingpoint_to_fp_signed_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25);
   Op floatingpoint_to_fp_unsigned_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 4, 25);
   Op floatingpoint_to_fp_generic =
       d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25);
   Op regexp_loop = d_solver.mkOp(REGEXP_LOOP, 2, 3);
@@ -106,14 +107,15 @@ TEST_F(TestApiBlackOp, subscriptOperator)
   Op floatingpoint_to_ubv = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 4);
   Op floatingopint_to_sbv = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 4);
   Op floatingpoint_to_fp_ieee_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 5);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 5);
   Op floatingpoint_to_fp_floatingpoint =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 5);
-  Op floatingpoint_to_fp_real = d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 5);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 5);
+  Op floatingpoint_to_fp_real =
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 5);
   Op floatingpoint_to_fp_signed_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 5);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 5);
   Op floatingpoint_to_fp_unsigned_bitvector =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 5);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 4, 5);
   Op floatingpoint_to_fp_generic =
       d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 5);
   Op regexp_loop = d_solver.mkOp(REGEXP_LOOP, 4, 5);
@@ -204,7 +206,7 @@ TEST_F(TestApiBlackOp, getIndicesPairUint)
       (bitvector_extract_indices == std::pair<uint32_t, uint32_t>{4, 0}));
 
   Op floatingpoint_to_fp_ieee_bitvector_ot =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_ieee_bitvector_indices =
       floatingpoint_to_fp_ieee_bitvector_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
@@ -212,7 +214,7 @@ TEST_F(TestApiBlackOp, getIndicesPairUint)
                == std::pair<uint32_t, uint32_t>{4, 25}));
 
   Op floatingpoint_to_fp_floatingpoint_ot =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_floatingpoint_indices =
       floatingpoint_to_fp_floatingpoint_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
@@ -220,14 +222,14 @@ TEST_F(TestApiBlackOp, getIndicesPairUint)
                == std::pair<uint32_t, uint32_t>{4, 25}));
 
   Op floatingpoint_to_fp_real_ot =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_real_indices =
       floatingpoint_to_fp_real_ot.getIndices<std::pair<uint32_t, uint32_t>>();
   ASSERT_TRUE((floatingpoint_to_fp_real_indices
                == std::pair<uint32_t, uint32_t>{4, 25}));
 
   Op floatingpoint_to_fp_signed_bitvector_ot =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_signed_bitvector_indices =
       floatingpoint_to_fp_signed_bitvector_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();
@@ -235,7 +237,7 @@ TEST_F(TestApiBlackOp, getIndicesPairUint)
                == std::pair<uint32_t, uint32_t>{4, 25}));
 
   Op floatingpoint_to_fp_unsigned_bitvector_ot =
-      d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25);
+      d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 4, 25);
   std::pair<uint32_t, uint32_t> floatingpoint_to_fp_unsigned_bitvector_indices =
       floatingpoint_to_fp_unsigned_bitvector_ot
           .getIndices<std::pair<uint32_t, uint32_t>>();

diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java
index 2de478b580795f7dfd68712cff7cb9cda134dfd7..393f658c586f504e3222bef804997bb9fc5d921a 100644 (file)
--- a/test/unit/api/java/OpTest.java
+++ b/test/unit/api/java/OpTest.java
@@ -118,29 +118,27 @@ class OpTest
     assertArrayEquals(bitvector_extract_indices, new int[] {4, 0});
 
     Op floatingpoint_to_fp_ieee_bitvector_ot =
-        d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25);
+        d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_IEEE_BV, 4, 25);
     int[] floatingpoint_to_fp_ieee_bitvector_indices =
         floatingpoint_to_fp_ieee_bitvector_ot.getIntegerIndices();
     assertArrayEquals(floatingpoint_to_fp_ieee_bitvector_indices, new int[] {4, 25});
 
-    Op floatingpoint_to_fp_floatingpoint_ot =
-        d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25);
+    Op floatingpoint_to_fp_floatingpoint_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_FP, 4, 25);
     int[] floatingpoint_to_fp_floatingpoint_indices =
         floatingpoint_to_fp_floatingpoint_ot.getIntegerIndices();
     assertArrayEquals(floatingpoint_to_fp_floatingpoint_indices, new int[] {4, 25});
 
-    Op floatingpoint_to_fp_real_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25);
+    Op floatingpoint_to_fp_real_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_REAL, 4, 25);
     int[] floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIntegerIndices();
     assertArrayEquals(floatingpoint_to_fp_real_indices, new int[] {4, 25});
 
-    Op floatingpoint_to_fp_signed_bitvector_ot =
-        d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25);
+    Op floatingpoint_to_fp_signed_bitvector_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_SBV, 4, 25);
     int[] floatingpoint_to_fp_signed_bitvector_indices =
         floatingpoint_to_fp_signed_bitvector_ot.getIntegerIndices();
     assertArrayEquals(floatingpoint_to_fp_signed_bitvector_indices, new int[] {4, 25});
 
     Op floatingpoint_to_fp_unsigned_bitvector_ot =
-        d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25);
+        d_solver.mkOp(FLOATINGPOINT_TO_FP_FROM_UBV, 4, 25);
     int[] floatingpoint_to_fp_unsigned_bitvector_indices =
         floatingpoint_to_fp_unsigned_bitvector_ot.getIntegerIndices();
     assertArrayEquals(floatingpoint_to_fp_unsigned_bitvector_indices, new int[] {4, 25});

diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py
index 4059a4fb0670f718764fa30664392aa5a5f4fda8..141c9d4e24d90061689035c5ffc240f0339d65d0 100644 (file)
--- a/test/unit/api/python/test_op.py
+++ b/test/unit/api/python/test_op.py
@@ -57,13 +57,11 @@ def test_get_num_indices(solver):
     iand = solver.mkOp(Kind.Iand, 3)
     floatingpoint_to_ubv = solver.mkOp(Kind.FPToUbv, 11)
     floatingopint_to_sbv = solver.mkOp(Kind.FPToSbv, 13)
-    floatingpoint_to_fp_ieee_bitvector = solver.mkOp(Kind.FPToFpIeeeBV, 4, 25)
-    floatingpoint_to_fp_floatingpoint = solver.mkOp(Kind.FPToFpFP, 4, 25)
-    floatingpoint_to_fp_real = solver.mkOp(Kind.FPToFpReal, 4, 25)
-    floatingpoint_to_fp_signed_bitvector = solver.mkOp(Kind.FPToFpSignedBV, 4,
-                                                       25)
-    floatingpoint_to_fp_unsigned_bitvector = solver.mkOp(
-        Kind.FPToFpUnsignedBV, 4, 25)
+    floatingpoint_to_fp_from_ieee_bv = solver.mkOp(Kind.FPToFpFromIeeeBv, 4, 25)
+    floatingpoint_to_fp_from_fp = solver.mkOp(Kind.FPToFpFromFp, 4, 25)
+    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)
 
@@ -78,11 +76,11 @@ def test_get_num_indices(solver):
     assert 1 == iand.getNumIndices()
     assert 1 == floatingpoint_to_ubv.getNumIndices()
     assert 1 == floatingopint_to_sbv.getNumIndices()
-    assert 2 == floatingpoint_to_fp_ieee_bitvector.getNumIndices()
-    assert 2 == floatingpoint_to_fp_floatingpoint.getNumIndices()
-    assert 2 == floatingpoint_to_fp_real.getNumIndices()
-    assert 2 == floatingpoint_to_fp_signed_bitvector.getNumIndices()
-    assert 2 == floatingpoint_to_fp_unsigned_bitvector.getNumIndices()
+    assert 2 == floatingpoint_to_fp_from_ieee_bv.getNumIndices()
+    assert 2 == floatingpoint_to_fp_from_fp.getNumIndices()
+    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()
 
@@ -142,36 +140,35 @@ def test_get_indices_pair_uint(solver):
     bitvector_extract_indices = bitvector_extract_ot.getIndices()
     assert bitvector_extract_indices == (4, 0)
 
-    floatingpoint_to_fp_ieee_bitvector_ot = solver.mkOp(
-        Kind.FPToFpIeeeBV, 4, 25)
-    floatingpoint_to_fp_ieee_bitvector_indices = floatingpoint_to_fp_ieee_bitvector_ot.getIndices(
-    )
-    assert floatingpoint_to_fp_ieee_bitvector_indices == (4, 25)
-
-    floatingpoint_to_fp_floatingpoint_ot = solver.mkOp(Kind.FPToFpFP, 4, 25)
-    floatingpoint_to_fp_floatingpoint_indices = floatingpoint_to_fp_floatingpoint_ot.getIndices(
-    )
-    assert floatingpoint_to_fp_floatingpoint_indices == (4, 25)
-
-    floatingpoint_to_fp_real_ot = solver.mkOp(Kind.FPToFpReal, 4, 25)
-    floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIndices()
-    assert floatingpoint_to_fp_real_indices == (4, 25)
-
-    floatingpoint_to_fp_signed_bitvector_ot = solver.mkOp(
-        Kind.FPToFpSignedBV, 4, 25)
-    floatingpoint_to_fp_signed_bitvector_indices = floatingpoint_to_fp_signed_bitvector_ot.getIndices(
-    )
-    assert floatingpoint_to_fp_signed_bitvector_indices == (4, 25)
-
-    floatingpoint_to_fp_unsigned_bitvector_ot = solver.mkOp(
-        Kind.FPToFpUnsignedBV, 4, 25)
-    floatingpoint_to_fp_unsigned_bitvector_indices = floatingpoint_to_fp_unsigned_bitvector_ot.getIndices(
-    )
-    assert floatingpoint_to_fp_unsigned_bitvector_indices == (4, 25)
+    floatingpoint_to_fp_from_ieee_bv_ot = \
+            solver.mkOp(Kind.FPToFpFromIeeeBv, 4, 25)
+    floatingpoint_to_fp_from_ieee_bv_indices = \
+            floatingpoint_to_fp_from_ieee_bv_ot.getIndices()
+    assert floatingpoint_to_fp_from_ieee_bv_indices == (4, 25)
+
+    floatingpoint_to_fp_from_fp_ot = solver.mkOp(Kind.FPToFpFromFp, 4, 25)
+    floatingpoint_to_fp_from_fp_indices = \
+            floatingpoint_to_fp_from_fp_ot.getIndices()
+    assert floatingpoint_to_fp_from_fp_indices == (4, 25)
+
+    floatingpoint_to_fp_from_real_ot = solver.mkOp(Kind.FPToFpFromReal, 4, 25)
+    floatingpoint_to_fp_from_real_indices = \
+            floatingpoint_to_fp_from_real_ot.getIndices()
+    assert floatingpoint_to_fp_from_real_indices == (4, 25)
+
+    floatingpoint_to_fp_from_sbv_ot = solver.mkOp(Kind.FPToFpFromSbv, 4, 25)
+    floatingpoint_to_fp_from_sbv_indices = \
+            floatingpoint_to_fp_from_sbv_ot.getIndices()
+    assert floatingpoint_to_fp_from_sbv_indices == (4, 25)
+
+    floatingpoint_to_fp_from_ubv_ot = solver.mkOp(Kind.FPToFpFromUbv, 4, 25)
+    floatingpoint_to_fp_from_ubv_indices = \
+            floatingpoint_to_fp_from_ubv_ot.getIndices()
+    assert floatingpoint_to_fp_from_ubv_indices == (4, 25)
 
     floatingpoint_to_fp_generic_ot = solver.mkOp(Kind.FPToFpGeneric, 4, 25)
-    floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot.getIndices(
-    )
+    floatingpoint_to_fp_generic_indices = \
+            floatingpoint_to_fp_generic_ot.getIndices()
     assert floatingpoint_to_fp_generic_indices == (4, 25)