diff options
author | Tim King <taking@cs.nyu.edu> | 2014-06-24 16:46:09 -0400 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2014-06-24 16:46:09 -0400 |
commit | 7346e80b4f443b2449a0d211b657e2929e065d62 (patch) | |
tree | 177a34c9aef712238dc5151a508ec97990fb7108 /src/theory/arith/arith_ite_utils.cpp | |
parent | 92b91586e48e5cc47ae998ecd2f9b0037a3ee174 (diff) |
Fixing a soundness bug in arithmetic and a roubustness problem in rings.
Diffstat (limited to 'src/theory/arith/arith_ite_utils.cpp')
-rw-r--r-- | src/theory/arith/arith_ite_utils.cpp | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index d5dcae726..d3702ccd8 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -308,6 +308,9 @@ 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); @@ -369,9 +372,21 @@ bool ArithIteUtils::solveBinOr(TNode binor){ Assert(binor[0].getKind() == kind::EQUAL); Assert(binor[1].getKind() == kind::EQUAL); + //Node n = Node n = applySubstitutions(binor); + if(n != binor){ + n = Rewriter::rewrite(n); + + if(!(n.getKind() == kind::OR && + n.getNumChildren() == 2 && + n[0].getKind() == kind::EQUAL && + n[1].getKind() == kind::EQUAL)){ + return false; + } + } + Assert(n.getKind() == kind::OR); - Assert(binor.getNumChildren() == 2); + Assert(n.getNumChildren() == 2); TNode l = n[0]; TNode r = n[1]; @@ -416,7 +431,7 @@ bool ArithIteUtils::solveBinOr(TNode binor){ NodeManager* nm = NodeManager::currentNM(); - Node cnd = findIteCnd(binor[0], binor[1]); + Node cnd = findIteCnd(l, r); Node sk = nm->mkSkolem("deor", nm->booleanType()); Node ite = sk.iteNode(otherL, otherR); |