Added GMP backed Rational and Integer classes, and white box tests for them. You may have to reconfigure after this update.

1 files changed, 276 insertions, 0 deletions

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());
+  }
+
+};