From 5b458eceb66a44f176133b4eaaf2bc8ab19ee918 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 2 Feb 2022 12:59:37 -0800 Subject: [PATCH] api: Rename mk functions for FP for consistency. (#8033) --- examples/api/cpp/floating_point_arith.cpp | 6 ++-- examples/api/java/FloatingPointArith.java | 6 ++-- src/api/cpp/cvc5.cpp | 10 +++--- src/api/cpp/cvc5.h | 10 +++--- src/api/java/io/github/cvc5/api/Solver.java | 30 +++++++++--------- src/api/java/jni/solver.cpp | 35 ++++++++++++--------- src/api/python/cvc5.pxd | 10 +++--- src/api/python/cvc5.pxi | 20 ++++++------ src/parser/smt2/smt2.cpp | 10 +++--- test/unit/api/cpp/solver_black.cpp | 21 +++++++------ test/unit/api/cpp/term_black.cpp | 10 +++--- test/unit/api/java/SolverTest.java | 20 ++++++------ test/unit/api/java/TermTest.java | 10 +++--- test/unit/api/python/test_solver.py | 20 ++++++------ test/unit/api/python/test_term.py | 10 +++--- 15 files changed, 118 insertions(+), 110 deletions(-) diff --git a/examples/api/cpp/floating_point_arith.cpp b/examples/api/cpp/floating_point_arith.cpp index 5c6c5a8a3..1448f7d1f 100644 --- 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 d8ed384d0..7f601eee8 100644 --- 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 df9a8b8ae..2105ecca0 100644 --- 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 901bc9f64..bb67659df 100644 --- 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 06b72dae4..2b32f18ce 100644 --- 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 f87ec6f49..ec54b09b7 100644 --- 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(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(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(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(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(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(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(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(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(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(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 6518c61a4..3d471817d 100644 --- 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 10f697196..1754e8219 100644 --- 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 0288040cc..9dd21b148 100644 --- 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 19a87f709..f644c3367 100644 --- 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 975cd7d79..c3f418dc4 100644 --- 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 c47332092..29efbea40 100644 --- 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 684aa1ec7..6783781de 100644 --- 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(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 7d3504501..f801245c1 100644 --- 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 b810f35b4..b24bb3375 100644 --- 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): -- 2.30.2