merge from arrays-clark branch

3 files changed, 76 insertions, 53 deletions

diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index d8757926a..4eabf63de 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -558,6 +558,11 @@ private:
   /** The false node */
   Node d_false;
 
+  /**
+   * Adds an equality of terms t1 and t2 to the database.
+   */
+  void addEqualityInternal(TNode t1, TNode t2, TNode reason);
+
 public:
 
   /**
@@ -617,6 +622,11 @@ public:
   bool hasTerm(TNode t) const;
 
   /**
+   * Adds aa predicate t with given polarity
+   */
+  void addPredicate(TNode t, bool polarity, TNode reason);
+
+  /**
    * Adds an equality t1 = t2 to the database.
    */
   void addEquality(TNode t1, TNode t2, TNode reason);
@@ -693,6 +703,13 @@ public:
    * Check whether the two term are dis-equal.
    */
   bool areDisequal(TNode t1, TNode t2);
+
+  /**
+   * Return the number of nodes in the equivalence class contianing t
+   * Adds t if not already there.
+   */
+  size_t getSize(TNode t);
+
 };
 
 } // Namespace uf
diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
index dd1bf0cbc..be12e5f19 100644
--- a/src/theory/uf/equality_engine_impl.h
+++ b/src/theory/uf/equality_engine_impl.h
@@ -188,9 +188,9 @@ const EqualityNode& EqualityEngine<NotifyClass>::getEqualityNode(EqualityNodeId
 }
 
 template <typename NotifyClass>
-void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason) {
+void EqualityEngine<NotifyClass>::addEqualityInternal(TNode t1, TNode t2, TNode reason) {
 
-  Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
+  Debug("equality") << "EqualityEngine::addEqualityInternal(" << t1 << "," << t2 << ")" << std::endl;
 
   // Add the terms if they are not already in the database
   addTerm(t1);
@@ -200,19 +200,39 @@ void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason)
   EqualityNodeId t1Id = getNodeId(t1);
   EqualityNodeId t2Id = getNodeId(t2);
   enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason));
+
   propagate();
 }
 
 template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addPredicate(TNode t, bool polarity, TNode reason) {
+
+  Debug("equality") << "EqualityEngine::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
+
+  addEqualityInternal(t, polarity ? d_true : d_false, reason);
+}
+
+template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::addEquality(TNode t1, TNode t2, TNode reason) {
+
+  Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl;
+
+  addEqualityInternal(t1, t2, reason);
+
+  Node equality = t1.eqNode(t2);
+  addEqualityInternal(equality, d_true, reason);
+}
+
+template <typename NotifyClass>
 void EqualityEngine<NotifyClass>::addDisequality(TNode t1, TNode t2, TNode reason) {
 
   Debug("equality") << "EqualityEngine::addDisequality(" << t1 << "," << t2 << ")" << std::endl;
 
   Node equality1 = t1.eqNode(t2);
-  addEquality(equality1, d_false, reason);
-
+  addEqualityInternal(equality1, d_false, reason);
+ 
   Node equality2 = t2.eqNode(t1);
-  addEquality(equality2, d_false, reason);
+  addEqualityInternal(equality2, d_false, reason);
 }
 
 
@@ -516,9 +536,6 @@ void EqualityEngine<NotifyClass>::explainEquality(TNode t1, TNode t2, std::vecto
   // Don't notify during this check
   ScopedBool turnOfNotify(d_performNotify, false);
 
-  // Push the context, so that we can remove the terms later
-  d_context->push();
-
   // Add the terms (they might not be there)
   addTerm(t1);
   addTerm(t2);
@@ -537,8 +554,6 @@ void EqualityEngine<NotifyClass>::explainEquality(TNode t1, TNode t2, std::vecto
   EqualityNodeId t2Id = getNodeId(t2);
   getExplanation(t1Id, t2Id, equalities);
 
-  // Pop the possible extra information
-  d_context->pop();
 }
 
 template <typename NotifyClass>
@@ -548,9 +563,6 @@ void EqualityEngine<NotifyClass>::explainDisequality(TNode t1, TNode t2, std::ve
   // Don't notify during this check
   ScopedBool turnOfNotify(d_performNotify, false);
 
-  // Push the context, so that we can remove the terms later
-  d_context->push();
-
   // Add the terms
   addTerm(t1);
   addTerm(t2);
@@ -573,8 +585,6 @@ void EqualityEngine<NotifyClass>::explainDisequality(TNode t1, TNode t2, std::ve
   EqualityNodeId falseId = getNodeId(d_false);
   getExplanation(equalityId, falseId, equalities);
 
-  // Pop the possible extra information
-  d_context->pop();
 }
 
 
@@ -722,6 +732,10 @@ void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode t
     }
   }
 
