summaryrefslogtreecommitdiff
path: root/test/unit/util
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2021-03-01 08:04:01 -0800
committerGitHub <noreply@github.com>2021-03-01 16:04:01 +0000
commit4e69b8bb9cb9787963036343e08030283515ccc5 (patch)
tree190c523d8fd1cee26e63406b8b9f19bb9543613a /test/unit/util
parent9628b9591044d167544cd195d51fe7a7709f3acb (diff)
google test: util: Migrate real_algebraic_number_black. (#6028)
Diffstat (limited to 'test/unit/util')
-rw-r--r--test/unit/util/CMakeLists.txt2
-rw-r--r--test/unit/util/real_algebraic_number_black.cpp84
-rw-r--r--test/unit/util/real_algebraic_number_black.h83
3 files changed, 85 insertions, 84 deletions
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index d0160c855..e1a0e863b 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -30,6 +30,6 @@ cvc4_add_unit_test_black(output_black util)
cvc4_add_unit_test_black(rational_black util)
cvc4_add_unit_test_white(rational_white util)
if(CVC4_USE_POLY_IMP)
-cvc4_add_cxx_unit_test_black(real_algebraic_number_black util)
+cvc4_add_unit_test_black(real_algebraic_number_black util)
endif()
cvc4_add_cxx_unit_test_black(stats_black util)
diff --git a/test/unit/util/real_algebraic_number_black.cpp b/test/unit/util/real_algebraic_number_black.cpp
new file mode 100644
index 000000000..82cd6caf3
--- /dev/null
+++ b/test/unit/util/real_algebraic_number_black.cpp
@@ -0,0 +1,84 @@
+/********************* */
+/*! \file real_algebraic_number_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz, Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::RealAlgebraicNumber.
+ **
+ ** Black box testing of CVC4::RealAlgebraicNumber.
+ **/
+
+#include "test.h"
+#include "util/real_algebraic_number.h"
+
+namespace CVC4 {
+namespace test {
+
+#ifndef CVC4_POLY_IMP
+#error "This unit test should only be enabled for CVC4_POLY_IMP"
+#endif
+
+class TestUtilBlackRealAlgebraicNumber : public TestInternal
+{
+};
+
+TEST_F(TestUtilBlackRealAlgebraicNumber, creation)
+{
+ ASSERT_TRUE(isZero(RealAlgebraicNumber()));
+ ASSERT_TRUE(isOne(RealAlgebraicNumber(Integer(1))));
+ ASSERT_FALSE(isOne(RealAlgebraicNumber(Rational(2))));
+ RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
+ ASSERT_TRUE(RealAlgebraicNumber(Integer(1)) < sqrt2);
+ ASSERT_TRUE(sqrt2 < RealAlgebraicNumber(Integer(2)));
+}
+
+TEST_F(TestUtilBlackRealAlgebraicNumber, comprison)
+{
+ RealAlgebraicNumber msqrt3({-3, 0, 1}, -2, -1);
+ RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1);
+ RealAlgebraicNumber zero;
+ RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
+ RealAlgebraicNumber sqrt3({-3, 0, 1}, 1, 2);
+
+ ASSERT_TRUE(msqrt3 < msqrt2);
+ ASSERT_TRUE(msqrt3 < zero);
+ ASSERT_TRUE(msqrt3 < sqrt2);
+ ASSERT_TRUE(msqrt3 < sqrt3);
+ ASSERT_TRUE(msqrt2 < zero);
+ ASSERT_TRUE(msqrt2 < sqrt2);
+ ASSERT_TRUE(msqrt2 < sqrt3);
+ ASSERT_TRUE(zero < sqrt2);
+ ASSERT_TRUE(zero < sqrt3);
+ ASSERT_TRUE(sqrt2 < sqrt3);
+}
+
+TEST_F(TestUtilBlackRealAlgebraicNumber, sgn)
+{
+ RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1);
+ RealAlgebraicNumber zero;
+ RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
+
+ ASSERT_EQ(sgn(msqrt2), -1);
+ ASSERT_EQ(sgn(zero), 0);
+ ASSERT_EQ(sgn(sqrt2), 1);
+}
+
+TEST_F(TestUtilBlackRealAlgebraicNumber, arithmetic)
+{
+ RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1);
+ RealAlgebraicNumber zero;
+ RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
+
+ ASSERT_EQ(msqrt2 + sqrt2, zero);
+ ASSERT_EQ(-msqrt2, sqrt2);
+ ASSERT_EQ(-msqrt2 + sqrt2, sqrt2 + sqrt2);
+ ASSERT_EQ(msqrt2 * sqrt2, RealAlgebraicNumber(Integer(-2)));
+}
+} // namespace test
+} // namespace CVC4
diff --git a/test/unit/util/real_algebraic_number_black.h b/test/unit/util/real_algebraic_number_black.h
deleted file mode 100644
index fbe8065a9..000000000
--- a/test/unit/util/real_algebraic_number_black.h
+++ /dev/null
@@ -1,83 +0,0 @@
-/********************* */
-/*! \file real_algebraic_number_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Gereon Kremer
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::RealAlgebraicNumber.
- **
- ** Black box testing of CVC4::RealAlgebraicNumber.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "util/real_algebraic_number.h"
-
-using namespace CVC4;
-using namespace std;
-
-#ifndef CVC4_POLY_IMP
-#error "This unit test should only be enabled for CVC4_POLY_IMP"
-#endif
-
-class RealAlgebraicNumberBlack : public CxxTest::TestSuite
-{
- public:
- void testCreation()
- {
- TS_ASSERT(isZero(RealAlgebraicNumber()));
- TS_ASSERT(isOne(RealAlgebraicNumber(Integer(1))));
- TS_ASSERT(!isOne(RealAlgebraicNumber(Rational(2))));
- RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
- TS_ASSERT(RealAlgebraicNumber(Integer(1)) < sqrt2);
- TS_ASSERT(sqrt2 < RealAlgebraicNumber(Integer(2)));
- }
-
- void testComparison()
- {
- RealAlgebraicNumber msqrt3({-3, 0, 1}, -2, -1);
- RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1);
- RealAlgebraicNumber zero;
- RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
- RealAlgebraicNumber sqrt3({-3, 0, 1}, 1, 2);
-
- TS_ASSERT(msqrt3 < msqrt2);
- TS_ASSERT(msqrt3 < zero);
- TS_ASSERT(msqrt3 < sqrt2);
- TS_ASSERT(msqrt3 < sqrt3);
- TS_ASSERT(msqrt2 < zero);
- TS_ASSERT(msqrt2 < sqrt2);
- TS_ASSERT(msqrt2 < sqrt3);
- TS_ASSERT(zero < sqrt2);
- TS_ASSERT(zero < sqrt3);
- TS_ASSERT(sqrt2 < sqrt3);
- }
-
- void testSgn()
- {
- RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1);
- RealAlgebraicNumber zero;
- RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
-
- TS_ASSERT_EQUALS(sgn(msqrt2), -1);
- TS_ASSERT_EQUALS(sgn(zero), 0);
- TS_ASSERT_EQUALS(sgn(sqrt2), 1);
- }
-
- void testArithmetic()
- {
- RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1);
- RealAlgebraicNumber zero;
- RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
-
- TS_ASSERT_EQUALS(msqrt2 + sqrt2, zero);
- TS_ASSERT_EQUALS(-msqrt2, sqrt2);
- TS_ASSERT_EQUALS(-msqrt2 + sqrt2, sqrt2 + sqrt2);
- TS_ASSERT_EQUALS(msqrt2 * sqrt2, RealAlgebraicNumber(Integer(-2)));
- }
-};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback