From: Tim King <taking@cs.nyu.edu>
Date: Wed, 7 Jul 2010 16:23:22 +0000 (+0000)
Subject: Fixes arith rewriter to allow for division by a constant. It previously only allowed... 
X-Git-Tag: cvc5-1.0.0~8920
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b017f6c69c9a32e229fe3a9e8b5aeacbfc35a47;p=cvc5.git

Fixes arith rewriter to allow for division by a constant. It previously only allowed for a constant divided by a constant.
---

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 9cd65b2d9..9b10f5a62 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -435,24 +435,27 @@ Node ArithRewriter::rewriteMult(TNode t){
   }
 }
 
-Node ArithRewriter::rewriteConstantDiv(TNode t){
+Node ArithRewriter::rewriteDivByConstant(TNode t){
   Assert(t.getKind()== kind::DIVISION);
 
-  Node reLeft = rewrite(t[0]);
+  Node left = t[0];
   Node reRight = rewrite(t[1]);
-  Assert(reLeft.getKind()== kind::CONST_RATIONAL);
   Assert(reRight.getKind()== kind::CONST_RATIONAL);
 
-  Rational num = reLeft.getConst<Rational>();
+
   Rational den = reRight.getConst<Rational>();
 
   Assert(den != d_constants->d_ZERO);
 
-  Rational div = num / den;
+  Rational div = den.inverse();
 
   Node result = mkRationalNode(div);
 
-  return result;
+  Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result);
+
+  Node reMult = rewrite(mult);
+
+  return reMult;
 }
 
 Node ArithRewriter::rewriteTerm(TNode t){
@@ -465,7 +468,7 @@ Node ArithRewriter::rewriteTerm(TNode t){
   }else if(t.getKind() == kind::PLUS){
     return rewritePlus(t);
   }else if(t.getKind() == kind::DIVISION){
-    return rewriteConstantDiv(t);
+    return rewriteDivByConstant(t);
   }else if(t.getKind() == kind::MINUS){
     Node sub = makeSubtractionNode(t[0],t[1]);
     return rewrite(sub);
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 38c72d38d..a76ee6e61 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -103,7 +103,7 @@ private:
 
   Node multPnfByNonZero(TNode pnf, Rational& q);
 
-  Node rewriteConstantDiv(TNode t);
+  Node rewriteDivByConstant(TNode t);
   void sortAndCombineCoefficients(std::vector<Node>& pnfs);