diff options
author | Tim King <taking@cs.nyu.edu> | 2010-05-26 22:41:54 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-05-26 22:41:54 +0000 |
commit | cae87e13a782fee7dc337de70c4137c791aeaab3 (patch) | |
tree | 285a481bb8aa312090623ecdf776a9c160a78e5a /src/theory/arith/arith_rewriter.cpp | |
parent | 4e410b38715248f4c74539ecf51dcc01f405105c (diff) |
. '+Outstanding case split in theory arith'
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 0eb3f2da7..922110765 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -448,6 +448,9 @@ Node ArithRewriter::rewriteTerm(TNode t){ }else if(t.getKind() == kind::MINUS){ Node sub = makeSubtractionNode(t[0],t[1]); return rewrite(sub); + }else if(t.getKind() == kind::UMINUS){ + Node sub = makeUnaryMinusNode(t[0]); + return rewrite(sub); }else{ Unreachable(); return Node::null(); @@ -481,13 +484,14 @@ Node ArithRewriter::multPnfByNonZero(TNode pnf, Rational& q){ return result; } - +Node ArithRewriter::makeUnaryMinusNode(TNode n){ + Node tmp = NodeManager::currentNM()->mkNode(kind::MULT,d_constants->d_NEGATIVE_ONE_NODE,n); + return tmp; +} Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){ - using namespace CVC4::kind; - NodeManager* currentNM = NodeManager::currentNM(); - Node negR = currentNM->mkNode(MULT, d_constants->d_NEGATIVE_ONE_NODE, r); - Node diff = currentNM->mkNode(PLUS, l, negR); + Node negR = makeUnaryMinusNode(r); + Node diff = NodeManager::currentNM()->mkNode(kind::PLUS, l, negR); return diff; } |