diff options
| author | Tim King <taking@cs.nyu.edu> | 2014-06-24 19:19:58 -0400 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2014-06-24 19:19:58 -0400 |
| commit | 7e5245639848594e5ff72a5104c340defe4aac7c (patch) | |
| tree | 07907e9fbad0450322ca85a69b25cf37bbbf2ec2 /src/theory/arith/arith_ite_utils.cpp | |
| parent | 7346e80b4f443b2449a0d211b657e2929e065d62 (diff) | |
Alternative lazier heuristic for assertion rewriting.
Diffstat (limited to 'src/theory/arith/arith_ite_utils.cpp')
| -rw-r--r-- | src/theory/arith/arith_ite_utils.cpp | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index d3702ccd8..fa631a527 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -308,9 +308,6 @@ void ArithIteUtils::addImplications(Node x, Node y){ // (=> (not x) y) // (=> (not y) x) - x = Rewriter::rewrite(x); - y = Rewriter::rewrite(y); - Node xneg = x.negate(); Node yneg = y.negate(); d_implies[xneg].insert(y); @@ -431,7 +428,7 @@ bool ArithIteUtils::solveBinOr(TNode binor){ NodeManager* nm = NodeManager::currentNM(); - Node cnd = findIteCnd(l, r); + Node cnd = findIteCnd(binor[0], binor[1]); Node sk = nm->mkSkolem("deor", nm->booleanType()); Node ite = sk.iteNode(otherL, otherR); |