diff options
| -rw-r--r-- | src/expr/node_value.h | 4 | ||||
| -rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 13 | ||||
| -rw-r--r-- | src/theory/rewriter.cpp | 4 |
3 files changed, 18 insertions, 3 deletions
diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 79ce8cb4f..dd5cf9a7f 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -494,7 +494,9 @@ inline NodeValue* NodeValue::getChild(int i) const { ++i; } - Assert(i >= 0 && unsigned(i) < d_nchildren); + if (!(i >= 0 && unsigned(i) < d_nchildren)) { + Assert(i >= 0 && unsigned(i) < d_nchildren); + } return d_children[i]; } diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 0faa3f3f7..8bbcacfae 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -415,11 +415,20 @@ public: template<bool Proof> static RewriteResponse postRewriteEx(TNode node, RewriteProof* proof) { + if (node.getKind() == kind::STORE) { + if (node[0].isConst() && node[1].isConst() && node[2].isConst()) { + // normalize constant + Node n = normalizeConstant(node); + Assert(n.isConst()); + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl; + return RewriteResponse(REWRITE_DONE, n); + } + } RewriteResponse r = arrays_post_applyRules<Proof>(node, NULL); /*if (r.node != node) { std::cout << node << " --> " << r.node << std::endl; }*/ - return postRewrite_(node); + return r; } static inline RewriteResponse preRewrite(TNode node) { @@ -529,7 +538,7 @@ public: /*if (r.node != node) { std::cout << node << " --> " << r.node << std::endl; }*/ - return preRewrite_(node); + return r; } static void printRewriteProof(bool use_cache, diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index a5d011e9f..02e35a46f 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -235,6 +235,10 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node, RewriteProof* rp) } else if (response.status == REWRITE_DONE) { #ifdef CVC4_ASSERTIONS RewriteResponse r2 = Rewriter::callPostRewrite(newTheoryId, response.node); + if (r2.node != response.node) { + std::cout << rewriteStackTop.node << std::endl; + std::cout << r2.node << " IS NOT EQUAL TO " << response.node << std::endl; + } Assert(r2.node == response.node); #endif rewriteStackTop.node = response.node; |