diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-22 22:31:59 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-22 22:31:59 +0000 |
commit | 3dff1d2eef828dc3ff17750a738d6a6bff0ed484 (patch) | |
tree | 52d26b9ba5ed3590bf728eb8ae384195e56c26fa /test/unit/expr | |
parent | 8ba847f7c4c6385cc4a788c3b965498acb3f0f08 (diff) |
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.
Diffstat (limited to 'test/unit/expr')
-rw-r--r-- | test/unit/expr/type_cardinality_public.h | 124 |
1 files changed, 66 insertions, 58 deletions
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; |