summaryrefslogtreecommitdiff
path: root/test/unit
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit')
-rw-r--r--test/unit/Makefile.am2
-rw-r--r--test/unit/expr/type_cardinality_public.h223
-rw-r--r--test/unit/util/cardinality_public.h255
-rw-r--r--test/unit/util/integer_black.h12
-rw-r--r--test/unit/util/subrange_bound_white.h4
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback