From 2635899db4a7622a206e2ec562d01e3337a92199 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 25 May 2010 21:45:18 +0000 Subject: [PATCH] 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. --- src/theory/arith/arith_rewriter.cpp | 35 ++++++++++++++++++++--------- src/util/integer.h | 2 +- src/util/rational.h | 18 ++++++++++++++- test/unit/expr/node_manager_black.h | 4 ++-- test/unit/expr/node_manager_white.h | 2 +- test/unit/util/integer_black.h | 6 +++++ test/unit/util/rational_white.h | 6 +++++ 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::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& variables){ NodeBuilder<> nb(kind::MULT); nb << mkRationalNode(c); + for(std::set::iterator i = variables.begin(); i != variables.end(); ++i){ nb << *i; } @@ -312,22 +316,31 @@ Node ArithRewriter::rewriteMult(TNode t){ Rational accumulator(1,1); set variables; vector sums; - stack > mult_iterators; - mult_iterators.push(make_pair(t, t.begin())); - while(!mult_iterators.empty()){ - pair p = mult_iterators.top(); - mult_iterators.pop(); + //These stacks need to be kept in lock step + stack mult_iterators_nodes; + stack 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) { @@ -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 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(),i); } void testMkConstRat() { - Rational r = "3/2"; + Rational r("3/2"); Node n = d_nodeManager->mkConst(r); TS_ASSERT_EQUALS(n.getConst(),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()); -- 2.30.2