diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-08 21:25:27 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-08 21:25:27 +0000 |
commit | b3470b5e0b7a664443b9f835db5dd86fb1487866 (patch) | |
tree | cbfe76629fc1de740b552e574a058906eb4f2321 /src/theory/arith/arith_rewriter.cpp | |
parent | 2d422bab11e46f056bfafa85b0d49282fec289d8 (diff) |
Improved support for division by zero. This adds the *_TOTAL kinds and uninterpreted functions for division by 0.
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 87 |
1 files changed, 64 insertions, 23 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 27014a3bf..b6275ba24 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -86,25 +86,50 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ return rewriteUMinus(t, true); }else if(t.getKind() == kind::DIVISION){ return RewriteResponse(REWRITE_DONE, t); // wait until t[1] is rewritten + }else if(t.getKind() == kind::DIVISION_TOTAL){ + if(t[1].getKind()== kind::CONST_RATIONAL && + t[1].getConst<Rational>().isZero()){ + return RewriteResponse(REWRITE_DONE, mkRationalNode(0)); + }else{ + return RewriteResponse(REWRITE_DONE, t); // wait until t[1] is rewritten + } }else if(t.getKind() == kind::PLUS){ return preRewritePlus(t); }else if(t.getKind() == kind::MULT){ return preRewriteMult(t); }else if(t.getKind() == kind::INTS_DIVISION){ Rational intOne(1); - if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst<Rational>() == intOne){ + if(t[1].getKind()== kind::CONST_RATIONAL && + t[1].getConst<Rational>().isOne()){ return RewriteResponse(REWRITE_AGAIN, t[0]); }else{ return RewriteResponse(REWRITE_DONE, t); } + }else if(t.getKind() == kind::INTS_DIVISION_TOTAL){ + if(t[1].getKind()== kind::CONST_RATIONAL){ + Rational intOne(1), intZero(0); + if(t[1].getConst<Rational>().isOne()){ + return RewriteResponse(REWRITE_AGAIN, t[0]); + } else if(t[1].getConst<Rational>().isZero()){ + return RewriteResponse(REWRITE_DONE, mkRationalNode(0)); + } + } + return RewriteResponse(REWRITE_DONE, t); }else if(t.getKind() == kind::INTS_MODULUS){ Rational intOne(1); - if(t[1].getKind()== kind::CONST_RATIONAL && t[1].getConst<Rational>() == intOne){ - Rational intZero(0); - return RewriteResponse(REWRITE_AGAIN, mkRationalNode(intZero)); + if(t[1].getKind()== kind::CONST_RATIONAL && + t[1].getConst<Rational>().isOne()){ + return RewriteResponse(REWRITE_AGAIN, mkRationalNode(0)); }else{ return RewriteResponse(REWRITE_DONE, t); } + }else if(t.getKind() == kind::INTS_MODULUS_TOTAL){ + if(t[1].getKind()== kind::CONST_RATIONAL){ + if(t[1].getConst<Rational>().isOne() || t[1].getConst<Rational>().isZero()){ + return RewriteResponse(REWRITE_DONE, mkRationalNode(0)); + } + } + return RewriteResponse(REWRITE_DONE, t); }else{ Unreachable(); } @@ -118,16 +143,24 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ return rewriteMinus(t, false); }else if(t.getKind() == kind::UMINUS){ return rewriteUMinus(t, false); - }else if(t.getKind() == kind::DIVISION){ - return rewriteDivByConstant(t, false); + }else if(t.getKind() == kind::DIVISION || + t.getKind() == kind::DIVISION_TOTAL){ + return rewriteDiv(t, false); }else if(t.getKind() == kind::PLUS){ return postRewritePlus(t); }else if(t.getKind() == kind::MULT){ return postRewriteMult(t); - }else if(t.getKind() == kind::INTS_DIVISION){ - return RewriteResponse(REWRITE_DONE, t); - }else if(t.getKind() == kind::INTS_MODULUS){ + }else if(t.getKind() == kind::INTS_DIVISION || + t.getKind() == kind::INTS_MODULUS){ return RewriteResponse(REWRITE_DONE, t); + }else if(t.getKind() == kind::INTS_DIVISION_TOTAL || + t.getKind() == kind::INTS_MODULUS_TOTAL){ + if(t[1].getKind() == kind::CONST_RATIONAL && + t[1].getConst<Rational>().isZero()){ + return RewriteResponse(REWRITE_DONE, mkRationalNode(0)); + }else{ + return RewriteResponse(REWRITE_DONE, t); + } }else{ Unreachable(); } @@ -272,27 +305,35 @@ Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){ return diff; } -RewriteResponse ArithRewriter::rewriteDivByConstant(TNode t, bool pre){ - Assert(t.getKind()== kind::DIVISION); +RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre){ + Assert(t.getKind()== kind::DIVISION || t.getKind() == kind::DIVISION_TOTAL); Node left = t[0]; Node right = t[1]; - Assert(right.getKind()== kind::CONST_RATIONAL); - - - const Rational& den = right.getConst<Rational>(); - - Assert(den != Rational(0)); + if(right.getKind() == kind::CONST_RATIONAL){ + const Rational& den = right.getConst<Rational>(); + + if(den.isZero()){ + if(t.getKind() == kind::DIVISION_TOTAL){ + return RewriteResponse(REWRITE_DONE, mkRationalNode(0)); + }else{ + return RewriteResponse(REWRITE_DONE, t); + } + } + Assert(den != Rational(0)); - Rational div = den.inverse(); + Rational div = den.inverse(); - Node result = mkRationalNode(div); + Node result = mkRationalNode(div); - Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result); - if(pre){ - return RewriteResponse(REWRITE_DONE, mult); + Node mult = NodeManager::currentNM()->mkNode(kind::MULT,left,result); + if(pre){ + return RewriteResponse(REWRITE_DONE, mult); + }else{ + return RewriteResponse(REWRITE_AGAIN, mult); + } }else{ - return RewriteResponse(REWRITE_AGAIN, mult); + return RewriteResponse(REWRITE_DONE, t); } } |