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.

7 files changed, 57 insertions, 16 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 6f1df5958..9ec5c9499 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -265,8 +265,11 @@ Node ArithRewriter::rewritePlus(TNode t){
 
   NodeBuilder<> nb(kind::PLUS);
   nb << mkRationalNode(accumulator);
+  Debug("arithrewrite") << mkRationalNode(accumulator) << std::endl;
   for(vector<Node>::iterator i = pnfs.begin(); i != pnfs.end(); ++i){
     nb << *i;
+    Debug("arithrewrite") << (*i) << std::endl;
+
   }
 
   Node normalForm = nb;
@@ -279,6 +282,7 @@ Node ArithRewriter::rewritePlus(TNode t){
 Node toPnf(Rational& c, std::set<Node>& variables){
   NodeBuilder<> nb(kind::MULT);
   nb << mkRationalNode(c);
+
   for(std::set<Node>::iterator i = variables.begin(); i != variables.end(); ++i){
     nb << *i;
   }
@@ -312,22 +316,31 @@ Node ArithRewriter::rewriteMult(TNode t){
   Rational accumulator(1,1);
   set<Node> variables;
   vector<Node> sums;
-  stack<pair<TNode, TNode::iterator> > mult_iterators;
 
-  mult_iterators.push(make_pair(t, t.begin()));
-  while(!mult_iterators.empty()){
-    pair<TNode, TNode::iterator> p = mult_iterators.top();
-    mult_iterators.pop();
+  //These stacks need to be kept in lock step
+  stack<TNode> mult_iterators_nodes;
+  stack<unsigned> mult_iterators_iters;
+
+  mult_iterators_nodes.push(t);
+  mult_iterators_iters.push(0);
 
-    TNode mult = p.first;
-    TNode::iterator i = p.second;
+  while(!mult_iterators_nodes.empty()){
+    TNode mult = mult_iterators_nodes.top();
+    unsigned i = mult_iterators_iters.top();
 
-    for(; i!= mult.end(); ++i){
-      TNode child = *i;
+    mult_iterators_nodes.pop();
+    mult_iterators_iters.pop();
+
+
+    for(; i < mult.getNumChildren(); ++i){
+      TNode child = mult[i];
       if(child.getKind() == kind::MULT){ //TODO add not rewritten already checks
         ++i;
-        mult_iterators.push(make_pair(mult,i));
-        mult_iterators.push(make_pair(child,child.begin()));
+        mult_iterators_nodes.push(mult);
+        mult_iterators_iters.push(i);
+
+        mult_iterators_nodes.push(child);
+        mult_iterators_iters.push(0);
         break;
       }
       Node rewrittenChild = rewrite(child);
diff --git a/src/util/integer.h b/src/util/integer.h
index c019144a9..41582d8db 100644
--- a/src/util/integer.h
+++ b/src/util/integer.h
@@ -56,7 +56,7 @@ public:
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  Integer(const char * s, int base = 10): d_value(s,base) {}
+  explicit Integer(const char * s, int base = 10): d_value(s,base) {}
   Integer(const std::string& s, unsigned base = 10) : d_value(s, base) {}
 
   Integer(const Integer& q) : d_value(q.d_value) {}
diff --git a/src/util/rational.h b/src/util/rational.h
index 53a7e9060..8218984a7 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -75,7 +75,7 @@ public:
    * For more information about what is a valid rational string,
    * see GMP's documentation for mpq_set_str().
    */
-  Rational(const char * s, int base = 10): d_value(s,base) {
+  explicit Rational(const char * s, int base = 10): d_value(s,base) {
     d_value.canonicalize();
   }
   Rational(const std::string& s, unsigned base = 10) : d_value(s, base) {
@@ -90,6 +90,22 @@ public:
   }
 
   /**
+   * Constructs a canonical Rational from a numerator.
+   */
+  Rational(signed int n) : d_value(n,1) {
+    d_value.canonicalize();
+  }
+  Rational(unsigned int n) : d_value(n,1) {
+    d_value.canonicalize();
+  }
+  Rational(signed long int n) : d_value(n,1) {
+    d_value.canonicalize();
+  }
+  Rational(unsigned long int n) : d_value(n,1) {
+    d_value.canonicalize();
+  }
+
+  /**
    * Constructs a canonical Rational from a numerator and denominator.
    */
   Rational(signed int n, signed int d) : d_value(n,d) {
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());