From c0445cf73589150725ff287c1e76761268c60cec Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Thu, 23 Aug 2012 18:53:26 +0000 Subject: [PATCH] Array constant coding done except for the attributes needed --- src/theory/arrays/theory_arrays_rewriter.h | 54 +++++++++++++------- src/theory/arrays/theory_arrays_type_rules.h | 14 ++--- 2 files changed, 43 insertions(+), 25 deletions(-) diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 50a5ee2d0..50873a6a1 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -23,6 +23,7 @@ #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H #include "theory/rewriter.h" +#include "type_enumerator.h" namespace CVC4 { namespace theory { @@ -44,8 +45,8 @@ class TheoryArraysRewriter { // 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; + unsigned depth = 1; + unsigned valCount = 1; while (store.getKind() == kind::STORE) { if (index == store[1]) { replacedValue = store[2]; @@ -108,7 +109,7 @@ class TheoryArraysRewriter { // the new default value TNode mostFrequentValue; - Integer mostFrequentValueCount = 0; + unsigned mostFrequentValueCount = 0; bool recompute = false; if (node[0].getKind() == kind::STORE) { // TODO: look up most frequent value and count @@ -126,10 +127,10 @@ class TheoryArraysRewriter { } // 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))) { + Cardinality::CardinalityComparison compare = indexCard.compare(mostFrequentValueCount + depth); + Assert(compare != Cardinality::UNKNOWN); + if (compare == Cardinality::GREATER || + (compare == Cardinality::EQUAL && (defaultValue < mostFrequentValue))) { return n; } @@ -164,25 +165,42 @@ class TheoryArraysRewriter { } Assert(depth == indices.size()); - //compare = indexCard.compare(max + depth); - // Assert result of compare is not unknown - if (compare > 0 || - (compare == 0 && (defaultValue < maxValue))) { + compare = indexCard.compare(max + depth); + Assert(compare != Cardinality::UNKNOWN); + if (compare == Cardinality::GREATER || + (compare == Cardinality::EQUAL && (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 + std::vector newIndices; + TypeEnumerator te(index.getType()); + bool needToSort = false; + while (!te.isFinished()) { + if (indexSet.find(*te) == indexSet.end()) { + if (!newIndices.empty() && (!(newIndices.back() < (*te)))) { + needToSort = true; + } + newIndices.push_back(*te); + } + ++te; + } + Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL); + if (needToSort) { + std::sort(newIndices.begin(), newIndices.end()); + } - //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(); + n = nm->mkConst(ArrayStoreAll(node.getType().toType(), maxValue.toExpr())); + std::vector::iterator itNew = newIndices.begin(), it_end = newIndices.end(); + while (itNew != it_end || !indices.empty()) { + if (itNew != it_end && (indices.empty() || (*itNew) < indices.back())) { + n = nm->mkNode(kind::STORE, n, (*itNew), defaultValue); + ++itNew; } - else if (newIndices.empty() || indices.back() < newIndices.back()) { + else if (itNew == it_end || indices.back() < (*itNew)) { if (elements.back() != maxValue) { n = nm->mkNode(kind::STORE, n, indices.back(), elements.back()); } diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index f6ce84d0f..a535067d0 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -87,8 +87,8 @@ struct ArrayStoreTypeRule { return false; } - Integer depth = 1; - Integer valCount = 1; + unsigned depth = 1; + unsigned valCount = 1; while (store.getKind() == kind::STORE) { depth += 1; if (store[2] == value) { @@ -116,7 +116,7 @@ struct ArrayStoreTypeRule { // Get the most frequently written value from n[0] TNode mostFrequentValue; - Integer mostFrequentValueCount = 0; + unsigned mostFrequentValueCount = 0; store = n[0]; if (store.getKind() == kind::STORE) { // TODO: look up most frequent value and count @@ -130,10 +130,10 @@ struct ArrayStoreTypeRule { } // 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)))) { + Cardinality::CardinalityComparison compare = indexCard.compare(mostFrequentValueCount + depth); + Assert(compare != Cardinality::UNKNOWN); + if (compare == Cardinality::LESS || + (compare == Cardinality::EQUAL && (!(defaultValue < mostFrequentValue)))) { return false; } -- 2.30.2