Added Rational constructors that only take a numerator. The const char* Rational and Integer constructors are now explicit. This means that 'Integer = 3;' and so on are no longer permitted. This closes bug 121.

4 files changed, 15 insertions, 3 deletions

diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 0e1e09178..6ff2b64e0 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -167,13 +167,13 @@ public:
 
 
   void testMkConstInt() {
-    Integer i = "3";
+    Integer i("3");
     Node n = d_nodeManager->mkConst(i);
     TS_ASSERT_EQUALS(n.getConst<Integer>(),i);
   }
 
   void testMkConstRat() {
-    Rational r = "3/2";
+    Rational r("3/2");
     Node n = d_nodeManager->mkConst(r);
     TS_ASSERT_EQUALS(n.getConst<Rational>(),r);
   }
diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h
index af38c790b..7f0115922 100644
--- a/test/unit/expr/node_manager_white.h
+++ b/test/unit/expr/node_manager_white.h
@@ -48,7 +48,7 @@ public:
   }
 
   void testMkConstInt() {
-    Integer i = "3";
+    Integer i("3");
     Node n = d_nm->mkConst(i);
     Node m = d_nm->mkConst(i);
     TS_ASSERT_EQUALS(n.getId(), m.getId());
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h
index 8b8faf895..627167ad3 100644
--- a/test/unit/util/integer_black.h
+++ b/test/unit/util/integer_black.h
@@ -57,6 +57,12 @@ public:
     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);
diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h
index 8a7f04fd3..45f1301f3 100644
--- a/test/unit/util/rational_white.h
+++ b/test/unit/util/rational_white.h
@@ -32,6 +32,12 @@ public:
     TS_ASSERT_THROWS_NOTHING( delete q );
   }
 
+  void testCompareAgainstZero(){
+    Rational q(0);
+    TS_ASSERT_THROWS_NOTHING(q == 0;);
+    TS_ASSERT_EQUALS(q,0);
+  }
+
   void testConstructors(){
     Rational zero; //Default constructor
     TS_ASSERT_EQUALS(0L, zero.getNumerator().getLong());