test/unit/util/integer_black.h

   1 /*********************                                                        */
   2 /*! \file integer_black.h
   3  ** \verbatim
   4  ** Original author: taking
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): cconway, mdeters
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Black box testing of CVC4::Integer.
  15  **
  16  ** Black box testing of CVC4::Integer.
  17  **/
  18
  19 #include <cxxtest/TestSuite.h>
  20 #include <sstream>
  21
  22 #include "util/integer.h"
  23
  24 using namespace CVC4;
  25 using namespace std;
  26
  27 const char* largeVal = "4547897890548754897897897897890789078907890";
  28
  29 class IntegerBlack : public CxxTest::TestSuite {
  30
  31
  32 public:
  33
  34   void testConstructors() {
  35     Integer z0(1);
  36     TS_ASSERT_EQUALS(z0.getLong(), 1);
  37
  38     Integer z1(0);
  39     TS_ASSERT_EQUALS(z1.getLong(), 0);
  40
  41     Integer z2(-1);
  42     TS_ASSERT_EQUALS(z2.getLong(), -1);
  43
  44     Integer z3(0x890UL);
  45     TS_ASSERT_EQUALS(z3.getUnsignedLong(), 0x890UL);
  46
  47     Integer z4;
  48     TS_ASSERT_EQUALS(z4.getLong(), 0);
  49
  50     Integer z5("7896890");
  51     TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890ul);
  52
  53     Integer z6(z5);
  54     TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890ul);
  55     TS_ASSERT_EQUALS(z6.getUnsignedLong(), 7896890ul);
  56
  57
  58     string bigValue("1536729");
  59     Integer z7(bigValue);
  60     TS_ASSERT_EQUALS(z7.getUnsignedLong(), 1536729ul);
  61   }
  62
  63   void testCompareAgainstZero(){
  64     Integer z(0);
  65     TS_ASSERT_THROWS_NOTHING(z == 0;);
  66     TS_ASSERT_EQUALS(z,0);
  67   }
  68
  69   void testOperatorAssign(){
  70     Integer x(0);
  71     Integer y(79);
  72     Integer z(45789);
  73
  74     TS_ASSERT_EQUALS(x.getUnsignedLong(), 0ul);
  75     TS_ASSERT_EQUALS(y.getUnsignedLong(), 79ul);
  76     TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
  77
  78     x = y = z;
  79
  80     TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789ul);
  81     TS_ASSERT_EQUALS(y.getUnsignedLong(), 45789ul);
  82     TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
  83
  84     Integer a(2);
  85
  86     y = a;
  87
  88     TS_ASSERT_EQUALS(a.getUnsignedLong(), 2ul);
  89     TS_ASSERT_EQUALS(y.getUnsignedLong(), 2ul);
  90     TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789ul);
  91     TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
  92   }
  93
  94   void testOperatorEquals(){
  95     Integer a(0);
  96     Integer b(79);
  97     Integer c("79");
  98     Integer d;
  99
 100     TS_ASSERT( (a==a));
 101     TS_ASSERT(!(a==b));
 102     TS_ASSERT(!(a==c));
 103     TS_ASSERT( (a==d));
 104
 105     TS_ASSERT(!(b==a));
 106     TS_ASSERT( (b==b));
 107     TS_ASSERT( (b==c));
 108     TS_ASSERT(!(b==d));
 109
 110     TS_ASSERT(!(c==a));
 111     TS_ASSERT( (c==b));
 112     TS_ASSERT( (c==c));
 113     TS_ASSERT(!(c==d));
 114
 115     TS_ASSERT( (d==a));
 116     TS_ASSERT(!(d==b));
 117     TS_ASSERT(!(d==c));
 118     TS_ASSERT( (d==d));
 119
 120   }
 121
 122   void testOperatorNotEquals(){
 123     Integer a(0);
 124     Integer b(79);
 125     Integer c("79");
 126     Integer d;
 127
 128     TS_ASSERT(!(a!=a));
 129     TS_ASSERT( (a!=b));
 130     TS_ASSERT( (a!=c));
 131     TS_ASSERT(!(a!=d));
 132
 133     TS_ASSERT( (b!=a));
 134     TS_ASSERT(!(b!=b));
 135     TS_ASSERT(!(b!=c));
 136     TS_ASSERT( (b!=d));
 137
 138     TS_ASSERT( (c!=a));
 139     TS_ASSERT(!(c!=b));
 140     TS_ASSERT(!(c!=c));
 141     TS_ASSERT( (c!=d));
 142
 143     TS_ASSERT(!(d!=a));
 144     TS_ASSERT( (d!=b));
 145     TS_ASSERT( (d!=c));
 146     TS_ASSERT(!(d!=d));
 147
 148   }
 149
 150   void testOperatorSubtract(){
 151     Integer x(0);
 152     Integer y(79);
 153     Integer z(-34);
 154
 155
 156     Integer act0 = x - x;
 157     Integer act1 = x - y;
 158     Integer act2 = x - z;
 159     Integer exp0(0);
 160     Integer exp1(-79);
 161     Integer exp2(34);
 162
 163
 164     Integer act3 = y - x;
 165     Integer act4 = y - y;
 166     Integer act5 = y - z;
 167     Integer exp3(79);
 168     Integer exp4(0);
 169     Integer exp5(113);
 170
 171
 172     Integer act6 = z - x;
 173     Integer act7 = z - y;
 174     Integer act8 = z - z;
 175     Integer exp6(-34);
 176     Integer exp7(-113);
 177     Integer exp8(0);
 178
 179
 180
 181     TS_ASSERT_EQUALS(act0, exp0);
 182     TS_ASSERT_EQUALS(act1, exp1);
 183     TS_ASSERT_EQUALS(act2, exp2);
 184     TS_ASSERT_EQUALS(act3, exp3);
 185     TS_ASSERT_EQUALS(act4, exp4);
 186     TS_ASSERT_EQUALS(act5, exp5);
 187     TS_ASSERT_EQUALS(act6, exp6);
 188     TS_ASSERT_EQUALS(act7, exp7);
 189     TS_ASSERT_EQUALS(act8, exp8);
 190   }
 191   void testOperatorAdd(){
 192     Integer x(0);
 193     Integer y(79);
 194     Integer z(-34);
 195
 196
 197     Integer act0 = x + x;
 198     Integer act1 = x + y;
 199     Integer act2 = x + z;
 200     Integer exp0(0);
 201     Integer exp1(79);
 202     Integer exp2(-34);
 203
 204
 205     Integer act3 = y + x;
 206     Integer act4 = y + y;
 207     Integer act5 = y + z;
 208     Integer exp3(79);
 209     Integer exp4(158);
 210     Integer exp5(45);
 211
 212
 213     Integer act6 = z + x;
 214     Integer act7 = z + y;
 215     Integer act8 = z + z;
 216     Integer exp6(-34);
 217     Integer exp7(45);
 218     Integer exp8(-68);
 219
 220
 221
 222     TS_ASSERT_EQUALS(act0, exp0);
 223     TS_ASSERT_EQUALS(act1, exp1);
 224     TS_ASSERT_EQUALS(act2, exp2);
 225     TS_ASSERT_EQUALS(act3, exp3);
 226     TS_ASSERT_EQUALS(act4, exp4);
 227     TS_ASSERT_EQUALS(act5, exp5);
 228     TS_ASSERT_EQUALS(act6, exp6);
 229     TS_ASSERT_EQUALS(act7, exp7);
 230     TS_ASSERT_EQUALS(act8, exp8);
 231   }
 232
 233   void testOperatorMult(){
 234     Integer x(0);
 235     Integer y(79);
 236     Integer z(-34);
 237
 238
 239     Integer act0 = x * x;
 240     Integer act1 = x * y;
 241     Integer act2 = x * z;
 242     Integer exp0(0);
 243     Integer exp1(0);
 244     Integer exp2(0);
 245
 246
 247     Integer act3 = y * x;
 248     Integer act4 = y * y;
 249     Integer act5 = y * z;
 250     Integer exp3(0);
 251     Integer exp4(6241);
 252     Integer exp5(-2686);
 253
 254
 255     Integer act6 = z * x;
 256     Integer act7 = z * y;
 257     Integer act8 = z * z;
 258     Integer exp6(0);
 259     Integer exp7(-2686);
 260     Integer exp8(1156);
 261
 262
 263
 264     TS_ASSERT_EQUALS(act0, exp0);
 265     TS_ASSERT_EQUALS(act1, exp1);
 266     TS_ASSERT_EQUALS(act2, exp2);
 267     TS_ASSERT_EQUALS(act3, exp3);
 268     TS_ASSERT_EQUALS(act4, exp4);
 269     TS_ASSERT_EQUALS(act5, exp5);
 270     TS_ASSERT_EQUALS(act6, exp6);
 271     TS_ASSERT_EQUALS(act7, exp7);
 272     TS_ASSERT_EQUALS(act8, exp8);
 273   }
 274
 275
 276   void testToStringStuff(){
 277     stringstream ss;
 278     Integer large (largeVal);
 279     ss << large;
 280     string res = ss.str();
 281
 282     TS_ASSERT_EQUALS(res, large.toString());
 283   }
 284
 285   void testPow() {
 286     TS_ASSERT_EQUALS( Integer(1), Integer(1).pow(0) );
 287     TS_ASSERT_EQUALS( Integer(1), Integer(5).pow(0) );
 288     TS_ASSERT_EQUALS( Integer(1), Integer(-1).pow(0) );
 289     TS_ASSERT_EQUALS( Integer(0), Integer(0).pow(1) );
 290     TS_ASSERT_EQUALS( Integer(5), Integer(5).pow(1) );
 291     TS_ASSERT_EQUALS( Integer(-5), Integer(-5).pow(1) );
 292     TS_ASSERT_EQUALS( Integer(16), Integer(2).pow(4) );
 293     TS_ASSERT_EQUALS( Integer(16), Integer(-2).pow(4) );
 294     TS_ASSERT_EQUALS( Integer(1000), Integer(10).pow(3) );
 295     TS_ASSERT_EQUALS( Integer(-1000), Integer(-10).pow(3) );
 296   }
 297 };