diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-18 22:18:27 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-18 22:18:27 +0000 |
| commit | 436c124105897977cec7a7f11c716f678dd3b7a5 (patch) | |
| tree | 491de3a87eb462a218ce4bfadd1a311ef6dfb2a0 /src/theory | |
| parent | a850215587ed07a536f77333c729b32966881716 (diff) | |
Fixed bug in rewriter
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 111 |
1 files changed, 57 insertions, 54 deletions
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index d59ef736d..5de9d225f 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -53,36 +53,39 @@ public: break; } val = eqRewritten.getConst<bool>(); - if (val) { - // select(store(a,i,v),i) = v - return RewriteResponse(REWRITE_DONE, store[2]); - } - else { - // select(store(a,i,v),j) = select(a,j) if i /= j - store = store[0]; - Node n; - while (store.getKind() == kind::STORE) { - if (index == store[1]) { - val = true; - } - else if (index.isConst() && store[1].isConst()) { - val = false; - } - else { - n = Rewriter::rewrite(store[1].eqNode(index)); - if (n.getKind() != kind::CONST_BOOLEAN) { - break; - } - val = n.getConst<bool>(); - } - if (val) { - return RewriteResponse(REWRITE_DONE, store[2]); + } + if (val) { + // select(store(a,i,v),i) = v + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store[2] << std::endl; + return RewriteResponse(REWRITE_DONE, store[2]); + } + else { + // select(store(a,i,v),j) = select(a,j) if i /= j + store = store[0]; + Node n; + while (store.getKind() == kind::STORE) { + if (index == store[1]) { + val = true; + } + else if (index.isConst() && store[1].isConst()) { + val = false; + } + else { + n = Rewriter::rewrite(store[1].eqNode(index)); + if (n.getKind() != kind::CONST_BOOLEAN) { + break; } - store = store[0]; + val = n.getConst<bool>(); } - n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index); - return RewriteResponse(REWRITE_DONE, n); + if (val) { + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store[2] << std::endl; + return RewriteResponse(REWRITE_DONE, store[2]); + } + store = store[0]; } + n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index); + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl; + return RewriteResponse(REWRITE_DONE, n); } } break; @@ -202,36 +205,36 @@ public: break; } val = eqRewritten.getConst<bool>(); - if (val) { - // select(store(a,i,v),i) = v - return RewriteResponse(REWRITE_DONE, store[2]); - } - else { - // select(store(a,i,v),j) = select(a,j) if i /= j - store = store[0]; - Node n; - while (store.getKind() == kind::STORE) { - if (index == store[1]) { - val = true; - } - else if (index.isConst() && store[1].isConst()) { - val = false; - } - else { - n = Rewriter::rewrite(store[1].eqNode(index)); - if (n.getKind() != kind::CONST_BOOLEAN) { - break; - } - val = n.getConst<bool>(); - } - if (val) { - return RewriteResponse(REWRITE_DONE, store[2]); + } + if (val) { + // select(store(a,i,v),i) = v + return RewriteResponse(REWRITE_DONE, store[2]); + } + else { + // select(store(a,i,v),j) = select(a,j) if i /= j + store = store[0]; + Node n; + while (store.getKind() == kind::STORE) { + if (index == store[1]) { + val = true; + } + else if (index.isConst() && store[1].isConst()) { + val = false; + } + else { + n = Rewriter::rewrite(store[1].eqNode(index)); + if (n.getKind() != kind::CONST_BOOLEAN) { + break; } - store = store[0]; + val = n.getConst<bool>(); } - n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index); - return RewriteResponse(REWRITE_DONE, n); + if (val) { + return RewriteResponse(REWRITE_DONE, store[2]); + } + store = store[0]; } + n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index); + return RewriteResponse(REWRITE_DONE, n); } } break; |