diff options
Diffstat (limited to 'test/unit/util')
-rw-r--r-- | test/unit/util/cardinality_public.h | 255 | ||||
-rw-r--r-- | test/unit/util/integer_black.h | 12 | ||||
-rw-r--r-- | test/unit/util/subrange_bound_white.h | 4 |
3 files changed, 269 insertions, 2 deletions
diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h new file mode 100644 index 000000000..5927e1bfa --- /dev/null +++ b/test/unit/util/cardinality_public.h @@ -0,0 +1,255 @@ +/********************* */ +/*! \file cardinality_public.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Public-box testing of CVC4::Cardinality + ** + ** Public-box testing of CVC4::Cardinality. + **/ + +#include "util/cardinality.h" +#include "util/integer.h" + +#include <string> +#include <sstream> + +using namespace CVC4; +using namespace std; + +class CardinalityPublic : public CxxTest::TestSuite { + stringstream ss; + +public: + + void testCardinalities() { + Cardinality zero(0); + Cardinality one(1); + Cardinality two(2); + + Cardinality invalid(0); + TS_ASSERT_THROWS( invalid = Cardinality(-1), IllegalArgumentException); + TS_ASSERT_THROWS( invalid = Cardinality(-2), IllegalArgumentException); + TS_ASSERT_THROWS( invalid = Cardinality(Integer("-3983982192391747295721957")), IllegalArgumentException); + invalid = one; // test assignment + invalid = Cardinality(5); // test assignment to temporary + + Cardinality copy(one); // test copy + Cardinality big(Integer("3983982192391747295721957")); + Cardinality r(Cardinality::REALS); + Cardinality i(Cardinality::INTEGERS); + + TS_ASSERT( zero < one ); + TS_ASSERT( one < two ); + TS_ASSERT( two < invalid ); + TS_ASSERT( invalid < big ); + TS_ASSERT( big < i ); + TS_ASSERT( i < r ); + + TS_ASSERT( zero <= one ); + TS_ASSERT( zero <= zero ); + TS_ASSERT( one <= two ); + TS_ASSERT( one <= one ); + TS_ASSERT( two <= invalid ); + TS_ASSERT( two <= two ); + TS_ASSERT( invalid <= big ); + TS_ASSERT( invalid <= invalid ); + TS_ASSERT( big <= i ); + TS_ASSERT( big <= big ); + TS_ASSERT( i <= r ); + TS_ASSERT( i <= i ); + TS_ASSERT( r <= r ); + + TS_ASSERT( zero == zero ); + TS_ASSERT( one == one ); + TS_ASSERT( two == two ); + TS_ASSERT( invalid == invalid ); + TS_ASSERT( copy == copy ); + TS_ASSERT( copy == one ); + TS_ASSERT( one == copy ); + TS_ASSERT( big == big ); + TS_ASSERT( i == i ); + TS_ASSERT( r == r ); + + TS_ASSERT( zero != one ); + TS_ASSERT( one != two ); + TS_ASSERT( two != invalid ); + TS_ASSERT( copy != r ); + TS_ASSERT( copy != i ); + TS_ASSERT( big != i ); + TS_ASSERT( i != big ); + TS_ASSERT( big != zero ); + TS_ASSERT( r != i ); + TS_ASSERT( i != r ); + + TS_ASSERT( r > zero ); + TS_ASSERT( r > one ); + TS_ASSERT( r > two ); + TS_ASSERT( r > copy ); + TS_ASSERT( r > invalid ); + TS_ASSERT( r > big ); + TS_ASSERT( r > i ); + TS_ASSERT( !( r > r ) ); + TS_ASSERT( r >= r ); + + TS_ASSERT( zero.isFinite() ); + TS_ASSERT( one.isFinite() ); + TS_ASSERT( two.isFinite() ); + TS_ASSERT( copy.isFinite() ); + TS_ASSERT( invalid.isFinite() ); + TS_ASSERT( big.isFinite() ); + TS_ASSERT( !i.isFinite() ); + TS_ASSERT( !r.isFinite() ); + + TS_ASSERT( zero.getFiniteCardinality() == 0 ); + TS_ASSERT( one.getFiniteCardinality() == 1 ); + TS_ASSERT( two.getFiniteCardinality() == 2 ); + TS_ASSERT( copy.getFiniteCardinality() == 1 ); + TS_ASSERT( invalid.getFiniteCardinality() == 5 ); + TS_ASSERT( big.getFiniteCardinality() == Integer("3983982192391747295721957") ); + TS_ASSERT_THROWS( i.getFiniteCardinality(), IllegalArgumentException ); + TS_ASSERT_THROWS( r.getFiniteCardinality(), IllegalArgumentException ); + + TS_ASSERT_THROWS( zero.getBethNumber(), IllegalArgumentException ); + TS_ASSERT_THROWS( one.getBethNumber(), IllegalArgumentException ); + TS_ASSERT_THROWS( two.getBethNumber(), IllegalArgumentException ); + TS_ASSERT_THROWS( copy.getBethNumber(), IllegalArgumentException ); + TS_ASSERT_THROWS( invalid.getBethNumber(), IllegalArgumentException ); + TS_ASSERT_THROWS( big.getBethNumber(), IllegalArgumentException ); + TS_ASSERT( i.getBethNumber() == 0 ); + TS_ASSERT( r.getBethNumber() == 1 ); + + TS_ASSERT( zero != Cardinality::INTEGERS ); + TS_ASSERT( one != Cardinality::INTEGERS ); + TS_ASSERT( two != Cardinality::INTEGERS ); + TS_ASSERT( copy != Cardinality::INTEGERS ); + TS_ASSERT( invalid != Cardinality::INTEGERS ); + TS_ASSERT( big != Cardinality::INTEGERS ); + TS_ASSERT( r != Cardinality::INTEGERS ); + TS_ASSERT( i == Cardinality::INTEGERS ); + + TS_ASSERT( zero != Cardinality::REALS ); + TS_ASSERT( one != Cardinality::REALS ); + TS_ASSERT( two != Cardinality::REALS ); + TS_ASSERT( copy != Cardinality::REALS ); + TS_ASSERT( invalid != Cardinality::REALS ); + TS_ASSERT( big != Cardinality::REALS ); + TS_ASSERT( i != Cardinality::REALS ); + TS_ASSERT( r == Cardinality::REALS ); + + // should work the other way too + + TS_ASSERT( Cardinality::INTEGERS != zero ); + TS_ASSERT( Cardinality::INTEGERS != one ); + TS_ASSERT( Cardinality::INTEGERS != two ); + TS_ASSERT( Cardinality::INTEGERS != copy ); + TS_ASSERT( Cardinality::INTEGERS != invalid ); + TS_ASSERT( Cardinality::INTEGERS != big ); + TS_ASSERT( Cardinality::INTEGERS != r ); + TS_ASSERT( Cardinality::INTEGERS == i ); + + TS_ASSERT( Cardinality::REALS != zero ); + TS_ASSERT( Cardinality::REALS != one ); + TS_ASSERT( Cardinality::REALS != two ); + TS_ASSERT( Cardinality::REALS != copy ); + TS_ASSERT( Cardinality::REALS != invalid ); + TS_ASSERT( Cardinality::REALS != big ); + TS_ASSERT( Cardinality::REALS != i ); + TS_ASSERT( Cardinality::REALS == r ); + + // finite cardinal arithmetic + + TS_ASSERT( zero + zero == zero ); + TS_ASSERT( zero * zero == zero ); + TS_ASSERT( (zero ^ zero) == one ); + TS_ASSERT( zero + one == one ); + TS_ASSERT( zero * one == zero ); + TS_ASSERT( (zero ^ one) == zero ); + TS_ASSERT( one + zero == one ); + TS_ASSERT( one * zero == zero ); + TS_ASSERT( (one ^ zero) == one ); + TS_ASSERT( two + two == 4 ); + TS_ASSERT( (two ^ two) == 4 ); + TS_ASSERT( two * two == 4 ); + TS_ASSERT( (two += two) == 4 ); + TS_ASSERT( two == 4 ); + TS_ASSERT( (two = 2) == 2 ); + TS_ASSERT( two == 2 ); + TS_ASSERT( (two *= 2) == 4 ); + TS_ASSERT( two == 4 ); + TS_ASSERT( ((two = 2) ^= 2) == 4 ); + TS_ASSERT( two == 4 ); + TS_ASSERT( (two = 2) == 2 ); + + // infinite cardinal arithmetic + + Cardinality x = i, y = Cardinality(2)^x, z = Cardinality(2)^y; + + TS_ASSERT( x == i && y == r ); + TS_ASSERT( x != r && y != i ); + TS_ASSERT( x != z && y != z ); + TS_ASSERT( x.isCountable() && !x.isFinite() ); + TS_ASSERT( !y.isCountable() && !y.isFinite() ); + TS_ASSERT( !z.isCountable() && !z.isFinite() ); + + TS_ASSERT( big < x ); + TS_ASSERT( x < y ); + TS_ASSERT( y < z ); + + TS_ASSERT_THROWS( big.getBethNumber(), IllegalArgumentException ); + TS_ASSERT( x.getBethNumber() == 0 ); + TS_ASSERT( y.getBethNumber() == 1 ); + TS_ASSERT( z.getBethNumber() == 2 ); + + TS_ASSERT( (zero ^ x) == zero ); + TS_ASSERT( (one ^ x) == one ); + TS_ASSERT( (two ^ x) == y && (two ^ x) != x ); + TS_ASSERT( (big ^ x) == y && (big ^ x) != x ); + TS_ASSERT( (two ^ x) == (big ^ x) ); + + TS_ASSERT( (x ^ zero) == one ); + TS_ASSERT( (x ^ one) == x ); + TS_ASSERT( (x ^ two) == x ); + TS_ASSERT( (x ^ big) == x ); + TS_ASSERT( (x ^ big) == (x ^ two) ); + + TS_ASSERT( (zero ^ y) == zero ); + TS_ASSERT( (one ^ y) == one ); + TS_ASSERT( (two ^ y) != x && (two ^ y) != y ); + TS_ASSERT( (big ^ y) != y && (big ^ y) != y ); + TS_ASSERT( (big ^ y).getBethNumber() == 2 ); + TS_ASSERT( (two ^ y) == (big ^ y) ); + + TS_ASSERT( (y ^ zero) == one ); + TS_ASSERT( (y ^ one) == y ); + TS_ASSERT( (y ^ two) == y ); + TS_ASSERT( (y ^ big) == y ); + TS_ASSERT( (y ^ big) == (y ^ two) ); + + TS_ASSERT( (x ^ x) == y ); + TS_ASSERT( (y ^ x) == y ); + TS_ASSERT( (x ^ y) == z ); + TS_ASSERT( (y ^ y) == z ); + TS_ASSERT( (z ^ x) == z ); + TS_ASSERT( (z ^ y) == z ); + TS_ASSERT( (zero ^ z) == 0 ); + TS_ASSERT( (z ^ zero) == 1 ); + TS_ASSERT( (z ^ 0) == 1 ); + TS_ASSERT( (two ^ z) > z ); + TS_ASSERT( (big ^ z) == (two ^ z) ); + TS_ASSERT( (x ^ z) == (two ^ z) ); + TS_ASSERT( (y ^ z) == (x ^ z) ); + TS_ASSERT( (z ^ z) == (x ^ z) ); + TS_ASSERT( (z ^ z).getBethNumber() == 3 ); + + }/* testCardinalities() */ + +};/* class CardinalityPublic */ diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h index f4bd1f8b8..66e29a01b 100644 --- a/test/unit/util/integer_black.h +++ b/test/unit/util/integer_black.h @@ -18,6 +18,7 @@ #include <cxxtest/TestSuite.h> #include <sstream> +#include <limits> #include "util/integer.h" @@ -295,6 +296,17 @@ public: TS_ASSERT_EQUALS( Integer(-1000), Integer(-10).pow(3) ); } + void testOverlyLong() { + unsigned long ul = numeric_limits<unsigned long>::max(); + Integer i(ul); + TS_ASSERT(i.getUnsignedLong() == ul); + TS_ASSERT_THROWS_ANYTHING(i.getLong()); + unsigned long ulplus1 = ul + 1; + TS_ASSERT(ulplus1 == 0); + i = i + 1; + TS_ASSERT_THROWS_ANYTHING(i.getUnsignedLong()); + } + void testTestBit() { TS_ASSERT( ! Integer(0).testBit(6) ); TS_ASSERT( ! Integer(0).testBit(5) ); diff --git a/test/unit/util/subrange_bound_white.h b/test/unit/util/subrange_bound_white.h index a41f75af9..d7587d679 100644 --- a/test/unit/util/subrange_bound_white.h +++ b/test/unit/util/subrange_bound_white.h @@ -11,9 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief White box testing of CVC4::SubrangeBound + ** \brief White-box testing of CVC4::SubrangeBound ** - ** White box testing of CVC4::SubrangeBound. + ** White-box testing of CVC4::SubrangeBound. **/ #include "util/subrange_bound.h" |