api: Rename mk<Value> functions for FP for consistency. (#8033)

diff --git a/examples/api/cpp/floating_point_arith.cpp b/examples/api/cpp/floating_point_arith.cpp
index 5c6c5a8a356e24aead97bb2787adb059896e06ea..1448f7d1f77e5a1dfe817251fcf35922dfcbfa7e 100644 (file)
--- a/examples/api/cpp/floating_point_arith.cpp
+++ b/examples/api/cpp/floating_point_arith.cpp
@@ -56,8 +56,8 @@ int main()
   cout << "c = " << solver.getValue(c) << endl;
 
   // Now, let's restrict `a` to be either NaN or positive infinity
-  Term nan = solver.mkNaN(8, 24);
-  Term inf = solver.mkPosInf(8, 24);
+  Term nan = solver.mkFloatingPointNaN(8, 24);
+  Term inf = solver.mkFloatingPointPosInf(8, 24);
   solver.assertFormula(solver.mkTerm(
       OR, solver.mkTerm(EQUAL, a, inf), solver.mkTerm(EQUAL, a, nan)));
 
@@ -91,7 +91,7 @@ int main()
 
   // For our final trick, let's try to find a floating-point number between
   // positive zero and the smallest positive floating-point number
-  Term zero = solver.mkPosZero(8, 24);
+  Term zero = solver.mkFloatingPointPosZero(8, 24);
   Term smallest = solver.mkFloatingPoint(8, 24, solver.mkBitVector(32, 0b001));
   solver.assertFormula(
       solver.mkTerm(AND,

diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java
index d8ed384d0feafa6fce2f6eafc6c376e665622ed1..7f601eee8148f4f9edab90347a1ea6c34f67695b 100644 (file)
--- a/examples/api/java/FloatingPointArith.java
+++ b/examples/api/java/FloatingPointArith.java
@@ -55,8 +55,8 @@ public class FloatingPointArith
       System.out.println("c = " + solver.getValue(c));
 
       // Now, let's restrict `a` to be either NaN or positive infinity
-      Term nan = solver.mkNaN(8, 24);
-      Term inf = solver.mkPosInf(8, 24);
+      Term nan = solver.mkFloatingPointNaN(8, 24);
+      Term inf = solver.mkFloatingPointPosInf(8, 24);
       solver.assertFormula(solver.mkTerm(
           Kind.OR, solver.mkTerm(Kind.EQUAL, a, inf), solver.mkTerm(Kind.EQUAL, a, nan)));
 
@@ -90,7 +90,7 @@ public class FloatingPointArith
 
       // For our final trick, let's try to find a floating-point number between
       // positive zero and the smallest positive floating-point number
-      Term zero = solver.mkPosZero(8, 24);
+      Term zero = solver.mkFloatingPointPosZero(8, 24);
       Term smallest = solver.mkFloatingPoint(8, 24, solver.mkBitVector(32, 0b001));
       solver.assertFormula(solver.mkTerm(Kind.AND,
           solver.mkTerm(Kind.FLOATINGPOINT_LT, zero, e),

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index df9a8b8ae5f92ded22c09cabd641314bfc779da9..2105ecca05363d2c03814450b0546a4b0d03adba 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6031,7 +6031,7 @@ Term Solver::mkConstArray(const Sort& sort, const Term& val) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
+Term Solver::mkFloatingPointPosInf(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
@@ -6041,7 +6041,7 @@ Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
+Term Solver::mkFloatingPointNegInf(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
@@ -6051,7 +6051,7 @@ Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
+Term Solver::mkFloatingPointNaN(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
@@ -6061,7 +6061,7 @@ Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
+Term Solver::mkFloatingPointPosZero(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
@@ -6071,7 +6071,7 @@ Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
   CVC5_API_TRY_CATCH_END;
 }
 
-Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
+Term Solver::mkFloatingPointNegZero(uint32_t exp, uint32_t sig) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 901bc9f64798478fadabfc0102da659bb1407172..bb67659df4acff25571d185c3ddd595eecd0aae7 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3647,7 +3647,7 @@ class CVC5_EXPORT Solver
    * @param sig Number of bits in the significand
    * @return the floating-point constant
    */
-  Term mkPosInf(uint32_t exp, uint32_t sig) const;
+  Term mkFloatingPointPosInf(uint32_t exp, uint32_t sig) const;
 
   /**
    * Create a negative infinity floating-point constant.
@@ -3655,7 +3655,7 @@ class CVC5_EXPORT Solver
    * @param sig Number of bits in the significand
    * @return the floating-point constant
    */
-  Term mkNegInf(uint32_t exp, uint32_t sig) const;
+  Term mkFloatingPointNegInf(uint32_t exp, uint32_t sig) const;
 
   /**
    * Create a not-a-number (NaN) floating-point constant.
@@ -3663,7 +3663,7 @@ class CVC5_EXPORT Solver
    * @param sig Number of bits in the significand
    * @return the floating-point constant
    */
-  Term mkNaN(uint32_t exp, uint32_t sig) const;
+  Term mkFloatingPointNaN(uint32_t exp, uint32_t sig) const;
 
   /**
    * Create a positive zero (+0.0) floating-point constant.
@@ -3671,7 +3671,7 @@ class CVC5_EXPORT Solver
    * @param sig Number of bits in the significand
    * @return the floating-point constant
    */
-  Term mkPosZero(uint32_t exp, uint32_t sig) const;
+  Term mkFloatingPointPosZero(uint32_t exp, uint32_t sig) const;
 
   /**
    * Create a negative zero (-0.0) floating-point constant.
@@ -3679,7 +3679,7 @@ class CVC5_EXPORT Solver
    * @param sig Number of bits in the significand
    * @return the floating-point constant
    */
-  Term mkNegZero(uint32_t exp, uint32_t sig) const;
+  Term mkFloatingPointNegZero(uint32_t exp, uint32_t sig) const;
 
   /**
    * Create a roundingmode constant.

diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 06b72dae4babe7cd389329ef9c201ce716cfdd70..2b32f18ceb57931ab8bdafd59fd107550f3e8961 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -1109,45 +1109,45 @@ public class Solver implements IPointer, AutoCloseable
    * @param sig Number of bits in the significand
    * @return the floating-point constant
    */
-  public Term mkPosInf(int exp, int sig) throws CVC5ApiException
+  public Term mkFloatingPointPosInf(int exp, int sig) throws CVC5ApiException
   {
     Utils.validateUnsigned(exp, "exp");
     Utils.validateUnsigned(sig, "sig");
-    long termPointer = mkPosInf(pointer, exp, sig);
+    long termPointer = mkFloatingPointPosInf(pointer, exp, sig);
     return new Term(this, termPointer);
   }
 
-  private native long mkPosInf(long pointer, int exp, int sig);
+  private native long mkFloatingPointPosInf(long pointer, int exp, int sig);
   /**
    * Create a negative infinity floating-point constant.
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
    */
-  public Term mkNegInf(int exp, int sig) throws CVC5ApiException
+  public Term mkFloatingPointNegInf(int exp, int sig) throws CVC5ApiException
   {
     Utils.validateUnsigned(exp, "exp");
     Utils.validateUnsigned(sig, "sig");
-    long termPointer = mkNegInf(pointer, exp, sig);
+    long termPointer = mkFloatingPointNegInf(pointer, exp, sig);
     return new Term(this, termPointer);
   }
 
-  private native long mkNegInf(long pointer, int exp, int sig);
+  private native long mkFloatingPointNegInf(long pointer, int exp, int sig);
   /**
    * Create a not-a-number (NaN) floating-point constant.
    * @param exp Number of bits in the exponent
    * @param sig Number of bits in the significand
    * @return the floating-point constant
    */
-  public Term mkNaN(int exp, int sig) throws CVC5ApiException
+  public Term mkFloatingPointNaN(int exp, int sig) throws CVC5ApiException
   {
     Utils.validateUnsigned(exp, "exp");
     Utils.validateUnsigned(sig, "sig");
-    long termPointer = mkNaN(pointer, exp, sig);
+    long termPointer = mkFloatingPointNaN(pointer, exp, sig);
     return new Term(this, termPointer);
   }
 
-  private native long mkNaN(long pointer, int exp, int sig);
+  private native long mkFloatingPointNaN(long pointer, int exp, int sig);
 
   /**
    * Create a positive zero (+0.0) floating-point constant.
@@ -1155,15 +1155,15 @@ public class Solver implements IPointer, AutoCloseable
    * @param sig Number of bits in the significand
    * @return the floating-point constant
    */
-  public Term mkPosZero(int exp, int sig) throws CVC5ApiException
+  public Term mkFloatingPointPosZero(int exp, int sig) throws CVC5ApiException
   {
     Utils.validateUnsigned(exp, "exp");
     Utils.validateUnsigned(sig, "sig");
-    long termPointer = mkPosZero(pointer, exp, sig);
+    long termPointer = mkFloatingPointPosZero(pointer, exp, sig);
     return new Term(this, termPointer);
   }
 
-  private native long mkPosZero(long pointer, int exp, int sig);
+  private native long mkFloatingPointPosZero(long pointer, int exp, int sig);
 
   /**
    * Create a negative zero (-0.0) floating-point constant.
@@ -1171,15 +1171,15 @@ public class Solver implements IPointer, AutoCloseable
    * @param sig Number of bits in the significand
    * @return the floating-point constant
    */
-  public Term mkNegZero(int exp, int sig) throws CVC5ApiException
+  public Term mkFloatingPointNegZero(int exp, int sig) throws CVC5ApiException
   {
     Utils.validateUnsigned(exp, "exp");
     Utils.validateUnsigned(sig, "sig");
-    long termPointer = mkNegZero(pointer, exp, sig);
+    long termPointer = mkFloatingPointNegZero(pointer, exp, sig);
     return new Term(this, termPointer);
   }
 
-  private native long mkNegZero(long pointer, int exp, int sig);
+  private native long mkFloatingPointNegZero(long pointer, int exp, int sig);
 
   /**
    * Create a roundingmode constant.

diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index f87ec6f491d5c43c6aedc74872d9097afa6cfc83..ec54b09b749e0686c5bb594939ebf8c1476d91fb 100644 (file)
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -1210,75 +1210,80 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkConstArray(
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    mkPosInf
+ * Method:    mkFloatingPointPosInf
  * Signature: (JII)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkPosInf(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFloatingPointPosInf(
     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* retPointer = new Term(solver->mkPosInf((uint32_t)exp, (uint32_t)sig));
+  Term* retPointer =
+      new Term(solver->mkFloatingPointPosInf((uint32_t)exp, (uint32_t)sig));
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    mkNegInf
+ * Method:    mkFloatingPointNegInf
  * Signature: (JII)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkNegInf(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFloatingPointNegInf(
     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* retPointer = new Term(solver->mkNegInf((uint32_t)exp, (uint32_t)sig));
+  Term* retPointer =
+      new Term(solver->mkFloatingPointNegInf((uint32_t)exp, (uint32_t)sig));
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    mkNaN
+ * Method:    mkFloatingPointNaN
  * Signature: (JII)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkNaN(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFloatingPointNaN(
     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* retPointer = new Term(solver->mkNaN((uint32_t)exp, (uint32_t)sig));
+  Term* retPointer =
+      new Term(solver->mkFloatingPointNaN((uint32_t)exp, (uint32_t)sig));
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    mkPosZero
+ * Method:    mkFloatingPointPosZero
  * Signature: (JII)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkPosZero(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFloatingPointPosZero(
     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* retPointer = new Term(solver->mkPosZero((uint32_t)exp, (uint32_t)sig));
+  Term* retPointer =
+      new Term(solver->mkFloatingPointPosZero((uint32_t)exp, (uint32_t)sig));
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     io_github_cvc5_api_Solver
- * Method:    mkNegZero
+ * Method:    mkFloatingPointNegZero
  * Signature: (JII)J
  */
-JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkNegZero(
+JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkFloatingPointNegZero(
     JNIEnv* env, jobject, jlong pointer, jint exp, jint sig)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
-  Term* retPointer = new Term(solver->mkNegZero((uint32_t)exp, (uint32_t)sig));
+  Term* retPointer =
+      new Term(solver->mkFloatingPointNegZero((uint32_t)exp, (uint32_t)sig));
   return reinterpret_cast<jlong>(retPointer);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 6518c61a44c79673104f78186ce01645e5364b3e..3d471817df9a8466969e51d69ce39178ccd2af5f 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -235,11 +235,11 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkBitVector(const string& s, uint32_t base) except +
         Term mkBitVector(uint32_t size, string& s, uint32_t base) except +
         Term mkConstArray(Sort sort, Term val) except +
-        Term mkPosInf(uint32_t exp, uint32_t sig) except +
-        Term mkNegInf(uint32_t exp, uint32_t sig) except +
-        Term mkNaN(uint32_t exp, uint32_t sig) except +
-        Term mkPosZero(uint32_t exp, uint32_t sig) except +
-        Term mkNegZero(uint32_t exp, uint32_t sig) except +
+        Term mkFloatingPointPosInf(uint32_t exp, uint32_t sig) except +
+        Term mkFloatingPointNegInf(uint32_t exp, uint32_t sig) except +
+        Term mkFloatingPointNaN(uint32_t exp, uint32_t sig) except +
+        Term mkFloatingPointPosZero(uint32_t exp, uint32_t sig) except +
+        Term mkFloatingPointNegZero(uint32_t exp, uint32_t sig) except +
         Term mkRoundingMode(RoundingMode rm) except +
         Term mkAbstractValue(const string& index) except +
         Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 10f697196b17ec71ee5c665ff027fbc35283c7f0..1754e821983e915d447c2ca7fcbdb80f7ba23635 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1325,7 +1325,7 @@ cdef class Solver:
         term.cterm = self.csolver.mkConstArray(sort.csort, val.cterm)
         return term
 
-    def mkPosInf(self, int exp, int sig):
+    def mkFloatingPointPosInf(self, int exp, int sig):
         """Create a positive infinity floating-point constant.
 
         :param exp: Number of bits in the exponent
@@ -1333,10 +1333,10 @@ cdef class Solver:
         :return: the floating-point constant
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.mkPosInf(exp, sig)
+        term.cterm = self.csolver.mkFloatingPointPosInf(exp, sig)
         return term
 
-    def mkNegInf(self, int exp, int sig):
+    def mkFloatingPointNegInf(self, int exp, int sig):
         """Create a negative infinity floating-point constant.
 
         :param exp: Number of bits in the exponent
@@ -1344,10 +1344,10 @@ cdef class Solver:
         :return: the floating-point constant
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.mkNegInf(exp, sig)
+        term.cterm = self.csolver.mkFloatingPointNegInf(exp, sig)
         return term
 
-    def mkNaN(self, int exp, int sig):
+    def mkFloatingPointNaN(self, int exp, int sig):
         """Create a not-a-number (NaN) floating-point constant.
 
         :param exp: Number of bits in the exponent
@@ -1355,10 +1355,10 @@ cdef class Solver:
         :return: the floating-point constant
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.mkNaN(exp, sig)
+        term.cterm = self.csolver.mkFloatingPointNaN(exp, sig)
         return term
 
-    def mkPosZero(self, int exp, int sig):
+    def mkFloatingPointPosZero(self, int exp, int sig):
         """Create a positive zero (+0.0) floating-point constant.
 
         :param exp: Number of bits in the exponent
@@ -1366,10 +1366,10 @@ cdef class Solver:
         :return: the floating-point constant
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.mkPosZero(exp, sig)
+        term.cterm = self.csolver.mkFloatingPointPosZero(exp, sig)
         return term
 
-    def mkNegZero(self, int exp, int sig):
+    def mkFloatingPointNegZero(self, int exp, int sig):
         """Create a negative zero (+0.0) floating-point constant.
 
         :param exp: Number of bits in the exponent
@@ -1377,7 +1377,7 @@ cdef class Solver:
         :return: the floating-point constant
         """
         cdef Term term = Term(self)
-        term.cterm = self.csolver.mkNegZero(exp, sig)
+        term.cterm = self.csolver.mkFloatingPointNegZero(exp, sig)
         return term
 
     def mkRoundingMode(self, RoundingMode rm):

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 0288040cc72557967406d514dc27cd5f550aab72..9dd21b148300a6154f44510867c45091507f1cf6 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -348,23 +348,23 @@ api::Term Smt2::mkIndexedConstant(const std::string& name,
   {
     if (name == "+oo")
     {
-      return d_solver->mkPosInf(numerals[0], numerals[1]);
+      return d_solver->mkFloatingPointPosInf(numerals[0], numerals[1]);
     }
     else if (name == "-oo")
     {
-      return d_solver->mkNegInf(numerals[0], numerals[1]);
+      return d_solver->mkFloatingPointNegInf(numerals[0], numerals[1]);
     }
     else if (name == "NaN")
     {
-      return d_solver->mkNaN(numerals[0], numerals[1]);
+      return d_solver->mkFloatingPointNaN(numerals[0], numerals[1]);
     }
     else if (name == "+zero")
     {
-      return d_solver->mkPosZero(numerals[0], numerals[1]);
+      return d_solver->mkFloatingPointPosZero(numerals[0], numerals[1]);
     }
     else if (name == "-zero")
     {
-      return d_solver->mkNegZero(numerals[0], numerals[1]);
+      return d_solver->mkFloatingPointNegZero(numerals[0], numerals[1]);
     }
   }
 

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 19a87f70937d6a7484e1364dc1e93a0c7f8f2dfe..f644c3367c096c6da302e175a5901db209f30ac4 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -518,26 +518,29 @@ TEST_F(TestApiBlackSolver, mkFalse)
   ASSERT_NO_THROW(d_solver.mkFalse());
 }
 
-TEST_F(TestApiBlackSolver, mkNaN) { ASSERT_NO_THROW(d_solver.mkNaN(3, 5)); }
+TEST_F(TestApiBlackSolver, mkFloatingPointNaN)
+{
+  ASSERT_NO_THROW(d_solver.mkFloatingPointNaN(3, 5));
+}
 
-TEST_F(TestApiBlackSolver, mkNegZero)
+TEST_F(TestApiBlackSolver, mkFloatingPointNegZero)
 {
-  ASSERT_NO_THROW(d_solver.mkNegZero(3, 5));
+  ASSERT_NO_THROW(d_solver.mkFloatingPointNegZero(3, 5));
 }
 
-TEST_F(TestApiBlackSolver, mkNegInf)
+TEST_F(TestApiBlackSolver, mkFloatingPointNegInf)
 {
-  ASSERT_NO_THROW(d_solver.mkNegInf(3, 5));
+  ASSERT_NO_THROW(d_solver.mkFloatingPointNegInf(3, 5));
 }
 
-TEST_F(TestApiBlackSolver, mkPosInf)
+TEST_F(TestApiBlackSolver, mkFloatingPointPosInf)
 {
-  ASSERT_NO_THROW(d_solver.mkPosInf(3, 5));
+  ASSERT_NO_THROW(d_solver.mkFloatingPointPosInf(3, 5));
 }
 
-TEST_F(TestApiBlackSolver, mkPosZero)
+TEST_F(TestApiBlackSolver, mkFloatingPointPosZero)
 {
-  ASSERT_NO_THROW(d_solver.mkPosZero(3, 5));
+  ASSERT_NO_THROW(d_solver.mkFloatingPointPosZero(3, 5));
 }
 
 TEST_F(TestApiBlackSolver, mkOp)

diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp
index 975cd7d79d6b4bb210695bba61e761113b1d2040..c3f418dc4faa2e14592970dc9a6a5eff6ec1b1b8 100644 (file)
--- a/test/unit/api/cpp/term_black.cpp
+++ b/test/unit/api/cpp/term_black.cpp
@@ -947,11 +947,11 @@ TEST_F(TestApiBlackTerm, getFloatingPoint)
   ASSERT_FALSE(fp.isFloatingPointNaN());
   ASSERT_EQ(std::make_tuple(5u, 11u, bvval), fp.getFloatingPointValue());
 
-  ASSERT_TRUE(d_solver.mkPosZero(5, 11).isFloatingPointPosZero());
-  ASSERT_TRUE(d_solver.mkNegZero(5, 11).isFloatingPointNegZero());
-  ASSERT_TRUE(d_solver.mkPosInf(5, 11).isFloatingPointPosInf());
-  ASSERT_TRUE(d_solver.mkNegInf(5, 11).isFloatingPointNegInf());
-  ASSERT_TRUE(d_solver.mkNaN(5, 11).isFloatingPointNaN());
+  ASSERT_TRUE(d_solver.mkFloatingPointPosZero(5, 11).isFloatingPointPosZero());
+  ASSERT_TRUE(d_solver.mkFloatingPointNegZero(5, 11).isFloatingPointNegZero());
+  ASSERT_TRUE(d_solver.mkFloatingPointPosInf(5, 11).isFloatingPointPosInf());
+  ASSERT_TRUE(d_solver.mkFloatingPointNegInf(5, 11).isFloatingPointNegInf());
+  ASSERT_TRUE(d_solver.mkFloatingPointNaN(5, 11).isFloatingPointNaN());
 }
 
 TEST_F(TestApiBlackTerm, getSet)

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index c4733209280d6a81f132582cd933ce1c76175718..29efbea400dcda050e1dc8d1274f2ac5393adc77 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -503,29 +503,29 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkFalse());
   }
 
-  @Test void mkNaN() throws CVC5ApiException
+  @Test void mkFloatingPointNaN() throws CVC5ApiException
   {
-    assertDoesNotThrow(() -> d_solver.mkNaN(3, 5));
+    assertDoesNotThrow(() -> d_solver.mkFloatingPointNaN(3, 5));
   }
 
-  @Test void mkNegZero() throws CVC5ApiException
+  @Test void mkFloatingPointNegZero() throws CVC5ApiException
   {
-    assertDoesNotThrow(() -> d_solver.mkNegZero(3, 5));
+    assertDoesNotThrow(() -> d_solver.mkFloatingPointNegZero(3, 5));
   }
 
-  @Test void mkNegInf()
+  @Test void mkFloatingPointNegInf()
   {
-    assertDoesNotThrow(() -> d_solver.mkNegInf(3, 5));
+    assertDoesNotThrow(() -> d_solver.mkFloatingPointNegInf(3, 5));
   }
 
-  @Test void mkPosInf()
+  @Test void mkFloatingPointPosInf()
   {
-    assertDoesNotThrow(() -> d_solver.mkPosInf(3, 5));
+    assertDoesNotThrow(() -> d_solver.mkFloatingPointPosInf(3, 5));
   }
 
-  @Test void mkPosZero()
+  @Test void mkFloatingPointPosZero()
   {
-    assertDoesNotThrow(() -> d_solver.mkPosZero(3, 5));
+    assertDoesNotThrow(() -> d_solver.mkFloatingPointPosZero(3, 5));
   }
 
   @Test void mkOp()

diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java
index 684aa1ec729b7a161b5f8295479bee92c48f6527..6783781de3dce4c87ffd00a286a81fa519b33e1e 100644 (file)
--- a/test/unit/api/java/TermTest.java
+++ b/test/unit/api/java/TermTest.java
@@ -899,11 +899,11 @@ class TermTest
     assertFalse(fp.isFloatingPointNaN());
     assertEquals(new Triplet<Long, Long, Term>(5L, 11L, bvval), fp.getFloatingPointValue());
 
-    assertTrue(d_solver.mkPosZero(5, 11).isFloatingPointPosZero());
-    assertTrue(d_solver.mkNegZero(5, 11).isFloatingPointNegZero());
-    assertTrue(d_solver.mkPosInf(5, 11).isFloatingPointPosInf());
-    assertTrue(d_solver.mkNegInf(5, 11).isFloatingPointNegInf());
-    assertTrue(d_solver.mkNaN(5, 11).isFloatingPointNaN());
+    assertTrue(d_solver.mkFloatingPointPosZero(5, 11).isFloatingPointPosZero());
+    assertTrue(d_solver.mkFloatingPointNegZero(5, 11).isFloatingPointNegZero());
+    assertTrue(d_solver.mkFloatingPointPosInf(5, 11).isFloatingPointPosInf());
+    assertTrue(d_solver.mkFloatingPointNegInf(5, 11).isFloatingPointNegInf());
+    assertTrue(d_solver.mkFloatingPointNaN(5, 11).isFloatingPointNaN());
   }
 
   @Test void getSet()

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 7d3504501c69bbf08c22a43e91dfa97c7d642f28..f801245c1b643e7e6508ffde8dd21e72df4bc09e 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -481,24 +481,24 @@ def test_mk_false(solver):
     solver.mkFalse()
 
 
-def test_mk_nan(solver):
-    solver.mkNaN(3, 5)
+def test_mk_floating_point_nan(solver):
+    solver.mkFloatingPointNaN(3, 5)
 
 
-def test_mk_neg_zero(solver):
-    solver.mkNegZero(3, 5)
+def test_mk_floating_point_neg_zero(solver):
+    solver.mkFloatingPointNegZero(3, 5)
 
 
-def test_mk_neg_inf(solver):
-    solver.mkNegInf(3, 5)
+def test_mk_floating_point_neg_inf(solver):
+    solver.mkFloatingPointNegInf(3, 5)
 
 
-def test_mk_pos_inf(solver):
-    solver.mkPosInf(3, 5)
+def test_mk_floating_point_pos_inf(solver):
+    solver.mkFloatingPointPosInf(3, 5)
 
 
-def test_mk_pos_zero(solver):
-    solver.mkPosZero(3, 5)
+def test_mk_floating_point_pos_zero(solver):
+    solver.mkFloatingPointPosZero(3, 5)
 
 
 def test_mk_op(solver):

diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py
index b810f35b4581c0a1e29fd9958227decae5fb40de..b24bb3375c1cce5f04c4bb5abdc883d4e8c6292b 100644 (file)
--- a/test/unit/api/python/test_term.py
+++ b/test/unit/api/python/test_term.py
@@ -1058,11 +1058,11 @@ def test_get_floating_point(solver):
     assert not fp.isFloatingPointNaN()
     assert (5, 11, bvval) == fp.getFloatingPointValue()
 
-    assert solver.mkPosZero(5, 11).isFloatingPointPosZero()
-    assert solver.mkNegZero(5, 11).isFloatingPointNegZero()
-    assert solver.mkPosInf(5, 11).isFloatingPointPosInf()
-    assert solver.mkNegInf(5, 11).isFloatingPointNegInf()
-    assert solver.mkNaN(5, 11).isFloatingPointNaN()
+    assert solver.mkFloatingPointPosZero(5, 11).isFloatingPointPosZero()
+    assert solver.mkFloatingPointNegZero(5, 11).isFloatingPointNegZero()
+    assert solver.mkFloatingPointPosInf(5, 11).isFloatingPointPosInf()
+    assert solver.mkFloatingPointNegInf(5, 11).isFloatingPointNegInf()
+    assert solver.mkFloatingPointNaN(5, 11).isFloatingPointNaN()
 
 
 def test_is_integer(solver):