Added Rational constructors that only take a numerator. The const char* Rational...

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 6f1df59580bdc7764608887835b318864b0febf8..9ec5c949968b8c04513db906ed645383d06f7879 100644 (file)
--- 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 c019144a9cd20eef0c0f93e158e3067df0928851..41582d8db69547c0c4c222d818f1b358397ec5fa 100644 (file)
--- 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 53a7e906058fb20237eeb5eed0ad0f44a1114306..8218984a7575be4c3ac6062e78f87a2e8d20e4e4 100644 (file)
--- 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) {
@@ -89,6 +89,22 @@ public:
     d_value.canonicalize();
   }
 
+  /**
+   * 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.
    */

diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 0e1e091784d557a1262c848399b82539369223a4..6ff2b64e056281f44bf42bdadeeb631297667890 100644 (file)
--- 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 af38c790b5aa11ed23cf50543158a077e2ca4266..7f01159220fdaf65606b91326bfcf466380db1bb 100644 (file)
--- 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 8b8faf8955936e9a05ee014a81f8440be43fce93..627167ad3a44ca43d63cab9ea3d0845e33cc462b 100644 (file)
--- 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 8a7f04fd3b4dbbd489c5b572f98a48cd047e422a..45f1301f3d83e12a9e00d2bfecb453e3cd0f7f0c 100644 (file)
--- 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());