diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 5 | ||||
-rw-r--r-- | test/unit/util/integer_black.h | 276 | ||||
-rw-r--r-- | test/unit/util/integer_white.h | 40 | ||||
-rw-r--r-- | test/unit/util/rational_white.h | 98 |
4 files changed, 418 insertions, 1 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index f78171dac..1d5bcc230 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -14,7 +14,10 @@ UNIT_TESTS = \ theory/theory_uf_white \ util/assert_white \ util/configuration_white \ - util/output_white + util/output_white \ + util/integer_black \ + util/integer_white \ + util/rational_white # Things that aren't tests but that tests rely on and need to # go into the distribution diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h new file mode 100644 index 000000000..afd2145e3 --- /dev/null +++ b/test/unit/util/integer_black.h @@ -0,0 +1,276 @@ +/********************* */ +/** integer_black.h + ** Original author: taking + ** 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. + ** + ** Black box testing of CVC4::Integer. + **/ + +#include <cxxtest/TestSuite.h> +#include <sstream> + +#include "util/integer.h" + +using namespace CVC4; +using namespace std; + +const char* largeVal = "4547897890548754897897897897890789078907890"; + +class IntegerBlack : public CxxTest::TestSuite { + + +public: + + void testConstructors() { + Integer z0(1); + TS_ASSERT_EQUALS(z0.getLong(), 1); + + Integer z1(0); + TS_ASSERT_EQUALS(z1.getLong(), 0); + + Integer z2(-1); + TS_ASSERT_EQUALS(z2.getLong(), -1); + + Integer z3(0x890UL); + TS_ASSERT_EQUALS(z3.getUnsignedLong(), 0x890UL); + + Integer z4; + TS_ASSERT_EQUALS(z4.getLong(), 0); + + Integer z5("7896890"); + TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890); + + Integer z6(z5); + TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890); + TS_ASSERT_EQUALS(z6.getUnsignedLong(), 7896890); + + + string bigValue("1536729"); + Integer z7(bigValue); + TS_ASSERT_EQUALS(z7.getUnsignedLong(), 1536729); + } + + void testOperatorAssign(){ + Integer x(0); + Integer y(79); + Integer z(45789); + + TS_ASSERT_EQUALS(x.getUnsignedLong(), 0); + TS_ASSERT_EQUALS(y.getUnsignedLong(), 79); + TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789); + + x = y = z; + + TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(y.getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789); + + Integer a(2); + + y = a; + + TS_ASSERT_EQUALS(a.getUnsignedLong(), 2); + TS_ASSERT_EQUALS(y.getUnsignedLong(), 2); + TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789); + } + + void testOperatorEquals(){ + Integer a(0); + Integer b(79); + Integer c("79"); + Integer d; + + TS_ASSERT( (a==a)); + TS_ASSERT(!(a==b)); + TS_ASSERT(!(a==c)); + TS_ASSERT( (a==d)); + + TS_ASSERT(!(b==a)); + TS_ASSERT( (b==b)); + TS_ASSERT( (b==c)); + TS_ASSERT(!(b==d)); + + TS_ASSERT(!(c==a)); + TS_ASSERT( (c==b)); + TS_ASSERT( (c==c)); + TS_ASSERT(!(c==d)); + + TS_ASSERT( (d==a)); + TS_ASSERT(!(d==b)); + TS_ASSERT(!(d==c)); + TS_ASSERT( (d==d)); + + } + + void testOperatorNotEquals(){ + Integer a(0); + Integer b(79); + Integer c("79"); + Integer d; + + TS_ASSERT(!(a!=a)); + TS_ASSERT( (a!=b)); + TS_ASSERT( (a!=c)); + TS_ASSERT(!(a!=d)); + + TS_ASSERT( (b!=a)); + TS_ASSERT(!(b!=b)); + TS_ASSERT(!(b!=c)); + TS_ASSERT( (b!=d)); + + TS_ASSERT( (c!=a)); + TS_ASSERT(!(c!=b)); + TS_ASSERT(!(c!=c)); + TS_ASSERT( (c!=d)); + + TS_ASSERT(!(d!=a)); + TS_ASSERT( (d!=b)); + TS_ASSERT( (d!=c)); + TS_ASSERT(!(d!=d)); + + } + + void testOperatorSubtract(){ + Integer x(0); + Integer y(79); + Integer z(-34); + + + Integer act0 = x - x; + Integer act1 = x - y; + Integer act2 = x - z; + Integer exp0(0); + Integer exp1(-79); + Integer exp2(34); + + + Integer act3 = y - x; + Integer act4 = y - y; + Integer act5 = y - z; + Integer exp3(79); + Integer exp4(0); + Integer exp5(113); + + + Integer act6 = z - x; + Integer act7 = z - y; + Integer act8 = z - z; + Integer exp6(-34); + Integer exp7(-113); + Integer exp8(0); + + + + TS_ASSERT_EQUALS(act0, exp0); + TS_ASSERT_EQUALS(act1, exp1); + TS_ASSERT_EQUALS(act2, exp2); + TS_ASSERT_EQUALS(act3, exp3); + TS_ASSERT_EQUALS(act4, exp4); + TS_ASSERT_EQUALS(act5, exp5); + TS_ASSERT_EQUALS(act6, exp6); + TS_ASSERT_EQUALS(act7, exp7); + TS_ASSERT_EQUALS(act8, exp8); + } + void testOperatorAdd(){ + Integer x(0); + Integer y(79); + Integer z(-34); + + + Integer act0 = x + x; + Integer act1 = x + y; + Integer act2 = x + z; + Integer exp0(0); + Integer exp1(79); + Integer exp2(-34); + + + Integer act3 = y + x; + Integer act4 = y + y; + Integer act5 = y + z; + Integer exp3(79); + Integer exp4(158); + Integer exp5(45); + + + Integer act6 = z + x; + Integer act7 = z + y; + Integer act8 = z + z; + Integer exp6(-34); + Integer exp7(45); + Integer exp8(-68); + + + + TS_ASSERT_EQUALS(act0, exp0); + TS_ASSERT_EQUALS(act1, exp1); + TS_ASSERT_EQUALS(act2, exp2); + TS_ASSERT_EQUALS(act3, exp3); + TS_ASSERT_EQUALS(act4, exp4); + TS_ASSERT_EQUALS(act5, exp5); + TS_ASSERT_EQUALS(act6, exp6); + TS_ASSERT_EQUALS(act7, exp7); + TS_ASSERT_EQUALS(act8, exp8); + } + + void testOperatorMult(){ + Integer x(0); + Integer y(79); + Integer z(-34); + + + Integer act0 = x * x; + Integer act1 = x * y; + Integer act2 = x * z; + Integer exp0(0); + Integer exp1(0); + Integer exp2(0); + + + Integer act3 = y * x; + Integer act4 = y * y; + Integer act5 = y * z; + Integer exp3(0); + Integer exp4(6241); + Integer exp5(-2686); + + + Integer act6 = z * x; + Integer act7 = z * y; + Integer act8 = z * z; + Integer exp6(0); + Integer exp7(-2686); + Integer exp8(1156); + + + + TS_ASSERT_EQUALS(act0, exp0); + TS_ASSERT_EQUALS(act1, exp1); + TS_ASSERT_EQUALS(act2, exp2); + TS_ASSERT_EQUALS(act3, exp3); + TS_ASSERT_EQUALS(act4, exp4); + TS_ASSERT_EQUALS(act5, exp5); + TS_ASSERT_EQUALS(act6, exp6); + TS_ASSERT_EQUALS(act7, exp7); + TS_ASSERT_EQUALS(act8, exp8); + } + + + void testToStringStuff(){ + stringstream ss; + Integer large (largeVal); + ss << large; + string res = ss.str(); + + TS_ASSERT_EQUALS(res, large.toString()); + } + +}; diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h new file mode 100644 index 000000000..739715ac2 --- /dev/null +++ b/test/unit/util/integer_white.h @@ -0,0 +1,40 @@ +/********************* */ +/** integer_white.h + ** Original author: taking + ** 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. + ** + ** White box testing of CVC4::Integer. + **/ + +#include <cxxtest/TestSuite.h> +#include <sstream> + +#include "util/integer.h" + +using namespace CVC4; +using namespace std; + +const char* largeVal = "4547897890548754897897897897890789078907890"; + +class IntegerWhite : public CxxTest::TestSuite { +public: + + void testHash(){ + Integer large (largeVal); + Integer zero; + Integer one_word(75890); + Integer two_words("7890D789D33234027890D789D3323402", 16); + + TS_ASSERT_EQUALS(zero.hash(), 0); + TS_ASSERT_EQUALS(one_word.hash(), 75890); + TS_ASSERT_EQUALS(two_words.hash(), 9921844058862803974UL); + TS_ASSERT_EQUALS(large.hash(), 772190219532412699UL); + } +}; diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h new file mode 100644 index 000000000..6acc5b71f --- /dev/null +++ b/test/unit/util/rational_white.h @@ -0,0 +1,98 @@ +/********************* */ +/** rational_white.h + ** Original author: taking + ** 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. + ** + ** White box testing of CVC4::Rational. + **/ + +#include <cxxtest/TestSuite.h> +#include <sstream> + +#include "util/rational.h" + +using namespace CVC4; +using namespace std; + +const char* canReduce = "4547897890548754897897897897890789078907890/54878902347890234"; + +class RationalWhite : public CxxTest::TestSuite { +public: + + void testReductionAtConstructionTime(){ + Rational reduce0(canReduce); + Integer num0("2273948945274377448948948948945394539453945"); + Integer den0("27439451173945117"); + + TS_ASSERT_EQUALS(reduce0.getNumerator(), num0); + TS_ASSERT_EQUALS(reduce0.getDenominator(), den0); + + Rational reduce1(0, 454789); + Integer num1(0); + Integer den1(1); + + TS_ASSERT_EQUALS(reduce1.getNumerator(), num1); + TS_ASSERT_EQUALS(reduce1.getDenominator(), den1); + + Rational reduce2(0, -454789); + Integer num2(0); + Integer den2(1); + + + TS_ASSERT_EQUALS(reduce2.getNumerator(), num2); + TS_ASSERT_EQUALS(reduce2.getDenominator(), den2); + + + Rational reduce3( 454789890342L, 273L); + Integer num3(151596630114L); + Integer den3(91); + + TS_ASSERT_EQUALS(reduce2.getNumerator(), num2); + TS_ASSERT_EQUALS(reduce2.getDenominator(), den2); + + Rational reduce4( 454789890342L,-273L); + Integer num4(-151596630114L); + Integer den4(91); + + + TS_ASSERT_EQUALS(reduce4.getNumerator(), num4); + TS_ASSERT_EQUALS(reduce4.getDenominator(), den4); + + Rational reduce5(-454789890342L, 273L); + Integer num5(-151596630114L); + Integer den5(91); + + + TS_ASSERT_EQUALS(reduce5.getNumerator(), num5); + TS_ASSERT_EQUALS(reduce5.getDenominator(), den5); + + Rational reduce6(-454789890342L,-273L); + Integer num6(151596630114L); + Integer den6(91); + + + TS_ASSERT_EQUALS(reduce6.getNumerator(), num6); + TS_ASSERT_EQUALS(reduce6.getDenominator(), den6); + + } + + void testHash(){ + Rational large (canReduce); + Rational zero; + Rational one_word(75890L,590L); + Rational two_words("7890D789D33234027890D789D3323402", 16); + + TS_ASSERT_EQUALS(zero.hash(), 1); + TS_ASSERT_EQUALS(one_word.hash(), 7589 xor 59); + TS_ASSERT_EQUALS(two_words.hash(), 9921844058862803974UL ^ 1); + TS_ASSERT_EQUALS(large.hash(), + (large.getNumerator().hash())^(large.getDenominator().hash())); + } +}; |