Implemented array type enumerator, more fixes for models

3 files changed, 91 insertions, 7 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 63b61995a..b4cc8e5f7 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -565,11 +565,17 @@ void TheoryArrays::computeCareGraph()
           // If arrays are known to be disequal, or cannot become equal, we can continue
           Assert(d_mayEqualEqualityEngine.hasTerm(r1[0]) && d_mayEqualEqualityEngine.hasTerm(r2[0]));
           if (r1[0].getType() != r2[0].getType() ||
-              (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) ||
               d_equalityEngine.areDisequal(r1[0], r2[0], false)) {
             Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
             continue;
           }
+          else if (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) {
+            if (r2.getType().getCardinality().isInfinite()) {
+              continue;
+            }
+            // TODO: add a disequality split for these two arrays
+            continue;
+          }
         }
 
         TNode x = r1[1];
@@ -678,11 +684,17 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
     if (it == defValues.end()) {
       TypeNode valueType = n.getType().getArrayConstituentType();
       rep = defaultValuesSet.nextTypeEnum(valueType);
+      if (rep.isNull()) {
+        Assert(defaultValuesSet.getSet(valueType)->begin() != defaultValuesSet.getSet(valueType)->end());
+        rep = *(defaultValuesSet.getSet(valueType)->begin());
+      }
+      Trace("arrays-models") << "New default value = " << rep << endl;
       defValues[mayRep] = rep;
     }
     else {
       rep = (*it).second;
     }
+
     // Build the STORE_ALL term with the default value
     rep = nm->mkConst(ArrayStoreAll(n.getType().toType(), rep.toExpr()));
     // For each read, require that the rep stores the right value
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index d120f8feb..0f46ffe7c 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -358,6 +358,10 @@ public:
           Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl;
           return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
         }
+        else if (node[0].isConst() && node[1].isConst()) {
+          Trace("arrays-postrewrite") << "Arrays::postRewrite returning false" << std::endl;
+          return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
+        }
         if (node[0] > node[1]) {
           Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
           Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << newNode << std::endl;
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index f6d871c48..c6b73b9f6 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -24,6 +24,7 @@
 #include "theory/type_enumerator.h"
 #include "expr/type_node.h"
 #include "expr/kind.h"
+#include "theory/rewriter.h"
 
 namespace CVC4 {
 namespace theory {
@@ -31,27 +32,94 @@ namespace arrays {
 
 class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
   TypeEnumerator d_index;
-  TypeEnumerator d_constituent;
+  TypeNode d_constituentType;
+  NodeManager* d_nm;
+  std::vector<Node> d_indexVec;
+  std::vector<TypeEnumerator*> d_constituentVec;
+  bool d_finished;
+  Node d_arrayConst;
 
 public:
 
   ArrayEnumerator(TypeNode type) throw(AssertionException) :
     TypeEnumeratorBase<ArrayEnumerator>(type),
-    d_index(TypeEnumerator(type.getArrayIndexType())),
-    d_constituent(TypeEnumerator(type.getArrayConstituentType())) {
+    d_index(type.getArrayIndexType()),
+    d_constituentType(type.getArrayConstituentType()),
+    d_nm(NodeManager::currentNM()),
+    d_finished(false)
+  {
+    d_indexVec.push_back(*d_index);
+    d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+    d_arrayConst = d_nm->mkConst(ArrayStoreAll(type.toType(), (*(*d_constituentVec.back())).toExpr()));
+  }
+
+  ~ArrayEnumerator() {
+    while (!d_constituentVec.empty()) {
+      delete d_constituentVec.back();
+      d_constituentVec.pop_back();
+    }
   }
 
   Node operator*() throw(NoMoreValuesException) {
-    return Node::null();
-    //return NodeManager::currentNM()->mkConst(Array(d_size, d_bits));
+    if (d_finished) {
+      throw NoMoreValuesException(getType());
+    }
+    Node n = d_arrayConst;
+    for (unsigned i = 0; i < d_indexVec.size(); ++i) {
+      n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i])));
+    }
+    Trace("array-type-enum") << "operator * prerewrite: " << n << std::endl;
+    n = Rewriter::rewrite(n);
+    Trace("array-type-enum") << "operator * returning: " << n << std::endl;
+    return n;
   }
 
   ArrayEnumerator& operator++() throw() {
+    Trace("array-type-enum") << "operator++ called, **this = " << **this << std::endl;
+
+    if (d_finished) {
+      Trace("array-type-enum") << "operator++ finished!" << std::endl;
+      return *this;
+    }
+    while (!d_constituentVec.empty()) {
+      ++(*d_constituentVec.back());
+      if (d_constituentVec.back()->isFinished()) {
+        delete d_constituentVec.back();
+        d_constituentVec.pop_back();
+      }
+      else {
+        break;
+      }
+    }
+
+    if (d_constituentVec.empty()) {
+      ++d_index;
+      if (d_index.isFinished()) {
+        Trace("array-type-enum") << "operator++ finished!" << std::endl;
+        d_finished = true;
+        return *this;
+      }
+      d_indexVec.push_back(*d_index);
+      d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+      ++(*d_constituentVec.back());
+      if (d_constituentVec.back()->isFinished()) {
+        Trace("array-type-enum") << "operator++ finished!" << std::endl;
+        d_finished = true;
+        return *this;
+      }
+    }
+
+    while (d_constituentVec.size() < d_indexVec.size()) {
+      d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+    }
+
+    Trace("array-type-enum") << "operator++ returning, **this = " << **this << std::endl;
     return *this;
   }
 
   bool isFinished() throw() {
-    Unimplemented();
+    Trace("array-type-enum") << "isFinished returning: " << d_finished << std::endl;
+    return d_finished;
   }
 
 };/* class ArrayEnumerator */