diff options
| author | Tim King <taking@cs.nyu.edu> | 2010-05-28 22:09:08 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2010-05-28 22:09:08 +0000 |
| commit | 07f9271bf426f9ed40bd0d01e4e77a17fa217e23 (patch) | |
| tree | 2d7772ece2b4b98aac323c762e197fd204fdc392 /src/theory/arith | |
| parent | ff066aebdc624a835c00414dd8ef56f70ad3aab2 (diff) | |
Bug fixes for combining coefficients of rewritten nodes.
Diffstat (limited to 'src/theory/arith')
| -rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 10 | ||||
| -rw-r--r-- | src/theory/arith/arith_rewriter.h | 1 |
2 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 922110765..312e1c6ea 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -189,7 +189,7 @@ Node addMatchingPnfs(TNode p0, TNode p1){ Rational addedC = c0 + c1; Node newC = mkRationalNode(addedC); - NodeBuilder<> nb(kind::PLUS); + NodeBuilder<> nb(kind::MULT); nb << newC; for(unsigned i=1; i <= M; ++i){ nb << p0[i]; @@ -198,7 +198,7 @@ Node addMatchingPnfs(TNode p0, TNode p1){ return newPnf; } -void sortAndCombineCoefficients(std::vector<Node>& pnfs){ +void ArithRewriter::sortAndCombineCoefficients(std::vector<Node>& pnfs){ using namespace std; /* combined contains exactly 1 representative per for each pnf. @@ -224,7 +224,10 @@ void sortAndCombineCoefficients(std::vector<Node>& pnfs){ pnfs.clear(); for(PnfSet::iterator i=combined.begin(); i != combined.end(); ++i){ Node pnf = *i; - pnfs.push_back(pnf); + if(pnf[0].getConst<Rational>() != d_constants->d_ZERO){ + //after combination the coefficient may be zero + pnfs.push_back(pnf); + } } } @@ -537,6 +540,7 @@ Node ArithRewriter::rewrite(TNode n){ }else{ n.setAttribute(NormalForm(), res); } + Debug("arithrewriter") << "Trace rewrite:" << n << "|->"<< res << std::endl; return res; } diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 611077038..6388c7031 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -85,6 +85,7 @@ private: Node multPnfByNonZero(TNode pnf, Rational& q); Node rewriteConstantDiv(TNode t); + void sortAndCombineCoefficients(std::vector<Node>& pnfs); public: |