bug fixes to models, array rewriter with previously failing testcases

5 files changed, 83 insertions, 58 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 342e67654..3a109b51a 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -423,7 +423,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node, bool internalAssert)
     Assert(d_equalityEngine.getRepresentative(store) == store);
     d_infoMap.addIndex(store, node[1]);
     if (internalAssert) {
-      d_readsInternal.push_back(node);
+      d_readsInternal.insert(node);
     }
     d_reads.push_back(node);
     Assert((d_isPreRegistered.insert(node), true));
@@ -445,7 +445,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node, bool internalAssert)
       NodeManager* nm = NodeManager::currentNM();
       Node ni = nm->mkNode(kind::SELECT, node, i);
       if (!d_equalityEngine.hasTerm(ni)) {
-        preRegisterTermInternal(ni);
+        preRegisterTermInternal(ni, false);
       }
 
       // Apply RIntro1 Rule
@@ -649,81 +649,80 @@ void TheoryArrays::computeCareGraph()
 /////////////////////////////////////////////////////////////////////////////
 
 
-void TheoryArrays::collectReads(TNode n, set<Node>& readSet, set<Node>& cache)
+void TheoryArrays::collectTerms(TNode n, set<Node>& termSet)
 {
-  if (cache.find(n) != cache.end()) {
+  if (termSet.find(n) != termSet.end()) {
     return;
   }
-  if (n.getKind() == kind::SELECT) {
-    readSet.insert(n);
-  }
-  for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
-    collectReads(*child_it, readSet, cache);
+  termSet.insert(n);
+  if (n.getType().isBoolean() || !isLeaf(n)) {
+    for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
+      collectTerms(*child_it, termSet);
+    }
   }
-  cache.insert(n);
 }
 
 
-void TheoryArrays::collectArrays(TNode n, set<Node>& arraySet, set<Node>& cache)
+void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel )
 {
-  if (cache.find(n) != cache.end()) {
-    return;
-  }
-  if (n.getType().isArray()) {
-    arraySet.insert(n);
-  }
-  for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
-    collectArrays(*child_it, arraySet, cache);
-  }
-  cache.insert(n);
-}
+  set<Node> termSet;
+  set<Node> cache;
 
-
-void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
-  m->assertEqualityEngine( &d_equalityEngine );
-
-  std::map<Node, std::vector<Node> > selects;
-
-  set<Node> readSet, arraySet;
-  set<Node> readCache, arrayCache;
-  // Collect all arrays and selects appearing in assertions
+  // Collect all terms appearing in assertions
   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
   for (; assert_it != assert_it_end; ++assert_it) {
-    collectReads(*assert_it, readSet, readCache);
-    collectArrays(*assert_it, arraySet, arrayCache);
+    collectTerms(*assert_it, termSet);
   }
 
-  // Add arrays and selects that are shared terms
+  // Add terms that are shared terms
   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
