From: Tim King <taking@cs.nyu.edu>
Date: Fri, 28 May 2010 22:09:08 +0000 (+0000)
Subject: Bug fixes for combining coefficients of rewritten nodes.
X-Git-Tag: cvc5-1.0.0~9024
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=07f9271bf426f9ed40bd0d01e4e77a17fa217e23;p=cvc5.git

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 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: