From 3dff1d2eef828dc3ff17750a738d6a6bff0ed484 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 22 Aug 2012 22:31:59 +0000 Subject: Cap finite cardinalities at 2^64, as discussed in the meeting last week. Replace all cardinality comparison functions <=, ==, !=, >=, <, >, with a single compare() function that can return UNKNOWN in the case of unknown (or large-finite and thus not *precisely* known) cardinalities. --- test/unit/expr/type_cardinality_public.h | 124 ++++++------ test/unit/util/cardinality_public.h | 313 ++++++++++++++++--------------- test/unit/util/datatype_black.h | 24 +-- 3 files changed, 239 insertions(+), 222 deletions(-) (limited to 'test/unit') diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 6d6b0740b..7ba212dd5 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -46,9 +46,9 @@ public: } 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 ); + TS_ASSERT( d_em->booleanType().getCardinality().compare(2) == Cardinality::EQUAL ); + TS_ASSERT( d_em->integerType().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL ); + TS_ASSERT( d_em->realType().getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); } void testArrays() { @@ -62,16 +62,15 @@ public: 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 ); -cout << "boolToBool " << boolToBool.getCardinality() << endl; - TS_ASSERT( boolToBool.getCardinality() == 4 ); + TS_ASSERT( intToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( realToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( realToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( intToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( intToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( realToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( boolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( boolToInt.getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL ); + TS_ASSERT( boolToBool.getCardinality().compare(4) == Cardinality::EQUAL ); } void testUnaryFunctions() { @@ -85,15 +84,15 @@ cout << "boolToBool " << boolToBool.getCardinality() << endl; 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 ); + TS_ASSERT( intToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( realToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( realToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( intToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( intToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( realToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( boolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( boolToInt.getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL ); + TS_ASSERT( boolToBool.getCardinality().compare(4) == Cardinality::EQUAL ); } void testBinaryFunctions() { @@ -143,41 +142,41 @@ cout << "boolToBool " << boolToBool.getCardinality() << endl; 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( boolboolToBool.getCardinality().compare(16) == Cardinality::EQUAL ); + TS_ASSERT( boolboolToInt.getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL ); + TS_ASSERT( boolboolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( boolintToBool.getCardinality() == Cardinality::REALS ); - TS_ASSERT( boolintToInt.getCardinality() == Cardinality::REALS ); - TS_ASSERT( boolintToReal.getCardinality() == Cardinality::REALS ); + TS_ASSERT( boolintToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( boolintToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( boolintToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( intboolToBool.getCardinality() == Cardinality::REALS ); - TS_ASSERT( intboolToInt.getCardinality() == Cardinality::REALS ); - TS_ASSERT( intboolToReal.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intboolToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( intboolToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( intboolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( intintToBool.getCardinality() == Cardinality::REALS ); - TS_ASSERT( intintToInt.getCardinality() == Cardinality::REALS ); - TS_ASSERT( intintToReal.getCardinality() == Cardinality::REALS ); + TS_ASSERT( intintToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( intintToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); + TS_ASSERT( intintToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL ); - TS_ASSERT( intrealToBool.getCardinality() > Cardinality::REALS ); - TS_ASSERT( intrealToInt.getCardinality() > Cardinality::REALS ); - TS_ASSERT( intrealToReal.getCardinality() > Cardinality::REALS ); + TS_ASSERT( intrealToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( intrealToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( intrealToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( realintToBool.getCardinality() > Cardinality::REALS ); - TS_ASSERT( realintToInt.getCardinality() > Cardinality::REALS ); - TS_ASSERT( realintToReal.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realintToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( realintToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( realintToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( realrealToBool.getCardinality() > Cardinality::REALS ); - TS_ASSERT( realrealToInt.getCardinality() > Cardinality::REALS ); - TS_ASSERT( realrealToReal.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realrealToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( realrealToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( realrealToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( realboolToBool.getCardinality() > Cardinality::REALS ); - TS_ASSERT( realboolToInt.getCardinality() > Cardinality::REALS ); - TS_ASSERT( realboolToReal.getCardinality() > Cardinality::REALS ); + TS_ASSERT( realboolToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( realboolToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( realboolToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); - TS_ASSERT( boolrealToBool.getCardinality() > Cardinality::REALS ); - TS_ASSERT( boolrealToInt.getCardinality() > Cardinality::REALS ); - TS_ASSERT( boolrealToReal.getCardinality() > Cardinality::REALS ); + TS_ASSERT( boolrealToBool.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( boolrealToInt.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); + TS_ASSERT( boolrealToReal.getCardinality().compare(Cardinality::REALS) == Cardinality::GREATER ); } void testTernaryFunctions() { @@ -191,9 +190,9 @@ cout << "boolToBool " << boolToBool.getCardinality() << endl; 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 ); + TS_ASSERT( boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8) == Cardinality::EQUAL ); + TS_ASSERT( boolboolToBoolbool.getCardinality().compare(/* 4 ^ 4 */ 4 * 4 * 4 * 4) == Cardinality::EQUAL ); + TS_ASSERT( boolToBoolboolbool.getCardinality().compare(/* 8 ^ 2 */ 8 * 8) == Cardinality::EQUAL ); } void testUndefinedSorts() { @@ -205,15 +204,24 @@ cout << "boolToBool " << boolToBool.getCardinality() << endl; void testBitvectors() { Debug.on("bvcard"); - TS_ASSERT( d_em->mkBitVectorType(0).getCardinality() == 0 ); - for(unsigned i = 1; i < 128; ++i) { + TS_ASSERT( d_em->mkBitVectorType(0).getCardinality().compare(0) == Cardinality::EQUAL ); + Cardinality lastCard = 0; + for(unsigned i = 1; i <= 65; ++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()); + Cardinality typeCard = d_em->mkBitVectorType(i).getCardinality(); + TS_ASSERT( typeCard.compare(lastCard) == Cardinality::GREATER || + (typeCard.isLargeFinite() && lastCard.isLargeFinite()) ); + if( typeCard.compare(card) != Cardinality::EQUAL ) { + if( typeCard.isLargeFinite() ) { + cout << "test hit large finite card at bitvector(" << i << ")" << endl; + } else { + stringstream ss; + ss << "test failed for bitvector(" << i << ")"; + TS_FAIL(ss.str().c_str()); + } } + lastCard = typeCard; } catch(Exception& e) { cout << endl << e << endl; throw; diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h index 5927e1bfa..02c80441c 100644 --- a/test/unit/util/cardinality_public.h +++ b/test/unit/util/cardinality_public.h @@ -47,58 +47,58 @@ public: 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.compare(one) == Cardinality::LESS ); + TS_ASSERT( one.compare(two) == Cardinality::LESS ); + TS_ASSERT( two.compare(invalid) == Cardinality::LESS ); + TS_ASSERT( invalid.compare(big) == Cardinality::LESS ); + TS_ASSERT( big.compare(i) == Cardinality::LESS ); + TS_ASSERT( i.compare(r) == Cardinality::LESS ); + + TS_ASSERT( zero.compare(one) != Cardinality::GREATER ); + TS_ASSERT( zero.compare(zero) != Cardinality::GREATER ); + TS_ASSERT( one.compare(two) != Cardinality::GREATER ); + TS_ASSERT( one.compare(one) != Cardinality::GREATER ); + TS_ASSERT( two.compare(invalid) != Cardinality::GREATER ); + TS_ASSERT( two.compare(two) != Cardinality::GREATER ); + TS_ASSERT( invalid.compare(big) != Cardinality::GREATER ); + TS_ASSERT( invalid.compare(invalid) != Cardinality::GREATER ); + TS_ASSERT( big.compare(i) != Cardinality::GREATER ); + TS_ASSERT( big.compare(big) != Cardinality::GREATER ); + TS_ASSERT( i.compare(r) != Cardinality::GREATER ); + TS_ASSERT( i.compare(i) != Cardinality::GREATER ); + TS_ASSERT( r.compare(r) != Cardinality::GREATER ); + + TS_ASSERT( zero.compare(zero) == Cardinality::EQUAL ); + TS_ASSERT( one.compare(one) == Cardinality::EQUAL ); + TS_ASSERT( two.compare(two) == Cardinality::EQUAL ); + TS_ASSERT( invalid.compare(invalid) == Cardinality::EQUAL ); + TS_ASSERT( copy.compare(copy) == Cardinality::EQUAL ); + TS_ASSERT( copy.compare(one) == Cardinality::EQUAL ); + TS_ASSERT( one.compare(copy) == Cardinality::EQUAL ); + TS_ASSERT( big.compare(big) == Cardinality::UNKNOWN ); + TS_ASSERT( i.compare(i) == Cardinality::EQUAL ); + TS_ASSERT( r.compare(r) == Cardinality::EQUAL ); + + TS_ASSERT( zero.compare(one) != Cardinality::EQUAL ); + TS_ASSERT( one.compare(two) != Cardinality::EQUAL ); + TS_ASSERT( two.compare(invalid) != Cardinality::EQUAL ); + TS_ASSERT( copy.compare(r) != Cardinality::EQUAL ); + TS_ASSERT( copy.compare(i) != Cardinality::EQUAL ); + TS_ASSERT( big.compare(i) != Cardinality::EQUAL ); + TS_ASSERT( i.compare(big) != Cardinality::EQUAL ); + TS_ASSERT( big.compare(zero) != Cardinality::EQUAL ); + TS_ASSERT( r.compare(i) != Cardinality::EQUAL ); + TS_ASSERT( i.compare(r) != Cardinality::EQUAL ); + + TS_ASSERT( r.compare(zero) == Cardinality::GREATER ); + TS_ASSERT( r.compare(one) == Cardinality::GREATER ); + TS_ASSERT( r.compare(two) == Cardinality::GREATER ); + TS_ASSERT( r.compare(copy) == Cardinality::GREATER ); + TS_ASSERT( r.compare(invalid) == Cardinality::GREATER ); + TS_ASSERT( r.compare(big) == Cardinality::GREATER ); + TS_ASSERT( r.compare(i) == Cardinality::GREATER ); + TS_ASSERT( r.compare(r) != Cardinality::GREATER ); + TS_ASSERT( r.compare(r) != Cardinality::LESS ); TS_ASSERT( zero.isFinite() ); TS_ASSERT( one.isFinite() ); @@ -109,12 +109,21 @@ public: TS_ASSERT( !i.isFinite() ); TS_ASSERT( !r.isFinite() ); + TS_ASSERT( !zero.isLargeFinite() ); + TS_ASSERT( !one.isLargeFinite() ); + TS_ASSERT( !two.isLargeFinite() ); + TS_ASSERT( !copy.isLargeFinite() ); + TS_ASSERT( !invalid.isLargeFinite() ); + TS_ASSERT( big.isLargeFinite() ); + TS_ASSERT( !i.isLargeFinite() ); + TS_ASSERT( !r.isLargeFinite() ); + 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( big.getFiniteCardinality(), IllegalArgumentException ); TS_ASSERT_THROWS( i.getFiniteCardinality(), IllegalArgumentException ); TS_ASSERT_THROWS( r.getFiniteCardinality(), IllegalArgumentException ); @@ -127,127 +136,127 @@ public: 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 ); + TS_ASSERT( zero.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); + TS_ASSERT( one.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); + TS_ASSERT( two.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); + TS_ASSERT( copy.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); + TS_ASSERT( invalid.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); + TS_ASSERT( big.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); + TS_ASSERT( r.compare(Cardinality::INTEGERS) != Cardinality::EQUAL ); + TS_ASSERT( i.compare(Cardinality::INTEGERS) == Cardinality::EQUAL ); + + TS_ASSERT( zero.compare(Cardinality::REALS) != Cardinality::EQUAL ); + TS_ASSERT( one.compare(Cardinality::REALS) != Cardinality::EQUAL ); + TS_ASSERT( two.compare(Cardinality::REALS) != Cardinality::EQUAL ); + TS_ASSERT( copy.compare(Cardinality::REALS) != Cardinality::EQUAL ); + TS_ASSERT( invalid.compare(Cardinality::REALS) != Cardinality::EQUAL ); + TS_ASSERT( big.compare(Cardinality::REALS) != Cardinality::EQUAL ); + TS_ASSERT( i.compare(Cardinality::REALS) != Cardinality::EQUAL ); + TS_ASSERT( r.compare(Cardinality::REALS) == Cardinality::EQUAL ); // 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 ); + TS_ASSERT( Cardinality::INTEGERS.compare(zero) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::INTEGERS.compare(one) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::INTEGERS.compare(two) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::INTEGERS.compare(copy) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::INTEGERS.compare(invalid) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::INTEGERS.compare(big) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::INTEGERS.compare(r) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::INTEGERS.compare(i) == Cardinality::EQUAL ); + + TS_ASSERT( Cardinality::REALS.compare(zero) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::REALS.compare(one) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::REALS.compare(two) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::REALS.compare(copy) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::REALS.compare(invalid) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::REALS.compare(big) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::REALS.compare(i) != Cardinality::EQUAL ); + TS_ASSERT( Cardinality::REALS.compare(r) == Cardinality::EQUAL ); // 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 ); + TS_ASSERT( (zero + zero).compare(zero) == Cardinality::EQUAL ); + TS_ASSERT( (zero * zero).compare(zero) == Cardinality::EQUAL ); + TS_ASSERT( (zero ^ zero).compare(one) == Cardinality::EQUAL ); + TS_ASSERT( (zero + one).compare(one) == Cardinality::EQUAL ); + TS_ASSERT( (zero * one).compare(zero) == Cardinality::EQUAL ); + TS_ASSERT( (zero ^ one).compare(zero) == Cardinality::EQUAL ); + TS_ASSERT( (one + zero).compare(one) == Cardinality::EQUAL ); + TS_ASSERT( (one * zero).compare(zero) == Cardinality::EQUAL ); + TS_ASSERT( (one ^ zero).compare(one) == Cardinality::EQUAL ); + TS_ASSERT( (two + two).compare(4) == Cardinality::EQUAL ); + TS_ASSERT( (two ^ two).compare(4) == Cardinality::EQUAL ); + TS_ASSERT( (two * two).compare(4) == Cardinality::EQUAL ); + TS_ASSERT( (two += two).compare(4) == Cardinality::EQUAL ); + TS_ASSERT( two.compare(4) == Cardinality::EQUAL ); + TS_ASSERT( (two = 2).compare(2) == Cardinality::EQUAL ); + TS_ASSERT( two.compare(2) == Cardinality::EQUAL ); + TS_ASSERT( (two *= 2).compare(4) == Cardinality::EQUAL ); + TS_ASSERT( two.compare(4) == Cardinality::EQUAL ); + TS_ASSERT( ((two = 2) ^= 2).compare(4) == Cardinality::EQUAL ); + TS_ASSERT( two.compare(4) == Cardinality::EQUAL ); + TS_ASSERT( (two = 2).compare(2) == Cardinality::EQUAL ); // 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.compare(i) == Cardinality::EQUAL && y.compare(r) == Cardinality::EQUAL ); + TS_ASSERT( x.compare(r) != Cardinality::EQUAL && y.compare(i) != Cardinality::EQUAL ); + TS_ASSERT( x.compare(z) != Cardinality::EQUAL && y.compare(z) != Cardinality::EQUAL ); 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( big.compare(x) == Cardinality::LESS ); + TS_ASSERT( x.compare(y) == Cardinality::LESS ); + TS_ASSERT( y.compare(z) == Cardinality::LESS ); 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( (zero ^ x).compare(zero) == Cardinality::EQUAL ); + TS_ASSERT( (one ^ x).compare(one) == Cardinality::EQUAL ); + TS_ASSERT( (two ^ x).compare(y) == Cardinality::EQUAL && (two ^ x).compare(x) != Cardinality::EQUAL ); + TS_ASSERT( (big ^ x).compare(y) == Cardinality::EQUAL && (big ^ x).compare(x) != Cardinality::EQUAL ); + TS_ASSERT( (two ^ x).compare(big ^ x) == Cardinality::EQUAL ); + + TS_ASSERT( (x ^ zero).compare(one) == Cardinality::EQUAL ); + TS_ASSERT( (x ^ one).compare(x) == Cardinality::EQUAL ); + TS_ASSERT( (x ^ two).compare(x) == Cardinality::EQUAL ); + TS_ASSERT( (x ^ big).compare(x) == Cardinality::EQUAL ); + TS_ASSERT( (x ^ big).compare(x ^ two) == Cardinality::EQUAL ); + + TS_ASSERT( (zero ^ y).compare(zero) == Cardinality::EQUAL ); + TS_ASSERT( (one ^ y).compare(one) == Cardinality::EQUAL ); + TS_ASSERT( (two ^ y).compare(x) != Cardinality::EQUAL && (two ^ y).compare(y) != Cardinality::EQUAL ); + TS_ASSERT( (big ^ y).compare(y) != Cardinality::EQUAL && (big ^ y).compare(y) != Cardinality::EQUAL ); 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( (two ^ y).compare(big ^ y) == Cardinality::EQUAL ); + + TS_ASSERT( (y ^ zero).compare(one) == Cardinality::EQUAL ); + TS_ASSERT( (y ^ one).compare(y) == Cardinality::EQUAL ); + TS_ASSERT( (y ^ two).compare(y) == Cardinality::EQUAL ); + TS_ASSERT( (y ^ big).compare(y) == Cardinality::EQUAL ); + TS_ASSERT( (y ^ big).compare(y ^ two) == Cardinality::EQUAL ); + + TS_ASSERT( (x ^ x).compare(y) == Cardinality::EQUAL ); + TS_ASSERT( (y ^ x).compare(y) == Cardinality::EQUAL ); + TS_ASSERT( (x ^ y).compare(z) == Cardinality::EQUAL ); + TS_ASSERT( (y ^ y).compare(z) == Cardinality::EQUAL ); + TS_ASSERT( (z ^ x).compare(z) == Cardinality::EQUAL ); + TS_ASSERT( (z ^ y).compare(z) == Cardinality::EQUAL ); + TS_ASSERT( (zero ^ z).compare(0) == Cardinality::EQUAL ); + TS_ASSERT( (z ^ zero).compare(1) == Cardinality::EQUAL ); + TS_ASSERT( (z ^ 0).compare(1) == Cardinality::EQUAL ); + TS_ASSERT( (two ^ z).compare(z) == Cardinality::GREATER ); + TS_ASSERT( (big ^ z).compare(two ^ z) == Cardinality::EQUAL ); + TS_ASSERT( (x ^ z).compare(two ^ z) == Cardinality::EQUAL ); + TS_ASSERT( (y ^ z).compare(x ^ z) == Cardinality::EQUAL ); + TS_ASSERT( (z ^ z).compare(x ^ z) == Cardinality::EQUAL ); TS_ASSERT( (z ^ z).getBethNumber() == 3 ); }/* testCardinalities() */ diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 6c449233c..5042852fc 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -71,8 +71,8 @@ public: TS_ASSERT_THROWS(colorsDT["blue"]["foo"], IllegalArgumentException); TS_ASSERT(colorsType.getDatatype().isFinite()); - TS_ASSERT(colorsType.getDatatype().getCardinality() == 4); - TS_ASSERT(ctor.getType().getCardinality() == 1); + TS_ASSERT(colorsType.getDatatype().getCardinality().compare(4) == Cardinality::EQUAL); + TS_ASSERT(ctor.getType().getCardinality().compare(1) == Cardinality::EQUAL); TS_ASSERT(colorsType.getDatatype().isWellFounded()); Debug("groundterms") << "ground term of " << colorsType.getDatatype().getName() << endl << " is " << colorsType.mkGroundTerm() << endl; @@ -108,7 +108,7 @@ public: Debug("datatypes") << apply << std::endl; TS_ASSERT(! natType.getDatatype().isFinite()); - TS_ASSERT(natType.getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(natType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(natType.getDatatype().isWellFounded()); Debug("groundterms") << "ground term of " << natType.getDatatype().getName() << endl << " is " << natType.mkGroundTerm() << endl; @@ -149,7 +149,7 @@ public: TS_ASSERT_THROWS(treeType.getConstructor("leff"), IllegalArgumentException); TS_ASSERT(! treeType.getDatatype().isFinite()); - TS_ASSERT(treeType.getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(treeType.getDatatype().isWellFounded()); Debug("groundterms") << "ground term of " << treeType.getDatatype().getName() << endl << " is " << treeType.mkGroundTerm() << endl; @@ -183,7 +183,7 @@ public: Debug("datatypes") << listType << std::endl; TS_ASSERT(! listType.getDatatype().isFinite()); - TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(listType.getDatatype().isWellFounded()); Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl << " is " << listType.mkGroundTerm() << endl; @@ -217,7 +217,7 @@ public: Debug("datatypes") << listType << std::endl; TS_ASSERT(! listType.getDatatype().isFinite()); - TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::REALS); + TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::REALS) == Cardinality::EQUAL); TS_ASSERT(listType.getDatatype().isWellFounded()); Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl << " is " << listType.mkGroundTerm() << endl; @@ -251,7 +251,7 @@ public: Debug("datatypes") << listType << std::endl; TS_ASSERT(! listType.getDatatype().isFinite()); - TS_ASSERT(listType.getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(listType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(listType.getDatatype().isWellFounded()); Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl << " is " << listType.mkGroundTerm() << endl; @@ -316,7 +316,7 @@ public: TS_ASSERT(dtts[1].getDatatype().isResolved()); TS_ASSERT(! dtts[0].getDatatype().isFinite()); - TS_ASSERT(dtts[0].getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(dtts[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(dtts[0].getDatatype().isWellFounded()); Debug("groundterms") << "ground term of " << dtts[0].getDatatype().getName() << endl << " is " << dtts[0].mkGroundTerm() << endl; @@ -333,7 +333,7 @@ public: } TS_ASSERT(! dtts[1].getDatatype().isFinite()); - TS_ASSERT(dtts[1].getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(dtts[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(dtts[1].getDatatype().isWellFounded()); Debug("groundterms") << "ground term of " << dtts[1].getDatatype().getName() << endl << " is " << dtts[1].mkGroundTerm() << endl; @@ -364,7 +364,7 @@ public: TS_ASSERT_DIFFERS(dtts[0], dtts2[0]); TS_ASSERT(! dtts2[0].getDatatype().isFinite()); - TS_ASSERT(dtts2[0].getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(dtts2[0].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(dtts2[0].getDatatype().isWellFounded()); Debug("groundterms") << "ground term of " << dtts2[0].getDatatype().getName() << endl << " is " << dtts2[0].mkGroundTerm() << endl; @@ -381,7 +381,7 @@ public: } TS_ASSERT(! dtts2[1].getDatatype().isFinite()); - TS_ASSERT(dtts2[1].getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(dtts2[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(dtts2[1].getDatatype().isWellFounded()); Debug("groundterms") << "ground term of " << dtts2[1].getDatatype().getName() << endl << " is " << dtts2[1].mkGroundTerm() << endl; @@ -411,7 +411,7 @@ public: Debug("datatypes") << treeType << std::endl; TS_ASSERT(! treeType.getDatatype().isFinite()); - TS_ASSERT(treeType.getDatatype().getCardinality() == Cardinality::INTEGERS); + TS_ASSERT(treeType.getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); TS_ASSERT(! treeType.getDatatype().isWellFounded()); TS_ASSERT_THROWS_ANYTHING( treeType.mkGroundTerm() ); TS_ASSERT_THROWS_ANYTHING( treeType.getDatatype().mkGroundTerm( treeType ) ); -- cgit v1.2.3