From: Aina Niemetz Date: Mon, 1 Mar 2021 16:04:01 +0000 (-0800) Subject: google test: util: Migrate real_algebraic_number_black. (#6028) X-Git-Tag: cvc5-1.0.0~2181 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4e69b8bb9cb9787963036343e08030283515ccc5;p=cvc5.git google test: util: Migrate real_algebraic_number_black. (#6028) --- 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 - -#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))); - } -};