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

2 files changed, 11 insertions, 8 deletions

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);