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 | |
parent | 4e410b38715248f4c74539ecf51dcc01f405105c (diff) |
. '+Outstanding case split in theory arith'
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 14 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.h | 1 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 2 |
3 files changed, 11 insertions, 6 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; } diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 184844dbc..611077038 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -77,6 +77,7 @@ private: Node rewritePlus(TNode t); Node rewriteMinus(TNode t); Node makeSubtractionNode(TNode l, TNode r); + Node makeUnaryMinusNode(TNode n); Node var2pnf(TNode variable); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index bdc32ab21..6ff74f0f9 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -428,7 +428,6 @@ Node TheoryArith::simulatePreprocessing(TNode n){ }else{ Node rewritten = rewrite(n); Kind k = rewritten.getKind(); - bool negate = false; if(rewritten.getKind() == NOT){ Node sub = simulatePreprocessing(rewritten[0]); @@ -532,6 +531,7 @@ void TheoryArith::check(Effort level){ } if(enqueuedCaseSplit){ //d_out->caseSplit(); + Warning() << "Outstanding case split in theory arith" << endl; } } } |