diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 2 | ||||
-rw-r--r-- | test/unit/expr/type_cardinality_public.h | 223 | ||||
-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 |
5 files changed, 494 insertions, 2 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 13d28f3bb..f50cc32db 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -19,6 +19,7 @@ UNIT_TESTS = \ expr/attribute_black \ expr/declaration_scope_black \ expr/node_self_iterator_black \ + expr/type_cardinality_public \ parser/parser_black \ parser/parser_builder_black \ prop/cnf_stream_black \ @@ -46,6 +47,7 @@ UNIT_TESTS = \ util/trans_closure_black \ util/boolean_simplification_black \ util/subrange_bound_white \ + util/cardinality_public \ main/interactive_shell_black export VERBOSE = 1 diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h new file mode 100644 index 000000000..381d5fdea --- /dev/null +++ b/test/unit/expr/type_cardinality_public.h @@ -0,0 +1,223 @@ +/********************* */ +/*! \file type_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 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 Type::getCardinality() for various Types + ** + ** Public box testing of Type::getCardinality() for various Types. + **/ + +#include <cxxtest/TestSuite.h> + +#include <iostream> +#include <string> +#include <sstream> + +#include "expr/kind.h" +#include "expr/type.h" +#include "expr/expr_manager.h" +#include "util/cardinality.h" +#include "util/Assert.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace std; + +class TypeCardinalityPublic : public CxxTest::TestSuite { + ExprManager* d_em; + +public: + + void setUp() { + d_em = new ExprManager(); + } + + void tearDown() { + delete d_em; + } + + void testTheBasics() { + TS_ASSERT( d_em->booleanType().getCardinality() == 2 ); + TS_ASSERT( d_em->integerType().getCardinality() == Cardinality::INTEGERS ); + TS_ASSERT( d_em->realType().getCardinality() == Cardinality::REALS ); + } + + void testArrays() { + Type intToInt = d_em->mkArrayType(d_em->integerType(), d_em->integerType()); + Type realToReal = d_em->mkArrayType(d_em->realType(), d_em->realType()); + Type realToInt = d_em->mkArrayType(d_em->realType(), d_em->integerType()); + Type intToReal = d_em->mkArrayType(d_em->integerType(), d_em->realType()); + Type intToBool = d_em->mkArrayType(d_em->integerType(), d_em->booleanType()); + Type realToBool = d_em->mkArrayType(d_em->realType(), d_em->booleanType()); + Type boolToReal = d_em->mkArrayType(d_em->booleanType(), d_em->realType()); + Type boolToInt = d_em->mkArrayType(d_em->booleanType(), d_em->integerType()); + Type boolToBool = d_em->mkArrayType(d_em->booleanType(), d_em->booleanType()); + + TS_ASSERT( intToInt.getCardinality() == Cardinality::REALS ); + TS_ASSERT( realToReal.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( intToReal.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intToBool.getCardinality() == Cardinality::REALS ); + TS_ASSERT( realToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( boolToReal.getCardinality() == Cardinality::REALS ); + TS_ASSERT( boolToInt.getCardinality() == Cardinality::INTEGERS ); + TS_ASSERT( boolToBool.getCardinality() == 4 ); + } + + void testUnaryFunctions() { + Type intToInt = d_em->mkFunctionType(d_em->integerType(), d_em->integerType()); + Type realToReal = d_em->mkFunctionType(d_em->realType(), d_em->realType()); + Type realToInt = d_em->mkFunctionType(d_em->realType(), d_em->integerType()); + Type intToReal = d_em->mkFunctionType(d_em->integerType(), d_em->realType()); + Type intToBool = d_em->mkFunctionType(d_em->integerType(), d_em->booleanType()); + Type realToBool = d_em->mkFunctionType(d_em->realType(), d_em->booleanType()); + Type boolToReal = d_em->mkFunctionType(d_em->booleanType(), d_em->realType()); + Type boolToInt = d_em->mkFunctionType(d_em->booleanType(), d_em->integerType()); + Type boolToBool = d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()); + + TS_ASSERT( intToInt.getCardinality() == Cardinality::REALS ); + TS_ASSERT( realToReal.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( intToReal.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intToBool.getCardinality() == Cardinality::REALS ); + TS_ASSERT( realToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( boolToReal.getCardinality() == Cardinality::REALS ); + TS_ASSERT( boolToInt.getCardinality() == Cardinality::INTEGERS ); + TS_ASSERT( boolToBool.getCardinality() == 4 ); + } + + void testBinaryFunctions() { + vector<Type> boolbool; boolbool.push_back(d_em->booleanType()); boolbool.push_back(d_em->booleanType()); + vector<Type> boolint; boolint.push_back(d_em->booleanType()); boolint.push_back(d_em->integerType()); + vector<Type> intbool; intbool.push_back(d_em->integerType()); intbool.push_back(d_em->booleanType()); + vector<Type> intint; intint.push_back(d_em->integerType()); intint.push_back(d_em->integerType()); + vector<Type> intreal; intreal.push_back(d_em->integerType()); intreal.push_back(d_em->realType()); + vector<Type> realint; realint.push_back(d_em->realType()); realint.push_back(d_em->integerType()); + vector<Type> realreal; realreal.push_back(d_em->realType()); realreal.push_back(d_em->realType()); + vector<Type> realbool; realbool.push_back(d_em->realType()); realbool.push_back(d_em->booleanType()); + vector<Type> boolreal; boolreal.push_back(d_em->booleanType()); boolreal.push_back(d_em->realType()); + + Type boolboolToBool = d_em->mkFunctionType(boolbool, d_em->booleanType()); + Type boolboolToInt = d_em->mkFunctionType(boolbool, d_em->integerType()); + Type boolboolToReal = d_em->mkFunctionType(boolbool, d_em->realType()); + + Type boolintToBool = d_em->mkFunctionType(boolint, d_em->booleanType()); + Type boolintToInt = d_em->mkFunctionType(boolint, d_em->integerType()); + Type boolintToReal = d_em->mkFunctionType(boolint, d_em->realType()); + + Type intboolToBool = d_em->mkFunctionType(intbool, d_em->booleanType()); + Type intboolToInt = d_em->mkFunctionType(intbool, d_em->integerType()); + Type intboolToReal = d_em->mkFunctionType(intbool, d_em->realType()); + + Type intintToBool = d_em->mkFunctionType(intint, d_em->booleanType()); + Type intintToInt = d_em->mkFunctionType(intint, d_em->integerType()); + Type intintToReal = d_em->mkFunctionType(intint, d_em->realType()); + + Type intrealToBool = d_em->mkFunctionType(intreal, d_em->booleanType()); + Type intrealToInt = d_em->mkFunctionType(intreal, d_em->integerType()); + Type intrealToReal = d_em->mkFunctionType(intreal, d_em->realType()); + + Type realintToBool = d_em->mkFunctionType(realint, d_em->booleanType()); + Type realintToInt = d_em->mkFunctionType(realint, d_em->integerType()); + Type realintToReal = d_em->mkFunctionType(realint, d_em->realType()); + + Type realrealToBool = d_em->mkFunctionType(realreal, d_em->booleanType()); + Type realrealToInt = d_em->mkFunctionType(realreal, d_em->integerType()); + Type realrealToReal = d_em->mkFunctionType(realreal, d_em->realType()); + + Type realboolToBool = d_em->mkFunctionType(realbool, d_em->booleanType()); + Type realboolToInt = d_em->mkFunctionType(realbool, d_em->integerType()); + Type realboolToReal = d_em->mkFunctionType(realbool, d_em->realType()); + + Type boolrealToBool = d_em->mkFunctionType(boolreal, d_em->booleanType()); + Type boolrealToInt = d_em->mkFunctionType(boolreal, d_em->integerType()); + Type boolrealToReal = d_em->mkFunctionType(boolreal, d_em->realType()); + + TS_ASSERT( boolboolToBool.getCardinality() == 16 ); + TS_ASSERT( boolboolToInt.getCardinality() == Cardinality::INTEGERS ); + TS_ASSERT( boolboolToReal.getCardinality() == Cardinality::REALS ); + + TS_ASSERT( boolintToBool.getCardinality() == Cardinality::REALS ); + TS_ASSERT( boolintToInt.getCardinality() == Cardinality::REALS ); + TS_ASSERT( boolintToReal.getCardinality() == Cardinality::REALS ); + + TS_ASSERT( intboolToBool.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intboolToInt.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intboolToReal.getCardinality() == Cardinality::REALS ); + + TS_ASSERT( intintToBool.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intintToInt.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intintToReal.getCardinality() == Cardinality::REALS ); + + TS_ASSERT( intrealToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( intrealToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( intrealToReal.getCardinality() > Cardinality::REALS ); + + TS_ASSERT( realintToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realintToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realintToReal.getCardinality() > Cardinality::REALS ); + + TS_ASSERT( realrealToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realrealToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realrealToReal.getCardinality() > Cardinality::REALS ); + + TS_ASSERT( realboolToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realboolToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realboolToReal.getCardinality() > Cardinality::REALS ); + + TS_ASSERT( boolrealToBool.getCardinality() > Cardinality::REALS ); + TS_ASSERT( boolrealToInt.getCardinality() > Cardinality::REALS ); + TS_ASSERT( boolrealToReal.getCardinality() > Cardinality::REALS ); + } + + void testTernaryFunctions() { + vector<Type> boolbool; boolbool.push_back(d_em->booleanType()); boolbool.push_back(d_em->booleanType()); + vector<Type> boolboolbool = boolbool; boolboolbool.push_back(d_em->booleanType()); + + Type boolboolTuple = d_em->mkTupleType(boolbool); + Type boolboolboolTuple = d_em->mkTupleType(boolboolbool); + + Type boolboolboolToBool = d_em->mkFunctionType(boolboolbool, d_em->booleanType()); + Type boolboolToBoolbool = d_em->mkFunctionType(boolbool, boolboolTuple); + Type boolToBoolboolbool = d_em->mkFunctionType(d_em->booleanType(), boolboolboolTuple); + + TS_ASSERT( boolboolboolToBool.getCardinality() == /* 2 ^ 8 */ 1 << 8 ); + TS_ASSERT( boolboolToBoolbool.getCardinality() == /* 4 ^ 4 */ 4 * 4 * 4 * 4 ); + TS_ASSERT( boolToBoolboolbool.getCardinality() == /* 8 ^ 2 */ 8 * 8 ); + } + + void testUndefinedSorts() { + Type foo = d_em->mkSort("foo"); + // We've currently assigned them a specific Beth number, which + // isn't really correct, but... + TS_ASSERT( !foo.getCardinality().isFinite() ); + } + + void testBitvectors() { + Debug.on("bvcard"); + TS_ASSERT( d_em->mkBitVectorType(0).getCardinality() == 0 ); + for(unsigned i = 1; i < 128; ++i) { + try { + Cardinality card = Cardinality(2) ^ i; + if( d_em->mkBitVectorType(i).getCardinality() != card ) { + stringstream ss; + ss << "test failed for bitvector(" << i << ")"; + TS_FAIL(ss.str().c_str()); + } + } catch(Exception& e) { + cout << endl << e << endl; + throw; + } + } + } + +};/* TypeCardinalityPublic */ 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" |