Enabled array propagation during lemma propagation - this should catch some

conflicts that now require extra splitting.

2 files changed, 42 insertions, 4 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 5af7f02db..89fdf7096 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -2434,11 +2434,8 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
   Trace("arrays-crl")<<"Arrays::checkLemmas done.\n";
 }
 
-void TheoryArrays::queueRowLemma(RowLemmaType lem)
+void TheoryArrays::propagate(RowLemmaType lem)
 {
-  if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
-    return;
-  }
   TNode a = lem.first;
   TNode b = lem.second;
   TNode i = lem.third;
@@ -2489,6 +2486,38 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       return;
     }
   }
+}
+
+void TheoryArrays::queueRowLemma(RowLemmaType lem)
+{
+  if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
+    return;
+  }
+  TNode a = lem.first;
+  TNode b = lem.second;
+  TNode i = lem.third;
+  TNode j = lem.fourth;
+
+  Assert(a.getType().isArray() && b.getType().isArray());
+  if (d_equalityEngine.areEqual(a,b) ||
+      d_equalityEngine.areEqual(i,j)) {
+    return;
+  }
+
+  NodeManager* nm = NodeManager::currentNM();
+  Node aj = nm->mkNode(kind::SELECT, a, j);
+  Node bj = nm->mkNode(kind::SELECT, b, j);
+
+  // Try to avoid introducing new read terms: track whether these already exist
+  bool ajExists = d_equalityEngine.hasTerm(aj);
+  bool bjExists = d_equalityEngine.hasTerm(bj);
+  bool bothExist = ajExists && bjExists;
+
+  // If propagating, check propagations
+  int prop = options::arraysPropagate();
+  if (prop > 0) {
+    propagate(lem);
+  }
 
   // If equivalent lemma already exists, don't enqueue this one
   if (d_useArrTable) {
@@ -2610,6 +2639,14 @@ bool TheoryArrays::dischargeLemmas()
       continue;
     }
 
+    int prop = options::arraysPropagate();
+    if (prop > 0) {
+      propagate(l);
+      if (d_conflict) {
+        return true;
+      }
+    }
+
     // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
     Node aj2 = Rewriter::rewrite(aj);
     if (aj != aj2) {
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 717c654d2..6a023c282 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -404,6 +404,7 @@ class TheoryArrays : public Theory {
   void checkStore(TNode a);
   void checkRowForIndex(TNode i, TNode a);
   void checkRowLemmas(TNode a, TNode b);
+  void propagate(RowLemmaType lem);
   void queueRowLemma(RowLemmaType lem);
   bool dischargeLemmas();