Fixed assertion failures in array theory

This fixes bugs 335 and 333.

4 files changed, 97 insertions, 10 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f073e67d7..3c48c7907 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -59,6 +59,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   //  d_ppCache(u),  
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),
+  d_isPreRegistered(c),
   d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual"),
   d_notify(*this),
   d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"),
@@ -370,15 +371,18 @@ void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions) {
 void TheoryArrays::preRegisterTerm(TNode node)
 {
   Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
-
   switch (node.getKind()) {
   case kind::EQUAL:
     // Add the trigger for equality
     d_equalityEngine.addTriggerEquality(node);
     break;
   case kind::SELECT: {
+    // Invariant: array terms should be preregistered before being added to the equality engine
+    if (d_equalityEngine.hasTerm(node)) {
+      Assert(d_isPreRegistered.find(node) != d_isPreRegistered.end());
+      return;
+    }
     // Reads
-    d_equalityEngine.addTerm(node);
     TNode store = d_equalityEngine.getRepresentative(node[0]);
 
     // Apply RIntro1 rule to any stores equal to store if not done already
@@ -392,7 +396,6 @@ void TheoryArrays::preRegisterTerm(TNode node)
         Assert(s.getKind()==kind::STORE);
         Node ni = nm->mkNode(kind::SELECT, s, s[1]);
         if (ni != node) {
-          Assert(!d_equalityEngine.hasTerm(ni));
           preRegisterTerm(ni);
         }
         d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true);
@@ -400,6 +403,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
       }
     }
 
+    d_equalityEngine.addTerm(node);
     // Maybe it's a predicate
     // TODO: remove this or keep it if we allow Boolean elements in arrays.
     if (node.getType().isBoolean()) {
@@ -408,11 +412,14 @@ void TheoryArrays::preRegisterTerm(TNode node)
     }
 
     d_infoMap.addIndex(node[0], node[1]);
-    checkRowForIndex(node[1], store);
     d_reads.push_back(node);
+    Assert((d_isPreRegistered.insert(node), true));
+    checkRowForIndex(node[1], store);
     break;
   }
   case kind::STORE: {
+    // Invariant: array terms should be preregistered before being added to the equality engine
+    Assert(!d_equalityEngine.hasTerm(node));
     d_equalityEngine.addTriggerTerm(node);
 
     TNode a = node[0];
@@ -440,12 +447,15 @@ void TheoryArrays::preRegisterTerm(TNode node)
     // Variables etc
     if (node.getType().isArray()) {
       d_equalityEngine.addTriggerTerm(node);
+      Assert(d_equalityEngine.getSize(node) == 1);
     }
     else {
       d_equalityEngine.addTerm(node);
     }
     break;
   }
+  // Invariant: preregistered terms are exactly the terms in the equality engine
+  Assert(d_equalityEngine.hasTerm(node));
 }
 
 
@@ -898,7 +908,6 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b)
     NodeManager* nm = NodeManager::currentNM();
     d_infoMap.setRIntro1Applied(s);
     Node ni = nm->mkNode(kind::SELECT, s, s[1]);
-    Assert(!d_equalityEngine.hasTerm(ni));
     preRegisterTerm(ni);
     d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true);
   }
@@ -1173,24 +1182,54 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 
   if (d_eagerLemmas || bothExist) {
 
-    Assert(aj == Rewriter::rewrite(aj));
-    Assert(bj == Rewriter::rewrite(bj));
+    // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
+    Node aj2 = Rewriter::rewrite(aj);
+    if (aj != aj2) {
+      if (!ajExists) {
+        preRegisterTerm(aj);
+      }
+      if (!d_equalityEngine.hasTerm(aj2)) {
+        preRegisterTerm(aj2);
+      }
+      d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true);
+    }
+    Node bj2 = Rewriter::rewrite(bj);
+    if (bj != bj2) {
+      if (!bjExists) {
+        preRegisterTerm(bj);
+      }
+      if (!d_equalityEngine.hasTerm(bj2)) {
+        preRegisterTerm(bj2);
+      }
+      d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true);
+    }
+    if (aj2 == bj2) {
+      return;
+    }
 
     // construct lemma
-    Node eq1 = aj.eqNode(bj);
+    Node eq1 = aj2.eqNode(bj2);
     Node eq1_r = Rewriter::rewrite(eq1);
     if (eq1_r == d_true) {
+      if (!d_equalityEngine.hasTerm(aj2)) {
+        preRegisterTerm(aj2);
+      }
+      if (!d_equalityEngine.hasTerm(bj2)) {
+        preRegisterTerm(bj2);
+      }
       d_equalityEngine.assertEquality(eq1, true, d_true);
       return;
     }
 
     Node eq2 = i.eqNode(j);
     Node eq2_r = Rewriter::rewrite(eq2);