+  if (Debug.isOn("equality::internal")) {
+    debugPrintGraph();
+  }
+
   Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl;
 }
 
@@ -809,17 +823,11 @@ bool EqualityEngine<NotifyClass>::areEqual(TNode t1, TNode t2)
   // Don't notify during this check
   ScopedBool turnOfNotify(d_performNotify, false);
 
-  // Push the context, so that we can remove the terms later
-  d_context->push();
-
   // Add the terms
   addTerm(t1);
   addTerm(t2);
   bool equal = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
 
-  // Pop the context (triggers new term removal)
-  d_context->pop();
-
   // Return whether the two terms are equal
   return equal;
 }
@@ -830,9 +838,6 @@ bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2)
   // Don't notify during this check
   ScopedBool turnOfNotify(d_performNotify, false);
 
-  // Push the context, so that we can remove the terms later
-  d_context->push();
-
   // Add the terms
   addTerm(t1);
   addTerm(t2);
@@ -841,18 +846,22 @@ bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2)
   Node equality = t1.eqNode(t2);
   addTerm(equality);
   if (getEqualityNode(equality).getFind() == getEqualityNode(d_false).getFind()) {
-    d_context->pop();
     return true;
   }
 
-  // Pop the context (triggers new term removal)
-  d_context->pop();
-
   // Return whether the terms are disequal
   return false;
 }
 
 template <typename NotifyClass>
+size_t EqualityEngine<NotifyClass>::getSize(TNode t)
+{
+  // Add the term
+  addTerm(t);
+  return getEqualityNode(getEqualityNode(t).getFind()).getSize();
+}
+
+template <typename NotifyClass>
 void EqualityEngine<NotifyClass>::addTriggerTerm(TNode t) 
 {
   Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ")" << std::endl;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 4ac81bc74..f53918683 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -96,11 +96,11 @@ void TheoryUF::check(Effort level) {
       d_equalityEngine.addEquality(fact[0], fact[1], fact);
       break;
     case kind::APPLY_UF:
-      d_equalityEngine.addEquality(fact, d_true, fact);
+      d_equalityEngine.addPredicate(fact, true, fact);
       break;
     case kind::NOT:
       if (fact[0].getKind() == kind::APPLY_UF) {
-        d_equalityEngine.addEquality(fact[0], d_false, fact);
+        d_equalityEngine.addPredicate(fact[0], false, fact);
       } else {
         // Assert the dis-equality
         d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
@@ -132,24 +132,21 @@ void TheoryUF::propagate(Effort level) {
       TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
       Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl;
       bool satValue;
-      if (!d_valuation.hasSatValue(literal, satValue)) {
+      Node normalized = Rewriter::rewrite(literal);
+      if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
         d_out->propagate(literal);
       } else {
-        if (!satValue) {
-          Debug("uf") << "TheoryUF::propagate(): in conflict" << std::endl;
-          Node negatedLiteral;
-          std::vector<TNode> assumptions;
-          if (literal != d_false) {
-            negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
-            assumptions.push_back(negatedLiteral);
-          }
-          explain(literal, assumptions);
-          d_conflictNode = mkAnd(assumptions);
-          d_conflict = true;
-          break;
-        } else {
-          Debug("uf") << "TheoryUF::propagate(): already asserted" << std::endl;
+        Debug("uf") << "TheoryUF::propagate(): in conflict, normalized = " << normalized << std::endl;
+        Node negatedLiteral;
+        std::vector<TNode> assumptions;
+        if (normalized != d_false) {
+          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;
       }
     }
   }
@@ -196,20 +193,18 @@ bool TheoryUF::propagate(TNode literal) {
   }
 
   // See if the literal has been asserted already
+  Node normalized = Rewriter::rewrite(literal);
   bool satValue = false;
-  bool isAsserted = literal == d_false || d_valuation.hasSatValue(literal, satValue);
+  bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
 
   // If asserted, we're done or in conflict
   if (isAsserted) {
-    if (satValue) {
-      Debug("uf") << "TheoryUF::propagate(" << literal << ") => already known" << std::endl;
-      return true;
-    } else {
-      Debug("uf") << "TheoryUF::propagate(" << literal << ") => conflict" << std::endl;
+    if (!satValue) {
+      Debug("uf") << "TheoryUF::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
       std::vector<TNode> assumptions;
       Node negatedLiteral;
-      if (literal != d_false) {
-        negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
+      if (normalized != d_false) {
+        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
         assumptions.push_back(negatedLiteral);
       }
       explain(literal, assumptions);
@@ -217,6 +212,8 @@ bool TheoryUF::propagate(TNode literal) {
       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!)
   }
 
   // Nothing, just enqueue it for propagation and mark it as asserted already