diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-14 13:35:53 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-14 13:35:53 -0600 |
| commit | e16ab44a2b4622bb5745633cbafd43a0023a518c (patch) | |
| tree | d980bdc3dc771abfc8101036d1e2aaebc8020134 /src/theory/arith/arith_rewriter.cpp | |
| parent | ad34df900d79aad64558b354a866870715bfd007 (diff) | |
| parent | effb0d47ba5bfaebae17dcd06153489dccd90eff (diff) | |
Merge branch 'master' into cav22-stringscav22-strings
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); } } } |