2 files changed, 43 insertions, 73 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 65e409012..4ba4aeba5 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -319,33 +319,12 @@ bool TheoryArrays::propagate(TNode literal)
     return false;
   }
 
-  // See if the literal has been asserted already
-  Node normalized = Rewriter::rewrite(literal);
-  bool satValue = false;
-  bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
-
-  // If asserted, we're done or in conflict
-  if (isAsserted) {
-    if (!satValue) {
-      Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
-      std::vector<TNode> assumptions;
-      Node negatedLiteral;
-      negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
-      assumptions.push_back(negatedLiteral);
-      explain(literal, assumptions);
-      d_conflictNode = mkAnd(assumptions);
-      d_conflict = true;
-      return false;
-    }
-    // Propagate even if already known in SAT - could be a new equation between shared terms
-    // (terms that weren't shared when the literal was asserted!)
+  // Propagate away
+  bool ok = d_out->propagate(literal);
+  if (!ok) {
+    d_conflict = true;
   }
-
-  // Nothing, just enqueue it for propagation and mark it as asserted already
-  Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
-  d_literalsToPropagate.push_back(literal);
-
-  return true;
+  return ok;
 }/* TheoryArrays::propagate(TNode) */
 
 
@@ -479,29 +458,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
 
 void TheoryArrays::propagate(Effort e)
 {
-  Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl;
-  if (!d_conflict) {
-    for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
-      TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-      Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl;
-      bool satValue;
-      Node normalized = Rewriter::rewrite(literal);
-      if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
-        d_out->propagate(literal);
-      } else {
-        Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl;
-        Node negatedLiteral;
-        std::vector<TNode> assumptions;
-        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
-        assumptions.push_back(negatedLiteral);
-        explain(literal, assumptions);
-        d_conflictNode = mkAnd(assumptions);
-        d_conflict = true;
-        break;
-      }
-    }
-  }
-
+  // direct propagation now
 }
 
 
@@ -634,6 +591,7 @@ void TheoryArrays::computeCareGraph()
             break;
           case EQUALITY_FALSE_IN_MODEL:
             Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl;
+            continue;
             break;
           default:
             break;
@@ -700,11 +658,21 @@ void TheoryArrays::check(Effort e) {
 
     Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
 
-    // If the assertion doesn't have a literal, it's a shared equality
-    Assert(assertion.isPreregistered ||
-           ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) ||
-            (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL &&
-             d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1]))));
+    bool polarity = fact.getKind() != kind::NOT;
+    TNode atom = polarity ? fact : fact[0];
+
+    if (!assertion.isPreregistered) {
+      if (atom.getKind() == kind::EQUAL) {
+        if (!d_equalityEngine.hasTerm(atom[0])) {
+          Assert(atom[0].isConst());
+          d_equalityEngine.addTerm(atom[0]);
+        }
+        if (!d_equalityEngine.hasTerm(atom[1])) {
+          Assert(atom[1].isConst());
+          d_equalityEngine.addTerm(atom[1]);
+        }
+      }
+    }
 
     // Do the work
     switch (fact.getKind()) {
@@ -758,19 +726,10 @@ void TheoryArrays::check(Effort e) {
   }
 
   // If in conflict, output the conflict
-  if (d_conflict) {
-    Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl;
-    d_out->conflict(d_conflictNode);
-  }
-  else {
-    // Otherwise we propagate
-    propagate(e);
-
-    if(!d_eagerLemmas && fullEffort(e) && !d_conflict) {
-      // generate the lemmas on the worklist
-      Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
-      dischargeLemmas();
-    }
+  if(!d_eagerLemmas && fullEffort(e) && !d_conflict) {
+    // generate the lemmas on the worklist
+    Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
+    dischargeLemmas();
   }
 
   Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
@@ -1138,6 +1097,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   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)) {
@@ -1345,6 +1305,16 @@ void TheoryArrays::dischargeLemmas()
   }
 }
 
+void TheoryArrays::conflict(TNode a, TNode b) {
+  if (Theory::theoryOf(a) == theory::THEORY_BOOL) {
+    d_conflictNode = explain(a.iffNode(b));
+  } else {
+    d_conflictNode = explain(a.eqNode(b));
+  }
+  d_out->conflict(d_conflictNode);
+  d_conflict = true;
+}
+
 
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index d17caba45..6592e86cf 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -261,11 +261,8 @@ class TheoryArrays : public Theory {
 
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
-      if (Theory::theoryOf(t1) == THEORY_BOOL) {
-        return d_arrays.propagate(t1.iffNode(t2));
-      } else {
-        return d_arrays.propagate(t1.eqNode(t2));
-      }
+      d_arrays.conflict(t1, t2);
+      return false;
     }
   };
 
@@ -275,9 +272,12 @@ class TheoryArrays : public Theory {
   /** Equaltity engine */
   eq::EqualityEngine d_equalityEngine;
 
-  // Are we in conflict?
+  /** Are we in conflict? */
   context::CDO<bool> d_conflict;
 
+  /** Conflict when merging constants */
+  void conflict(TNode a, TNode b);
+
   /** The conflict node */
   Node d_conflictNode;