Fix for array bug with decision heuristic

Also fixed one bv rewrite failure (more to come)

4 files changed, 29 insertions, 18 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 91bbae2f4..81661acd1 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -71,6 +71,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_RowQueue(c),
   d_RowAlreadyAdded(u),
   d_sharedArrays(c),
+  d_sharedOther(c),
   d_sharedTerms(c, false),
   d_reads(c),
   d_permRef(c)
@@ -481,9 +482,12 @@ void TheoryArrays::addSharedTerm(TNode t) {
   Debug("arrays::sharing") << spaces(getSatContext()->getLevel()) << "TheoryArrays::addSharedTerm(" << t << ")" << std::endl;
   d_equalityEngine.addTriggerTerm(t, THEORY_ARRAY);
   if (t.getType().isArray()) {
-    d_sharedArrays.insert(t,true);
+    d_sharedArrays.insert(t);
   }
   else {
+#ifdef CVC4_ASSERTIONS
+    d_sharedOther.insert(t);
+#endif
     d_sharedTerms = true;
   }
 }
@@ -507,18 +511,18 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) {
 void TheoryArrays::computeCareGraph()
 {
   if (d_sharedArrays.size() > 0) {
-    context::CDHashMap<TNode, bool, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end();
+    context::CDHashSet<TNode, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end();
     for (; it1 != iend; ++it1) {
       for (it2 = it1, ++it2; it2 != iend; ++it2) {
-        if ((*it1).first.getType() != (*it2).first.getType()) {
+        if ((*it1).getType() != (*it2).getType()) {
           continue;
         }
-        EqualityStatus eqStatusArr = getEqualityStatus((*it1).first, (*it2).first);
+        EqualityStatus eqStatusArr = getEqualityStatus((*it1), (*it2));
         if (eqStatusArr != EQUALITY_UNKNOWN) {
           continue;
         }
-        Assert(d_valuation.getEqualityStatus((*it1).first, (*it2).first) == EQUALITY_UNKNOWN);
-        addCarePair((*it1).first, (*it2).first);
+        Assert(d_valuation.getEqualityStatus((*it1), (*it2)) == EQUALITY_UNKNOWN);
+        addCarePair((*it1), (*it2));
         ++d_numSharedArrayVarSplits;
         return;
       }
@@ -533,6 +537,11 @@ void TheoryArrays::computeCareGraph()
     for (unsigned i = 0; i < size; ++ i) {
       TNode r1 = d_reads[i];
 
+      // Make sure shared terms were identified correctly
+      Assert(theoryOf(r1[0]) == THEORY_ARRAY || isShared(r1[0]));
+      Assert(theoryOf(r1[1]) == THEORY_ARRAY ||
+             d_sharedOther.find(r1[1]) != d_sharedOther.end());
+
       for (unsigned j = i + 1; j < size; ++ j) {
         TNode r2 = d_reads[j];
 
@@ -707,13 +716,10 @@ void TheoryArrays::check(Effort e) {
 
             Node ak = nm->mkNode(kind::SELECT, fact[0][0], k);
             Node bk = nm->mkNode(kind::SELECT, fact[0][1], k);
-            if (!d_equalityEngine.hasTerm(ak)) {
-              preRegisterTerm(ak);
-            }
-            if (!d_equalityEngine.hasTerm(bk)) {
-              preRegisterTerm(bk);
-            }
-            d_equalityEngine.assertEquality(ak.eqNode(bk), false, fact);
+            Node eq = d_valuation.ensureLiteral(ak.eqNode(bk));
+            Assert(eq.getKind() == kind::EQUAL);
+            d_equalityEngine.assertEquality(eq, false, fact);
+            propagate(eq.notNode());
             Trace("arrays-lem")<<"Arrays::addExtLemma "<< ak << " /= " << bk <<"\n";
             ++d_numExt;
           }
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 54d20d478..80fe692c0 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -305,7 +305,8 @@ class TheoryArrays : public Theory {
   context::CDQueue<RowLemmaType> d_RowQueue;
   context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
 
-  context::CDHashMap<TNode, bool, TNodeHashFunction> d_sharedArrays;
+  context::CDHashSet<TNode, TNodeHashFunction> d_sharedArrays;
+  context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther;
   context::CDO<bool> d_sharedTerms;
   context::CDList<TNode> d_reads;
   std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 47725444d..85ccbc787 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -521,10 +521,6 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) {
         >::apply(node);
     return RewriteResponse(REWRITE_DONE, resultNode); 
   }
-  else if(RewriteRule<BitwiseEq>::applies(node)) {
-    Node resultNode = RewriteRule<BitwiseEq>::run<false>(node);
-    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode); 
-  }
   else {
     Node resultNode = LinearRewriteStrategy
       < RewriteRule<FailEq>,
@@ -532,6 +528,12 @@ RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool preregister) {
         RewriteRule<ReflexivityEq>,
         RewriteRule<SolveEq>
         >::apply(node);
+
+    if(RewriteRule<BitwiseEq>::applies(resultNode)) {
+      resultNode = RewriteRule<BitwiseEq>::run<false>(resultNode);
+      return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+    }
+
     return RewriteResponse(REWRITE_DONE, resultNode); 
   }
 }
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 18274e060..7d5f541c0 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -173,6 +173,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 	  rewriteStackTop.node = response.node;
           break;
         }
+        // Check for trivial rewrite loop of size 2
+        Assert(Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, response.node).node != rewriteStackTop.node);
 	rewriteStackTop.node = response.node;
       }
       // We're done with the post rewrite, so we add to the cache