Bug fixes for combining coefficients of rewritten nodes.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 92211076598c93abee0a1968351c4de8c84d8a3f..312e1c6eaa6c9d9f459bf5bbd6b49df9176191a7 100644 (file)
--- 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 61107703808681c1d4b3dee2ccbc7db91fd63ad2..6388c7031898d1c5cdb1ec7e3eb59041ecca641f 100644 (file)
--- 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: