diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 16 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 48 |
2 files changed, 32 insertions, 32 deletions
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 4402c43ea..d120f8feb 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -119,14 +119,10 @@ class TheoryArraysRewriter { TNode mostFrequentValue; unsigned mostFrequentValueCount = 0; - bool recompute CVC4_UNUSED = false; - if (node[0].getKind() == kind::STORE) { - // TODO: look up most frequent value and count - mostFrequentValue = node.getAttribute(ArrayConstantMostFrequentValueAttr()); - mostFrequentValueCount = node.getAttribute(ArrayConstantMostFrequentValueCountAttr()); - if (!replacedValue.isNull() && mostFrequentValue == replacedValue) { - recompute = true; - } + store = node[0]; + if (store.getKind() == kind::STORE) { + mostFrequentValue = store.getAttribute(ArrayConstantMostFrequentValueAttr()); + mostFrequentValueCount = store.getAttribute(ArrayConstantMostFrequentValueCountAttr()); } // Compute the most frequently written value for n @@ -134,7 +130,6 @@ class TheoryArraysRewriter { (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 @@ -180,7 +175,7 @@ class TheoryArraysRewriter { Assert(compare != Cardinality::UNKNOWN); if (compare == Cardinality::GREATER || (compare == Cardinality::EQUAL && (defaultValue < maxValue))) { - Assert(recompute); + Assert(!replacedValue.isNull() && mostFrequentValue == replacedValue); return n; } @@ -283,6 +278,7 @@ public: if (store.isConst() && index.isConst() && value.isConst()) { // normalize constant Node n = normalizeConstant(node); + Assert(n.isConst()); Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl; return RewriteResponse(REWRITE_DONE, n); } diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 2cad1fa43..8b31a31f9 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -48,24 +48,31 @@ struct ArraySelectTypeRule { struct ArrayStoreTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { - Assert(n.getKind() == kind::STORE); - TypeNode arrayType = n[0].getType(check); - if( check ) { - if(!arrayType.isArray()) { - throw TypeCheckingExceptionPrivate(n, "array store operating on non-array"); - } - TypeNode indexType = n[1].getType(check); - TypeNode valueType = n[2].getType(check); - if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ - throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array"); - } - if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){ - Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl; - Debug("array-types") << "value types: " << valueType << std::endl; - throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array"); + if (n.getKind() == kind::STORE) { + TypeNode arrayType = n[0].getType(check); + if( check ) { + if(!arrayType.isArray()) { + throw TypeCheckingExceptionPrivate(n, "array store operating on non-array"); + } + TypeNode indexType = n[1].getType(check); + TypeNode valueType = n[2].getType(check); + if(!indexType.isSubtypeOf(arrayType.getArrayIndexType())){ + throw TypeCheckingExceptionPrivate(n, "array store not indexed with correct type for array"); + } + if(!valueType.isSubtypeOf(arrayType.getArrayConstituentType())){ + Debug("array-types") << "array type: "<< arrayType.getArrayConstituentType() << std::endl; + Debug("array-types") << "value types: " << valueType << std::endl; + throw TypeCheckingExceptionPrivate(n, "array store not assigned with correct type for array"); + } } + return arrayType; + } + else { + Assert(n.getKind() == kind::STORE_ALL); + ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>(); + ArrayType arrayType = storeAll.getType(); + return TypeNode::fromType(arrayType); } - return arrayType; } inline static bool computeIsConst(NodeManager* nodeManager, TNode n) @@ -116,14 +123,13 @@ struct ArrayStoreTypeRule { // that is written to more than the default value. If so, it is not in // normal form. - // Get the most frequently written value from n[0] + // Get the most frequently written value for n[0] TNode mostFrequentValue; unsigned mostFrequentValueCount = 0; store = n[0]; if (store.getKind() == kind::STORE) { - // TODO: look up most frequent value and count - mostFrequentValue = n.getAttribute(ArrayConstantMostFrequentValueAttr()); - mostFrequentValueCount = n.getAttribute(ArrayConstantMostFrequentValueCountAttr()); + mostFrequentValue = store.getAttribute(ArrayConstantMostFrequentValueAttr()); + mostFrequentValueCount = store.getAttribute(ArrayConstantMostFrequentValueCountAttr()); } // Compute the most frequently written value for n @@ -140,8 +146,6 @@ struct ArrayStoreTypeRule { (compare == Cardinality::EQUAL && (!(defaultValue < mostFrequentValue)))) { return false; } - - // TODO: store mostFrequentValue and mostFrequentValueCount for this node n.setAttribute(ArrayConstantMostFrequentValueAttr(), mostFrequentValue); n.setAttribute(ArrayConstantMostFrequentValueCountAttr(), mostFrequentValueCount); return true; |