-  for (; shared_it != shared_it_end; ++ shared_it) {
-    collectReads(*shared_it, readSet, readCache);
-    collectArrays(*shared_it, arraySet, arrayCache);
+  for (; shared_it != shared_it_end; ++shared_it) {
+    collectTerms(*shared_it, termSet);
   }
 
   // Add selects that were generated internally
-  unsigned size = d_readsInternal.size();
-  for (unsigned i = 0; i < size; ++i) {
-    readSet.insert(d_readsInternal[i]);
+  context::CDHashSet<TNode, TNodeHashFunction>::iterator internal_it = d_readsInternal.begin(), internal_it_end = d_readsInternal.end();
+  for (; internal_it != internal_it_end; ++internal_it) {
+    termSet.insert(*internal_it);
   }
 
   // Go through all equivalence classes and collect relevant arrays and reads
   std::vector<Node> arrays;
+  std::map<Node, std::vector<Node> > selects;
+  bool computeRep, isArray;
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
-  bool computeRep;
   while( !eqcs_i.isFinished() ){
     Node eqc = (*eqcs_i);
+    isArray = eqc.getType().isArray();
     computeRep = false;
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
     while( !eqc_i.isFinished() ){
       Node n = *eqc_i;
       // If this EC is an array type and it contains something other than STORE nodes, we have to compute a representative explicitly
-      if (!computeRep && n.getKind() != kind::STORE && arraySet.find(n) != arraySet.end()) {
-        arrays.push_back(eqc);
-        computeRep = true;
+      if (isArray && termSet.find(n) != termSet.end()) {
+        if (n.getKind() == kind::STORE) {
+          // Make sure RIntro1 reads are included
+          termSet.insert(NodeManager::currentNM()->mkNode(kind::SELECT, n, n[1]));
+        }
+        else if (!computeRep) {
+          arrays.push_back(eqc);
+          computeRep = true;
+        }
       }
-      // If this term is a select, and it appears in an assertion or was generated internally,
+      ++eqc_i;
+    }
+    ++eqcs_i;
+  }
+
+  eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
+  while( !eqcs_i.isFinished() ){
+    Node eqc = (*eqcs_i);
+    eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
+    while( !eqc_i.isFinished() ){
+      Node n = *eqc_i;
+      // If this term is a select, and it appears in an assertion or was derived from one,
       // record that the EC rep of its store parameter is being read from using this term
-      if (n.getKind() == kind::SELECT && readSet.find(n) != readSet.end()) {
+      if (n.getKind() == kind::SELECT && termSet.find(n) != termSet.end()) {
         selects[d_equalityEngine.getRepresentative(n[0])].push_back(n);
       }
       ++eqc_i;
@@ -731,6 +730,8 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
     ++eqcs_i;
   }
 
+  m->assertEqualityEngine(&d_equalityEngine, &termSet);
+
   NodeManager* nm = NodeManager::currentNM();
   Node rep;
   map<Node, Node> defValues;
@@ -1259,6 +1260,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       Node i_eq_j = i.eqNode(j);
       Node reason = nm->mkNode(kind::OR, aj_eq_bj, i_eq_j);
       d_permRef.push_back(reason);
+      d_readsInternal.insert(aj);
+      d_readsInternal.insert(bj);
       if (!ajExists) {
         preRegisterTermInternal(aj);
       }
@@ -1301,6 +1304,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
     // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
     Node aj2 = Rewriter::rewrite(aj);
     if (aj != aj2) {
+      d_readsInternal.insert(aj);
+      d_readsInternal.insert(aj2);
       if (!ajExists) {
         preRegisterTermInternal(aj);
       }
@@ -1311,6 +1316,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
     }
     Node bj2 = Rewriter::rewrite(bj);
     if (bj != bj2) {
+      d_readsInternal.insert(bj);
+      d_readsInternal.insert(bj2);
       if (!bjExists) {
         preRegisterTermInternal(bj);
       }
@@ -1327,6 +1334,8 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
     Node eq1 = aj2.eqNode(bj2);
     Node eq1_r = Rewriter::rewrite(eq1);
     if (eq1_r == d_true) {
+      d_readsInternal.insert(aj2);
+      d_readsInternal.insert(bj2);
       if (!d_equalityEngine.hasTerm(aj2)) {
         preRegisterTermInternal(aj2);
       }
@@ -1401,6 +1410,8 @@ void TheoryArrays::dischargeLemmas()
     // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
     Node aj2 = Rewriter::rewrite(aj);
     if (aj != aj2) {
+      d_readsInternal.insert(aj);
+      d_readsInternal.insert(aj2);
       if (!ajExists) {
         preRegisterTermInternal(aj);
       }
@@ -1411,6 +1422,8 @@ void TheoryArrays::dischargeLemmas()
     }
     Node bj2 = Rewriter::rewrite(bj);
     if (bj != bj2) {
+      d_readsInternal.insert(bj);
+      d_readsInternal.insert(bj2);
       if (!bjExists) {
         preRegisterTermInternal(bj);
       }
@@ -1427,6 +1440,8 @@ void TheoryArrays::dischargeLemmas()
     Node eq1 = aj2.eqNode(bj2);
     Node eq1_r = Rewriter::rewrite(eq1);
     if (eq1_r == d_true) {
+      d_readsInternal.insert(aj2);
+      d_readsInternal.insert(bj2);
       if (!d_equalityEngine.hasTerm(aj2)) {
         preRegisterTermInternal(aj2);
       }
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index a47c8440e..9bf1201f3 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -218,12 +218,12 @@ class TheoryArrays : public Theory {
   /////////////////////////////////////////////////////////////////////////////
 
   private:
-  /** Helper functions for collectModelInfo */
-  void collectReads(TNode n, std::set<Node>& readSet, std::set<Node>& cache);
-  void collectArrays(TNode n, std::set<Node>& arraySet, std::set<Node>& cache);
+  /** Helper function for collectModelInfo */
+  void collectTerms(TNode n, std::set<Node>& termSet);
+
   public:
 
-  void collectModelInfo( TheoryModel* m, bool fullModel );
+  void collectModelInfo(TheoryModel* m, bool fullModel);
 
   /////////////////////////////////////////////////////////////////////////////
   // NOTIFICATIONS
@@ -337,7 +337,7 @@ class TheoryArrays : public Theory {
   context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther;
   context::CDO<bool> d_sharedTerms;
   context::CDList<TNode> d_reads;
-  context::CDList<TNode> d_readsInternal;
+  context::CDHashSet<TNode, TNodeHashFunction> d_readsInternal;
   std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
 
   // The decision requests we have for the core
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 62782f90e..da479616d 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -306,7 +306,15 @@ public:
           NodeManager* nm = NodeManager::currentNM();
           if (val) {
             // store(store(a,i,v),i,w) = store(a,i,w)
-            Node result = nm->mkNode(kind::STORE, store[0], index, value);
+            Node result;
+            if (value.getKind() == kind::SELECT &&
+                value[0] == store[0] &&
+                value[1] == index) {
+              result = store[0];
+            }
+            else {
+              result = nm->mkNode(kind::STORE, store[0], index, value);
+            }
             Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << result << std::endl;
             return RewriteResponse(REWRITE_DONE, result);
           }
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index a01844f77..0e1d90a74 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -246,9 +246,10 @@ void TheoryModel::assertPredicate( Node a, bool polarity ){
 }
 
 /** assert equality engine */
-void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
+void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>* termSet)
+{
   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
-  while( !eqcs_i.isFinished() ){
+  for (; !eqcs_i.isFinished(); ++eqcs_i) {
     Node eqc = (*eqcs_i);
     bool predicate = false;
     bool predTrue = false;
@@ -259,7 +260,10 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
       predFalse = ee->areEqual(eqc, d_false);
     }
     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
-    while(!eqc_i.isFinished()) {
+    for (; !eqc_i.isFinished(); ++eqc_i) {
+      if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) {
+        continue;
+      }
       if (predicate) {
         if (predTrue) {
           assertPredicate(*eqc_i, true);
@@ -275,9 +279,7 @@ void TheoryModel::assertEqualityEngine( const eq::EqualityEngine* ee ){
       } else {
         assertEquality(*eqc_i, eqc, true);
       }
-      ++eqc_i;
     }
-    ++eqcs_i;
   }
 }
 
diff --git a/src/theory/model.h b/src/theory/model.h
index 5b691d4d9..d17192281 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -92,7 +92,7 @@ public:
   /** assert predicate holds in the model */
   void assertPredicate( Node a, bool polarity );
   /** assert all equalities/predicates in equality engine hold in the model */
-  void assertEqualityEngine( const eq::EqualityEngine* ee );
+  void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL);
   /** assert representative
     *  This function tells the model that n should be the representative of its equivalence class.
     *  It should be called during model generation, before final representatives are chosen.  In the