From f3682605175f1deb62f5390c5e39ccfba0b170fd Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Wed, 22 Aug 2012 18:04:10 +0000 Subject: [PATCH] More progress on array constants. Here's a fun way to give yourself a week-long headache: try to figure out how to write efficient code to normalize array constants. It's mostly there now - just need to figure out how to use type enumerators and update once the new cardinality stuff is in place. --- src/theory/arrays/theory_arrays_rewriter.h | 287 +++++++++++++++---- src/theory/arrays/theory_arrays_type_rules.h | 72 +++-- 2 files changed, 264 insertions(+), 95 deletions(-) diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index ba2baab2c..50a5ee2d0 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -30,6 +30,169 @@ namespace arrays { class TheoryArraysRewriter { + static Node normalizeConstant(TNode node) { + TNode store = node[0]; + TNode index = node[1]; + TNode value = node[2]; + + std::vector indices; + std::vector elements; + + // Normal form for nested stores is just ordering by index - but also need + // to check if we are writing to default value + + // Go through nested stores looking for where to insert index + // Also check whether we are replacing an existing store + TNode replacedValue; + Integer depth = 1; + Integer valCount = 1; + while (store.getKind() == kind::STORE) { + if (index == store[1]) { + replacedValue = store[2]; + store = store[0]; + break; + } + else if (!(index < store[1])) { + break; + } + if (value == store[2]) { + valCount += 1; + } + depth += 1; + indices.push_back(store[1]); + elements.push_back(store[2]); + store = store[0]; + } + Node n = store; + + // Get the default value at the bottom of the nested stores + while (store.getKind() == kind::STORE) { + if (value == store[2]) { + valCount += 1; + } + depth += 1; + store = store[0]; + } + Assert(store.getKind() == kind::STORE_ALL); + ArrayStoreAll storeAll = store.getConst(); + Node defaultValue = Node::fromExpr(storeAll.getExpr()); + NodeManager* nm = NodeManager::currentNM(); + + // Check if we are writing to default value - if so the store + // to index can be ignored + if (value == defaultValue) { + if (replacedValue.isNull()) { + // Quick exit - if writing to default value and nothing was + // replaced, we can just return node[0] + return node[0]; + } + } + else { + n = nm->mkNode(kind::STORE, n, index, value); + } + + // Build the rest of the store after inserting/deleting + while (!indices.empty()) { + n = nm->mkNode(kind::STORE, n, indices.back(), elements.back()); + indices.pop_back(); + elements.pop_back(); + } + + Cardinality indexCard = index.getType().getCardinality(); + if (indexCard.isInfinite()) { + return n; + } + + // When index sort is finite, we have to check whether there is any value + // that is written to more than the default value. If so, it must become + // the new default value + + TNode mostFrequentValue; + Integer mostFrequentValueCount = 0; + bool recompute = false; + if (node[0].getKind() == kind::STORE) { + // TODO: look up most frequent value and count + if (!replacedValue.isNull() && mostFrequentValue == replacedValue) { + recompute = true; + } + } + + // Compute the most frequently written value for n + if (valCount > mostFrequentValueCount || + (valCount == mostFrequentValueCount && value < mostFrequentValue)) { + mostFrequentValue = value; + mostFrequentValueCount = valCount; + recompute = false; + } + + // Need to make sure the default value count is larger, or the same and the default value is expression-order-less-than nextValue + int compare;// = indexCard.compare(mostFrequentValueCount + depth); + // Assert result of compare is not unknown + if (compare > 0 || + (compare == 0 && (defaultValue < mostFrequentValue))) { + return n; + } + + // Bad case: have to recompute value counts and/or possibly switch out + // default value + store = n; + std::hash_set indexSet; + std::hash_map elementsMap; + std::hash_map::iterator it; + unsigned count; + unsigned max = 0; + TNode maxValue; + while (store.getKind() == kind::STORE) { + indices.push_back(store[1]); + indexSet.insert(store[1]); + elements.push_back(store[2]); + it = elementsMap.find(store[2]); + if (it != elementsMap.end()) { + (*it).second = (*it).second + 1; + count = (*it).second; + } + else { + elementsMap[store[2]] = 1; + count = 1; + } + if (count > max || + (count == max && store[2] < maxValue)) { + max = count; + maxValue = store[2]; + } + store = store[0]; + } + + Assert(depth == indices.size()); + //compare = indexCard.compare(max + depth); + // Assert result of compare is not unknown + if (compare > 0 || + (compare == 0 && (defaultValue < maxValue))) { + Assert(recompute); + return n; + } + + // Out of luck: have to swap out default value + std::vector newIndices; + // Enumerate values from index type into newIndices and sort + + //n = storeAll(maxValue) + while (!newIndices.empty() || !indices.empty()) { + if (!newIndices.empty() && (indices.empty() || newIndices.back() < indices.back())) { + n = nm->mkNode(kind::STORE, n, newIndices.back(), defaultValue); + newIndices.pop_back(); + } + else if (newIndices.empty() || indices.back() < newIndices.back()) { + if (elements.back() != maxValue) { + n = nm->mkNode(kind::STORE, n, indices.back(), elements.back()); + } + indices.pop_back(); + elements.pop_back(); + } + } + return n; + } + public: static RewriteResponse postRewrite(TNode node) { @@ -37,21 +200,43 @@ public: switch (node.getKind()) { case kind::SELECT: { 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) { - // 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); + TNode index = node[1]; + Node n; + bool val; + 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) { + // select(store(a,i,v),j) = v if i = j + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store[2] << std::endl; + return RewriteResponse(REWRITE_DONE, store[2]); } + // select(store(a,i,v),j) = select(a,j) if i /= j + store = store[0]; + } + if (store.getKind() == kind::STORE_ALL) { + // select(store_all(v),i) = v + ArrayStoreAll storeAll = store.getConst(); + n = Node::fromExpr(storeAll.getExpr()); + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl; + Assert(n.isConst()); + return RewriteResponse(REWRITE_DONE, n); + } + else if (store != node[0]) { + n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index); + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl; + return RewriteResponse(REWRITE_DONE, n); } break; } @@ -65,9 +250,15 @@ public: Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store << std::endl; return RewriteResponse(REWRITE_DONE, store); } + TNode index = node[1]; + if (store.isConst() && index.isConst() && value.isConst()) { + // normalize constant + Node n = normalizeConstant(node); + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl; + return RewriteResponse(REWRITE_DONE, n); + } if (store.getKind() == kind::STORE) { // store(store(a,i,v),j,w) - TNode index = node[1]; bool val; if (index == store[1]) { val = true; @@ -161,10 +352,10 @@ public: 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; + TNode index = node[1]; + Node n; + bool val; + while (store.getKind() == kind::STORE) { if (index == store[1]) { val = true; } @@ -172,45 +363,32 @@ public: val = false; } else { - Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); - if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { + n = Rewriter::rewrite(store[1].eqNode(index)); + if (n.getKind() != kind::CONST_BOOLEAN) { break; } - val = eqRewritten.getConst(); + val = n.getConst(); } if (val) { - // select(store(a,i,v),i) = v + // select(store(a,i,v),j) = v if i = j Trace("arrays-prerewrite") << "Arrays::preRewrite 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; - } - val = n.getConst(); - } - if (val) { - Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store[2] << std::endl; - return RewriteResponse(REWRITE_DONE, store[2]); - } - store = store[0]; - } - n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index); - Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl; - return RewriteResponse(REWRITE_DONE, n); + return RewriteResponse(REWRITE_AGAIN, store[2]); } + // select(store(a,i,v),j) = select(a,j) if i /= j + store = store[0]; + } + if (store.getKind() == kind::STORE_ALL) { + // select(store_all(v),i) = v + ArrayStoreAll storeAll = store.getConst(); + n = Node::fromExpr(storeAll.getExpr()); + Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl; + Assert(n.isConst()); + return RewriteResponse(REWRITE_DONE, n); + } + else if (store != node[0]) { + n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index); + Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl; + return RewriteResponse(REWRITE_DONE, n); } break; } @@ -222,7 +400,7 @@ public: value[0] == store && value[1] == node[1]) { Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store << std::endl; - return RewriteResponse(REWRITE_DONE, store); + return RewriteResponse(REWRITE_AGAIN, store); } if (store.getKind() == kind::STORE) { // store(store(a,i,v),j,w) @@ -237,8 +415,7 @@ public: else { Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { - Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << node << std::endl; - return RewriteResponse(REWRITE_DONE, node); + break; } val = eqRewritten.getConst(); } @@ -255,7 +432,7 @@ public: case kind::EQUAL: case kind::IFF: { if(node[0] == node[1]) { - Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl; + Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl; return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } break; diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 9c678d6ce..f6ce84d0f 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -81,71 +81,63 @@ struct ArrayStoreTypeRule { return false; } - // If store indices are not in order, not in normal form - if (store.getKind() == kind::STORE && index < store[1]) { + // Normal form for nested stores is just ordering by index but also need to check that we are not writing + // to default value + if (store.getKind() == kind::STORE && (!(store[1] < index))) { return false; } - // Compute the number of nested stores Integer depth = 1; + Integer valCount = 1; while (store.getKind() == kind::STORE) { - store = store[0]; depth += 1; + if (store[2] == value) { + valCount += 1; + } + store = store[0]; } - - // Get the default value in the STORE_ALL object at the bottom of the nested stores Assert(store.getKind() == kind::STORE_ALL); ArrayStoreAll storeAll = store.getConst(); - TNode defaultValue /* = storeAll.getExpr().getTNode()*/ ; - - // If writing to default value, not in normal form - if (defaultValue == value) { + Node defaultValue = Node::fromExpr(storeAll.getExpr()); + if (value == defaultValue) { return false; } - + // Get the cardinality of the index type Cardinality indexCard = index.getType().getCardinality(); - // If cardinality is infinite, ok - in normal form if (indexCard.isInfinite()) { return true; } - - /* - Assert(depth <= indexCard); - - // If number of stores is equal to cardinality of index type, - // then the default value is overridden at all indices. Our normal form - // requires that the most frequent value is the default value. - if (depth == indexCard) { - return false; - } - // If the number of stores is less than half of the cardinality, then we - // know the default value is the most frequent value, so in normal form - if (depth*2 < indexCard) { - return true; - } - Integer defaultCount = indexCard - depth; + // When index sort is finite, we have to check whether there is any value + // that is written to more than the default value. If so, it is not in + // normal form. - // Have to compare number of occurrences of value with defaultValue + // Get the most frequently written value from n[0] + TNode mostFrequentValue; + Integer mostFrequentValueCount = 0; store = n[0]; - depth = 1; - while (store.getKind() == kind::STORE) { - if (store[2] == value) { - depth += 1; - } - store = store[0]; + if (store.getKind() == kind::STORE) { + // TODO: look up most frequent value and count + } + + // Compute the most frequently written value for n + if (valCount > mostFrequentValueCount || + (valCount == mostFrequentValueCount && value < mostFrequentValue)) { + mostFrequentValue = value; + mostFrequentValueCount = valCount; } - // If value occurs more frequently than the default value or the same - // and is less than defaultValue, then this is not in normal form - if (depth > defaultCount || - (depth == defaultCount && value < defaultValue)) { + // Need to make sure the default value count is larger, or the same and the default value is expression-order-less-than nextValue + int compare;// = indexCard.compare(mostFrequentValueCount + depth); + // Assert result of compare is not unknown + if (compare < 0 || + (compare == 0 && (!(defaultValue < mostFrequentValue)))) { return false; } - */ + // TODO: store mostFrequentValue and mostFrequentValueCount for this node return true; } -- 2.30.2