google test: util: Migrate real_algebraic_number_black. (#6028)

diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index d0160c855352e7726497fc402897a84de9e34220..e1a0e863b25eed51c87acebf879aaae9488a95f4 100644 (file)
--- 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 (file)
index 0000000..82cd6ca
--- /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 (file)
index fbe8065..0000000
--- 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)));
-  }
-};