diff options
author | Tim King <taking@cs.nyu.edu> | 2010-05-25 21:45:18 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-05-25 21:45:18 +0000 |
commit | 2635899db4a7622a206e2ec562d01e3337a92199 (patch) | |
tree | 43222be9c81680f93120e8e82100b8d46b821f2a /src/theory/arith | |
parent | e87c14798b99ccb586751d291b0eeb3208265bd8 (diff) |
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.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 35 |
1 files changed, 24 insertions, 11 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); |