diff options
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
| -rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 8408f15bb..af6f23c1f 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -214,7 +214,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ return RewriteResponse(REWRITE_DONE, t); case kind::TO_REAL: case kind::CAST_TO_REAL: return RewriteResponse(REWRITE_DONE, t[0]); - case kind::TO_INTEGER:return rewriteExtIntegerOp(t); + case kind::TO_INTEGER: return rewriteExtIntegerOp(t); case kind::POW: { if(t[1].getKind() == kind::CONST_RATIONAL){ @@ -402,11 +402,11 @@ RewriteResponse ArithRewriter::postRewritePow2(TNode t) RewriteResponse ArithRewriter::postRewriteIAnd(TNode t) { Assert(t.getKind() == kind::IAND); + size_t bsize = t.getOperator().getConst<IntAnd>().d_size; NodeManager* nm = NodeManager::currentNM(); // if constant, we eliminate if (t[0].isConst() && t[1].isConst()) { - size_t bsize = t.getOperator().getConst<IntAnd>().d_size; Node iToBvop = nm->mkConst(IntToBitVector(bsize)); Node arg1 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[0]); Node arg2 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[1]); @@ -437,6 +437,11 @@ RewriteResponse ArithRewriter::postRewriteIAnd(TNode t) // ((_ iand k) 0 y) ---> 0 return RewriteResponse(REWRITE_DONE, t[i]); } + if (t[i].getConst<Rational>().getNumerator() == Integer(2).pow(bsize) - 1) + { + // ((_ iand k) 111...1 y) ---> y + return RewriteResponse(REWRITE_DONE, t[i == 0 ? 1 : 0]); + } } return RewriteResponse(REWRITE_DONE, t); } @@ -511,7 +516,7 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { msum.erase(pi); if (!msum.empty()) { - rem = ArithMSum::mkNode(msum); + rem = ArithMSum::mkNode(t[0].getType(), msum); } } } |