Array constants finished and working. Unit tests for array constants.

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;