diff options
Diffstat (limited to 'test/unit/util/cardinality_public.h')
| -rw-r--r-- | test/unit/util/cardinality_public.h | 255 |
1 files changed, 255 insertions, 0 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 */ |