From 8adb4e13c5c28059ed9271522137daf341942a75 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 18 Jun 2012 19:59:56 +0000 Subject: [PATCH] Fix for slow array rewrite and minor bug fix in arrays that popped up as a result --- src/theory/arrays/theory_arrays.cpp | 4 +- src/theory/arrays/theory_arrays_rewriter.h | 281 +++++++++++++++++++-- 2 files changed, 263 insertions(+), 22 deletions(-) diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index da82e4bc3..460289439 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -770,7 +770,9 @@ Node TheoryArrays::mkAnd(std::vector& conjunctions) all.insert(t); } - Assert(all.size() > 0); + if (all.size() == 0) { + return d_true; + } if (all.size() == 1) { // All the same, or just one return *(all.begin()); diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index c6ef5cd25..d59ef736d 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -39,17 +39,49 @@ public: TNode store = node[0]; if (store.getKind() == kind::STORE) { // select(store(a,i,v),j) - Node eqRewritten = Rewriter::rewrite(store[1].eqNode(node[1])); - if (eqRewritten.getKind() == kind::CONST_BOOLEAN) { - bool value = eqRewritten.getConst(); - if (value) { + TNode index = node[1]; + bool val; + if (index == store[1]) { + val = true; + } + else if (index.isConst() && store[1].isConst()) { + val = false; + } + else { + Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); + if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { + break; + } + val = eqRewritten.getConst(); + 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 - Node newNode = NodeManager::currentNM()->mkNode(kind::SELECT, store[0], node[1]); - return RewriteResponse(REWRITE_AGAIN_FULL, newNode); + 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(); + } + if (val) { + return RewriteResponse(REWRITE_DONE, store[2]); + } + store = store[0]; + } + n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index); + return RewriteResponse(REWRITE_DONE, n); } } } @@ -66,22 +98,67 @@ public: } if (store.getKind() == kind::STORE) { // store(store(a,i,v),j,w) - Node eqRewritten = Rewriter::rewrite(store[1].eqNode(node[1])); - if (eqRewritten.getKind() == kind::CONST_BOOLEAN) { - bool val = eqRewritten.getConst(); - NodeManager* nm = NodeManager::currentNM(); - if (val) { - // store(store(a,i,v),i,w) = store(a,i,w) - Node newNode = nm->mkNode(kind::STORE, store[0], store[1], value); - return RewriteResponse(REWRITE_AGAIN_FULL, newNode); + TNode index = node[1]; + bool val; + if (index == store[1]) { + val = true; + } + else if (index.isConst() && store[1].isConst()) { + val = false; + } + else { + Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); + if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { + return RewriteResponse(REWRITE_DONE, node); } - else if (node[1] < store[1]) { - // store(store(a,i,v),j,w) = store(store(a,j,w),i,v) - // IF i != j and j comes before i in the ordering - Node newNode = nm->mkNode(kind::STORE, store[0], node[1], value); - newNode = nm->mkNode(kind::STORE, newNode, store[1], store[2]); - return RewriteResponse(REWRITE_AGAIN_FULL, newNode); + val = eqRewritten.getConst(); + } + NodeManager* nm = NodeManager::currentNM(); + if (val) { + // store(store(a,i,v),i,w) = store(a,i,w) + return RewriteResponse(REWRITE_DONE, nm->mkNode(kind::STORE, store[0], index, value)); + } + else if (index < store[1]) { + // store(store(a,i,v),j,w) = store(store(a,j,w),i,v) + // IF i != j and j comes before i in the ordering + std::vector indices; + std::vector elements; + indices.push_back(store[1]); + elements.push_back(store[2]); + 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(); + } + if (val) { + store = store[0]; + break; + } + else if (!(index < store[1])) { + break; + } + indices.push_back(store[1]); + elements.push_back(store[2]); + store = store[0]; } + n = nm->mkNode(kind::STORE, store, index, value); + while (!indices.empty()) { + n = nm->mkNode(kind::STORE, n, indices.back(), elements.back()); + indices.pop_back(); + elements.pop_back(); + } + return RewriteResponse(REWRITE_DONE, n); } } break; @@ -105,7 +182,169 @@ public: } static inline RewriteResponse preRewrite(TNode node) { - Trace("arrays-prerewrite") << "Arrays::preRewrite " << node << std::endl; + Trace("arrays-prerewrite") << "Arrays::preRewrite start " << node << std::endl; + switch (node.getKind()) { + case kind::SELECT: { + TNode store = node[0]; + if (store.getKind() == kind::STORE) { + // select(store(a,i,v),j) + TNode index = node[1]; + bool val; + if (index == store[1]) { + val = true; + } + else if (index.isConst() && store[1].isConst()) { + val = false; + } + else { + Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); + if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { + break; + } + val = eqRewritten.getConst(); + 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(); + } + 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; + } + case kind::STORE: { + TNode store = node[0]; + TNode value = node[2]; + // store(a,i,select(a,i)) = a + if (value.getKind() == kind::SELECT && + value[0] == store && + value[1] == node[1]) { + return RewriteResponse(REWRITE_DONE, store); + } + if (store.getKind() == kind::STORE) { + // store(store(a,i,v),j,w) + TNode index = node[1]; + bool val; + if (index == store[1]) { + val = true; + } + else if (index.isConst() && store[1].isConst()) { + val = false; + } + else { + Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); + if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { + return RewriteResponse(REWRITE_DONE, node); + } + val = eqRewritten.getConst(); + } + NodeManager* nm = NodeManager::currentNM(); + if (val) { + // store(store(a,i,v),i,w) = store(a,i,w) + return RewriteResponse(REWRITE_DONE, nm->mkNode(kind::STORE, store[0], index, value)); + } + else if (index.isConst() && store[1].isConst()) { + std::map elements; + elements[index] = value; + elements[store[1]] = store[2]; + store = store[0]; + Node n; + while (store.getKind() == kind::STORE) { + if (!store[1].isConst()) { + break; + } + if (elements.find(store[1]) != elements.end()) { + elements[store[1]] = store[2]; + } + store = store[0]; + } + std::map::iterator it = elements.begin(); + std::map::iterator iend = elements.end(); + for (; it != iend; ++it) { + n = nm->mkNode(kind::STORE, store, (*it).first, (*it).second); + } + return RewriteResponse(REWRITE_DONE, n); + } + else if (index < store[1]) { + // store(store(a,i,v),j,w) = store(store(a,j,w),i,v) + // IF i != j and j comes before i in the ordering + std::vector indices; + std::vector elements; + indices.push_back(store[1]); + elements.push_back(store[2]); + 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(); + } + if (val) { + store = store[0]; + break; + } + else if (!(index < store[1])) { + break; + } + indices.push_back(store[1]); + elements.push_back(store[2]); + store = store[0]; + } + n = nm->mkNode(kind::STORE, store, index, value); + while (!indices.empty()) { + n = nm->mkNode(kind::STORE, n, indices.back(), elements.back()); + indices.pop_back(); + elements.pop_back(); + } + return RewriteResponse(REWRITE_DONE, n); + } + } + break; + } + case kind::EQUAL: + case kind::IFF: { + if(node[0] == node[1]) { + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + break; + } + default: + break; + } + return RewriteResponse(REWRITE_DONE, node); } -- 2.30.2