-    if (eq2 == d_true) {
+    if (eq2_r == d_true) {
       d_equalityEngine.assertEquality(eq2, true, d_true);
       return;
     }
+
     Node lemma = nm->mkNode(kind::OR, eq2_r, eq1_r);
+
     Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lemma<<"\n";
     d_RowAlreadyAdded.insert(lem);
     d_out->lemma(lemma);
@@ -1221,22 +1260,37 @@ void TheoryArrays::dischargeLemmas()
     NodeManager* nm = NodeManager::currentNM();
     Node aj = nm->mkNode(kind::SELECT, a, j);
     Node bj = nm->mkNode(kind::SELECT, b, j);
+    bool ajExists = d_equalityEngine.hasTerm(aj);
+    bool bjExists = d_equalityEngine.hasTerm(bj);
 
     // Check for redundant lemma
     // TODO: more checks possible (i.e. check d_RowAlreadyAdded in context)
     if (d_equalityEngine.areEqual(i,j) ||
         d_equalityEngine.areEqual(a,b) ||
-        (d_equalityEngine.hasTerm(aj) && d_equalityEngine.hasTerm(bj) && d_equalityEngine.areEqual(aj,bj))) {
+        (ajExists && bjExists && d_equalityEngine.areEqual(aj,bj))) {
       d_RowQueue.push(l);
       continue;
     }
 
+    // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
     Node aj2 = Rewriter::rewrite(aj);
     if (aj != aj2) {
+      if (!ajExists) {
+        preRegisterTerm(aj);
+      }
+      if (!d_equalityEngine.hasTerm(aj2)) {
+        preRegisterTerm(aj2);
+      }
       d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true);
     }
     Node bj2 = Rewriter::rewrite(bj);
     if (bj != bj2) {
+      if (!bjExists) {
+        preRegisterTerm(bj);
+      }
+      if (!d_equalityEngine.hasTerm(bj2)) {
+        preRegisterTerm(bj2);
+      }
       d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true);
     }
     if (aj2 == bj2) {
@@ -1248,6 +1302,12 @@ void TheoryArrays::dischargeLemmas()
     Node eq1 = aj2.eqNode(bj2);
     Node eq1_r = Rewriter::rewrite(eq1);
     if (eq1_r == d_true) {
+      if (!d_equalityEngine.hasTerm(aj2)) {
+        preRegisterTerm(aj2);
+      }
+      if (!d_equalityEngine.hasTerm(bj2)) {
+        preRegisterTerm(bj2);
+      }
       d_equalityEngine.assertEquality(eq1, true, d_true);
       d_RowQueue.push(l);
       continue;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 88986ee7a..146a2145b 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -165,6 +165,9 @@ class TheoryArrays : public Theory {
   /** Explain why this literal is true by adding assumptions */
   void explain(TNode literal, std::vector<TNode>& assumptions);
 
+  /** For debugging only- checks invariants about when things are preregistered*/
+  context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered;
+
   public:
 
   void preRegisterTerm(TNode n);
diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am
index fcbeb208e..452663456 100644
--- a/test/regress/regress0/arrays/Makefile.am
+++ b/test/regress/regress0/arrays/Makefile.am
@@ -27,6 +27,7 @@ TESTS =	\
 	incorrect9.smt \
 	incorrect10.smt \
 	incorrect11.smt \
+	swap_t1_np_nf_ai_00005_007.cvc.smt \
 	x2.smt \
 	x3.smt
 
diff --git a/test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt b/test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt
new file mode 100644
index 000000000..af609c86f
--- /dev/null
+++ b/test/regress/regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt
@@ -0,0 +1,23 @@
+(benchmark swap
+  :source {
+Benchmarks used in the followin paper:
+Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure
+Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. 
+PDPAR'05
+http://www.ai.dist.unige.it/pdpar05/
+
+
+}
+  :status unsat
+:difficulty { 0 }
+:category { crafted }
+  :logic QF_AX
+  :extrafuns ((a1 Array))
+  :extrafuns ((i0 Index))
+  :extrafuns ((i1 Index))
+  :extrafuns ((i2 Index))
+  :extrafuns ((i3 Index))
+  :extrafuns ((i4 Index))
+  :formula
+(let (?cvc_4 (select a1 i4)) (let (?cvc_5 (select a1 i2)) (let (?cvc_0 (store (store a1 i4 ?cvc_5) i2 ?cvc_4)) (let (?cvc_1 (store (store ?cvc_0 i0 (select ?cvc_0 i3)) i3 (select ?cvc_0 i0))) (let (?cvc_2 (store (store ?cvc_1 i2 (select ?cvc_1 i1)) i1 (select ?cvc_1 i2))) (let (?cvc_3 (store (store ?cvc_2 i4 (select ?cvc_2 i3)) i3 (select ?cvc_2 i4))) (let (?cvc_6 (store (store a1 i2 ?cvc_4) i4 ?cvc_5)) (let (?cvc_7 (store (store ?cvc_6 i0 (select ?cvc_6 i3)) i3 (select ?cvc_6 i0))) (let (?cvc_8 (store (store ?cvc_7 i1 (select ?cvc_7 i2)) i2 (select ?cvc_7 i1))) (let (?cvc_9 (store (store ?cvc_8 i3 (select ?cvc_8 i4)) i4 (select ?cvc_8 i3))) (not (= (store (store ?cvc_3 i3 (select ?cvc_3 i2)) i2 (select ?cvc_3 i3)) (store (store ?cvc_9 i2 (select ?cvc_9 i3)) i3 (select ?cvc_9 i2))))))))))))))
+)