diff options
author | Tim King <taking@cs.nyu.edu> | 2010-07-07 16:23:22 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-07-07 16:23:22 +0000 |
commit | 3b017f6c69c9a32e229fe3a9e8b5aeacbfc35a47 (patch) | |
tree | f8e34bd16a03a779113cee7943299039246e4cae /src/theory/arith | |
parent | 26c1b20086b26da79d938057b7761de95fabf731 (diff) |
Fixes arith rewriter to allow for division by a constant. It previously only allowed for a constant divided by a constant.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 17 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.h | 2 |
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); |