summaryrefslogtreecommitdiff
path: root/test/unit/util/integer_black.h
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/util/integer_black.h')
-rw-r--r--test/unit/util/integer_black.h559
1 files changed, 0 insertions, 559 deletions
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
deleted file mode 100644
index ccceefac6..000000000
--- a/test/unit/util/integer_black.h
+++ /dev/null
@@ -1,559 +0,0 @@
-/********************* */
-/*! \file integer_black.h
- ** \verbatim
- ** Top contributors (to current version):
- ** Tim King, Aina Niemetz, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Black box testing of CVC4::Integer.
- **
- ** Black box testing of CVC4::Integer.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <limits>
-#include <sstream>
-
-#include "util/integer.h"
-
-using namespace CVC4;
-using namespace std;
-
-const char* largeVal = "4547897890548754897897897897890789078907890";
-const char* lotsOfLeadingZeroes = "00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000001";
-
-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(), 7896890ul);
-
- Integer z6(z5);
- TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890ul);
- TS_ASSERT_EQUALS(z6.getUnsignedLong(), 7896890ul);
-
-
- string bigValue("1536729");
- Integer z7(bigValue);
- TS_ASSERT_EQUALS(z7.getUnsignedLong(), 1536729ul);
- }
-
- void testCompareAgainstZero(){
- Integer z(0);
- TS_ASSERT_THROWS_NOTHING(z == 0;);
- TS_ASSERT_EQUALS(z,0);
- }
-
- void testOperatorAssign(){
- Integer x(0);
- Integer y(79);
- Integer z(45789);
-
- TS_ASSERT_EQUALS(x.getUnsignedLong(), 0ul);
- TS_ASSERT_EQUALS(y.getUnsignedLong(), 79ul);
- TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
-
- x = y = z;
-
- TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789ul);
- TS_ASSERT_EQUALS(y.getUnsignedLong(), 45789ul);
- TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
-
- Integer a(2);
-
- y = a;
-
- TS_ASSERT_EQUALS(a.getUnsignedLong(), 2ul);
- TS_ASSERT_EQUALS(y.getUnsignedLong(), 2ul);
- TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789ul);
- TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
- }
-
- 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());
- }
-
- void testBaseInference() {
- TS_ASSERT_EQUALS(Integer("0xa", 0), 10);
- TS_ASSERT_EQUALS(Integer("0xff", 0), 255);
- TS_ASSERT_EQUALS(Integer("011", 0), 9);
- TS_ASSERT_EQUALS(Integer("0b1010", 0), 10);
- TS_ASSERT_EQUALS(Integer("-1", 0), -1);
- TS_ASSERT_EQUALS(Integer("42", 0), 42);
- }
-
- void testParseErrors() {
- TS_ASSERT_THROWS(Integer("abracadabra"), std::invalid_argument&);
- TS_ASSERT_THROWS(Integer("+-1"), std::invalid_argument&);
- TS_ASSERT_THROWS(Integer("-+1"), std::invalid_argument&);
- TS_ASSERT_THROWS(Integer("5i"), std::invalid_argument&);
- TS_ASSERT_THROWS(Integer("10xyz"), std::invalid_argument&);
- TS_ASSERT_THROWS(Integer("0xff", 10), std::invalid_argument&);
- TS_ASSERT_THROWS(Integer("#x5", 0), std::invalid_argument&);
- TS_ASSERT_THROWS(Integer("0b123", 0), std::invalid_argument&);
- }
-
- void testPow() {
- TS_ASSERT_EQUALS( Integer(1), Integer(1).pow(0) );
- TS_ASSERT_EQUALS( Integer(1), Integer(5).pow(0) );
- TS_ASSERT_EQUALS( Integer(1), Integer(-1).pow(0) );
- TS_ASSERT_EQUALS( Integer(0), Integer(0).pow(1) );
- TS_ASSERT_EQUALS( Integer(5), Integer(5).pow(1) );
- TS_ASSERT_EQUALS( Integer(-5), Integer(-5).pow(1) );
- TS_ASSERT_EQUALS( Integer(16), Integer(2).pow(4) );
- TS_ASSERT_EQUALS( Integer(16), Integer(-2).pow(4) );
- TS_ASSERT_EQUALS( Integer(1000), Integer(10).pow(3) );
- 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) );
- TS_ASSERT( ! Integer(0).testBit(4) );
- TS_ASSERT( ! Integer(0).testBit(3) );
- TS_ASSERT( ! Integer(0).testBit(2) );
- TS_ASSERT( ! Integer(0).testBit(1) );
- TS_ASSERT( ! Integer(0).testBit(0) );
-
- TS_ASSERT( Integer(-1).testBit(6) );
- TS_ASSERT( Integer(-1).testBit(5) );
- TS_ASSERT( Integer(-1).testBit(4) );
- TS_ASSERT( Integer(-1).testBit(3) );
- TS_ASSERT( Integer(-1).testBit(2) );
- TS_ASSERT( Integer(-1).testBit(1) );
- TS_ASSERT( Integer(-1).testBit(0) );
-
- TS_ASSERT( ! Integer(10).testBit(6) );
- TS_ASSERT( ! Integer(10).testBit(5) );
- TS_ASSERT( ! Integer(10).testBit(4) );
- TS_ASSERT( Integer(10).testBit(3) );
- TS_ASSERT( ! Integer(10).testBit(2) );
- TS_ASSERT( Integer(10).testBit(1) );
- TS_ASSERT( ! Integer(10).testBit(0) );
-
- TS_ASSERT( ! Integer(14).testBit(6) );
- TS_ASSERT( ! Integer(14).testBit(5) );
- TS_ASSERT( ! Integer(14).testBit(4) );
- TS_ASSERT( Integer(14).testBit(3) );
- TS_ASSERT( Integer(14).testBit(2) );
- TS_ASSERT( Integer(14).testBit(1) );
- TS_ASSERT( ! Integer(14).testBit(0) );
-
- TS_ASSERT( Integer(64).testBit(6) );
- TS_ASSERT( ! Integer(64).testBit(5) );
- TS_ASSERT( ! Integer(64).testBit(4) );
- TS_ASSERT( ! Integer(64).testBit(3) );
- TS_ASSERT( ! Integer(64).testBit(2) );
- TS_ASSERT( ! Integer(64).testBit(1) );
- TS_ASSERT( ! Integer(64).testBit(0) );
- }
-
- unsigned int internalLength(int i){
- if ( i == 0){
- return 1;
- }else{
- int absi = i < 0 ? -i : i;
- unsigned int n = 0;
- int powN = 1;
- do {
- powN <<= 1;
- ++n;
- }while(absi >= powN);
- return n;
- }
- }
-
- void testTestLength() {
- for(int i = -17; i <= 17; ++i){
- TS_ASSERT_EQUALS(Integer(i).length(), internalLength(i));
- }
- }
-
- void testEuclideanDivision() {
- Integer q, r;
-
- Integer::euclidianQR(q, r, 1, 4);
- TS_ASSERT_EQUALS( q, Integer(0));
- TS_ASSERT_EQUALS( r, Integer(1));
-
-
- Integer::euclidianQR(q, r, 1, -4);
- TS_ASSERT_EQUALS( q, Integer(0));
- TS_ASSERT_EQUALS( r, Integer(1));
-
- Integer::euclidianQR(q, r, -1, 4);
- TS_ASSERT_EQUALS( q, Integer(-1));
- TS_ASSERT_EQUALS( r, Integer(3));
-
- Integer::euclidianQR(q,r, -1, -4);
- TS_ASSERT_EQUALS( q, Integer(1));
- TS_ASSERT_EQUALS( r, Integer(3));
-
- Integer::euclidianQR(q,r, 5, 4);
- TS_ASSERT_EQUALS( q, Integer(1));
- TS_ASSERT_EQUALS( r, Integer(1));
-
- Integer::euclidianQR(q,r, 5, -4);
- TS_ASSERT_EQUALS( q, Integer(-1));
- TS_ASSERT_EQUALS( r, Integer(1));
-
- Integer::euclidianQR(q,r, -5, 4);
- TS_ASSERT_EQUALS( q, Integer(-2));
- TS_ASSERT_EQUALS( r, Integer(3));
-
- Integer::euclidianQR(q,r, -5, -4);
- TS_ASSERT_EQUALS( q, Integer(2));
- TS_ASSERT_EQUALS( r, Integer(3));
-
- }
- void testFloorDivision() {
- Integer q, r;
-
- Integer::floorQR(q, r, 1, 4);
- TS_ASSERT_EQUALS( q, Integer(0));
- TS_ASSERT_EQUALS( r, Integer(1));
-
-
- Integer::floorQR(q, r, 1, -4);
- TS_ASSERT_EQUALS( q, Integer(-1));
- TS_ASSERT_EQUALS( r, Integer(-3));
-
- Integer::floorQR(q, r, -1, 4);
- TS_ASSERT_EQUALS( q, Integer(-1));
- TS_ASSERT_EQUALS( r, Integer(3));
-
- Integer::floorQR(q,r, -1, -4);
- TS_ASSERT_EQUALS( q, Integer(0));
- TS_ASSERT_EQUALS( r, Integer(-1));
-
- Integer::floorQR(q,r, 5, 4);
- TS_ASSERT_EQUALS( q, Integer(1));
- TS_ASSERT_EQUALS( r, Integer(1));
-
- Integer::floorQR(q,r, 5, -4);
- TS_ASSERT_EQUALS( q, Integer(-2));
- TS_ASSERT_EQUALS( r, Integer(-3));
-
- Integer::floorQR(q,r, -5, 4);
- TS_ASSERT_EQUALS( q, Integer(-2));
- TS_ASSERT_EQUALS( r, Integer(3));
-
- Integer::floorQR(q,r, -5, -4);
- TS_ASSERT_EQUALS( q, Integer(1));
- TS_ASSERT_EQUALS( r, Integer(-1));
-
- }
-
- void testLeadingZeroes() {
- string leadingZeroes(lotsOfLeadingZeroes);
- Integer one(1u);
- Integer one_from_string(leadingZeroes,2);
- TS_ASSERT_EQUALS(one, one_from_string);
- }
-
- void testModAdd()
- {
- for (unsigned i = 0; i <= 10; ++i)
- {
- for (unsigned j = 0; j <= 10; ++j)
- {
- Integer yy;
- Integer x(i);
- Integer y = x + j;
- Integer yp = x.modAdd(j, 3);
- for (yy = y; yy >= 3; yy -= 3)
- ;
- TS_ASSERT(yp == yy);
- yp = x.modAdd(j, 7);
- for (yy = y; yy >= 7; yy -= 7)
- ;
- TS_ASSERT(yp == yy);
- yp = x.modAdd(j, 11);
- for (yy = y; yy >= 11; yy -= 11)
- ;
- TS_ASSERT(yp == yy);
- }
- }
- }
-
- void testModMultiply()
- {
- for (unsigned i = 0; i <= 10; ++i)
- {
- for (unsigned j = 0; j <= 10; ++j)
- {
- Integer yy;
- Integer x(i);
- Integer y = x * j;
- Integer yp = x.modMultiply(j, 3);
- for (yy = y; yy >= 3; yy -= 3)
- ;
- TS_ASSERT(yp == yy);
- yp = x.modMultiply(j, 7);
- for (yy = y; yy >= 7; yy -= 7)
- ;
- TS_ASSERT(yp == yy);
- yp = x.modMultiply(j, 11);
- for (yy = y; yy >= 11; yy -= 11)
- ;
- TS_ASSERT(yp == yy);
- }
- }
- }
-
- void testModInverse()
- {
- for (unsigned i = 0; i <= 10; ++i)
- {
- Integer x(i);
- Integer inv = x.modInverse(3);
- if (i == 0 || i == 3 || i == 6 || i == 9)
- {
- TS_ASSERT(inv == -1); /* no inverse */
- }
- else
- {
- TS_ASSERT(x.modMultiply(inv, 3) == 1);
- }
- inv = x.modInverse(7);
- if (i == 0 || i == 7)
- {
- TS_ASSERT(inv == -1); /* no inverse */
- }
- else
- {
- TS_ASSERT(x.modMultiply(inv, 7) == 1);
- }
- inv = x.modInverse(11);
- if (i == 0)
- {
- TS_ASSERT(inv == -1); /* no inverse */
- }
- else
- {
- TS_ASSERT(x.modMultiply(inv, 11) == 1);
- }
- }
- }
-};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback