diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-29 21:55:51 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-29 19:55:51 -0700 |
commit | 8c794ae1009bf8515b965c1023de188f50b35d60 (patch) | |
tree | 7dcf7bed2aa581fb806c8b23efe77c33f6632754 /src/theory/arith/arith_rewriter.cpp | |
parent | 19054b3b1d427e662d30d4322df2b2f2361353da (diff) |
Add internal support for integer and operator (#4668)
Towards merging iand branch to master. This adds internal support for an "integer AND" operator.
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 50 |
1 files changed, 46 insertions, 4 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index e50b79bbc..188ef47e6 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -25,6 +25,7 @@ #include "theory/arith/arith_utilities.h" #include "theory/arith/normal_form.h" #include "theory/theory.h" +#include "util/iand.h" namespace CVC4 { namespace theory { @@ -101,8 +102,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::PLUS: return preRewritePlus(t); case kind::MULT: - case kind::NONLINEAR_MULT: - return preRewriteMult(t); + case kind::NONLINEAR_MULT: return preRewriteMult(t); + case kind::IAND: return RewriteResponse(REWRITE_DONE, t); case kind::EXPONENTIAL: case kind::SINE: case kind::COSINE: @@ -165,8 +166,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ case kind::PLUS: return postRewritePlus(t); case kind::MULT: - case kind::NONLINEAR_MULT: - return postRewriteMult(t); + case kind::NONLINEAR_MULT: return postRewriteMult(t); + case kind::IAND: return postRewriteIAnd(t); case kind::EXPONENTIAL: case kind::SINE: case kind::COSINE: @@ -371,6 +372,47 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ return RewriteResponse(REWRITE_DONE, res.getNode()); } +RewriteResponse ArithRewriter::postRewriteIAnd(TNode t) +{ + Assert(t.getKind() == kind::IAND); + 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]); + Node bvand = nm->mkNode(kind::BITVECTOR_AND, arg1, arg2); + Node ret = nm->mkNode(kind::BITVECTOR_TO_NAT, bvand); + return RewriteResponse(REWRITE_AGAIN_FULL, ret); + } + else if (t[0] > t[1]) + { + // ((_ iand k) x y) ---> ((_ iand k) y x) if x > y by node ordering + Node ret = nm->mkNode(kind::IAND, t.getOperator(), t[1], t[0]); + return RewriteResponse(REWRITE_AGAIN, ret); + } + else if (t[0] == t[1]) + { + // ((_ iand k) x x) ---> x + return RewriteResponse(REWRITE_DONE, t[0]); + } + // simplifications involving constants + for (unsigned i = 0; i < 2; i++) + { + if (!t[i].isConst()) + { + continue; + } + if (t[i].getConst<Rational>().sgn() == 0) + { + // ((_ iand k) 0 y) ---> 0 + return RewriteResponse(REWRITE_DONE, t[i]); + } + } + return RewriteResponse(REWRITE_DONE, t); +} RewriteResponse ArithRewriter::preRewriteTranscendental(TNode t) { return RewriteResponse(REWRITE_DONE, t); |