* merging some uf stuff from incremental_work branch that somehow nobody merged-in

* since two theories can propagate the same literal minisat now explicitly checks that a propagated literal has not been asserted yet

5 files changed, 69 insertions, 15 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 8a883b1cb..e1a8ded8e 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -698,9 +698,18 @@ CRef Solver::propagate(TheoryCheckType type)
 void Solver::propagateTheory() {
   std::vector<Lit> propagatedLiterals;
   proxy->theoryPropagate(propagatedLiterals);
+  int oldTrailSize = trail.size();
   for (unsigned i = 0, i_end = propagatedLiterals.size(); i < i_end; ++ i) {
     Debug("minisat") << "Theory propagated: " << propagatedLiterals[i] << std::endl;
-    uncheckedEnqueue(propagatedLiterals[i], CRef_Lazy);
+    // multiple theories can propagate the same literal
+    Lit p = propagatedLiterals[i];
+    if (value(p) == l_Undef) {
+      uncheckedEnqueue(p, CRef_Lazy);
+    } else {
+      // but we check that this is the case and that they agree
+      Assert(trail_index(var(p)) >= oldTrailSize);
+      Assert(value(p) == lbool(!sign(p)));
+    }
   }
 }
 
diff --git a/src/theory/arith/difference_manager.cpp b/src/theory/arith/difference_manager.cpp
index dfb07bcf4..f366116d4 100644
--- a/src/theory/arith/difference_manager.cpp
+++ b/src/theory/arith/difference_manager.cpp
@@ -33,7 +33,7 @@ void DifferenceManager::explain(TNode literal, std::vector<TNode>& assumptions)
     default:
       Unreachable();
   }
-  d_ee.getExplanation(lhs, rhs, assumptions);
+  d_ee.explainEquality(lhs, rhs, assumptions);
 }
 
 #warning "Stolen from theory_uf.h verbatim. Generalize me!"
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 13b8898d5..01ae6bfb4 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -613,9 +613,16 @@ public:
   /**
    * Get an explanation of the equality t1 = t2. Returns the asserted equalities that
    * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
-   * else. TODO: mark the phantom equalities (skolems).
+   * else. 
+   */
+  void explainEquality(TNode t1, TNode t2, std::vector<TNode>& equalities) const;
+
+  /**
+   * Get an explanation of the equality t1 = t2. Returns the asserted equalities that
+   * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
+   * else. 
    */
-  void getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const;
+  void explainDisequality(TNode t1, TNode t2, std::vector<TNode>& equalities) const;
 
   /**
    * Add term to the trigger terms. The notify class will get notified when two 
diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
index 77c8e80b4..61823c143 100644
--- a/src/theory/uf/equality_engine_impl.h
+++ b/src/theory/uf/equality_engine_impl.h
@@ -549,10 +549,17 @@ std::string EqualityEngine<NotifyClass>::edgesToString(EqualityEdgeId edgeId) co
 }
 
 template <typename NotifyClass>
-void EqualityEngine<NotifyClass>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
-  Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl;
-
-  Assert(getRepresentative(t1) == getRepresentative(t2));
+void EqualityEngine<NotifyClass>::explainEquality(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
+  Debug("equality") << "EqualityEngine::explainEquality(" << t1 << "," << t2 << ")" << std::endl;
+
+  Assert(getRepresentative(t1) == getRepresentative(t2),
+         "Cannot explain an equality, because the two terms are not equal!\n"
+         "The representative of %s\n"
+         "                   is %s\n"
+         "The representative of %s\n"
+         "                   is %s",
+         t1.toString().c_str(), getRepresentative(t1).toString().c_str(),
+         t2.toString().c_str(), getRepresentative(t2).toString().c_str());
 
   // Get the explanation
   EqualityNodeId t1Id = getNodeId(t1);
@@ -561,6 +568,28 @@ void EqualityEngine<NotifyClass>::getExplanation(TNode t1, TNode t2, std::vector
 }
 
 template <typename NotifyClass>
+void EqualityEngine<NotifyClass>::explainDisequality(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
+  Debug("equality") << "EqualityEngine::explainDisequality(" << t1 << "," << t2 << ")" << std::endl;
+
+  Node equality = t1.eqNode(t2);
+
+  Assert(getRepresentative(equality) == getRepresentative(d_false),
+         "Cannot explain the dis-equality, because the two terms are not dis-equal!\n"
+         "The representative of %s\n"
+         "                   is %s\n"
+         "The representative of %s\n"
+         "                   is %s",
+         equality.toString().c_str(), getRepresentative(equality).toString().c_str(),
+         d_false.toString().c_str(), getRepresentative(d_false).toString().c_str());
+
+  // Get the explanation 
+  EqualityNodeId equalityId = getNodeId(equality);
+  EqualityNodeId falseId = getNodeId(d_false);
+  getExplanation(equalityId, falseId, equalities);
+}
+
+
+template <typename NotifyClass>
 void EqualityEngine<NotifyClass>::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities) const {
 
   Debug("equality") << "EqualityEngine::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl;
@@ -672,12 +701,12 @@ void EqualityEngine<NotifyClass>::addTriggerEquality(TNode t1, TNode t2, TNode t
   // Get the information about t1
   EqualityNodeId t1Id = getNodeId(t1);
   EqualityNodeId t1classId = getEqualityNode(t1Id).getFind();
-  TriggerId t1TriggerId = d_nodeTriggers[t1Id];
+  TriggerId t1TriggerId = d_nodeTriggers[t1classId];
 
   // Get the information about t2
   EqualityNodeId t2Id = getNodeId(t2);
   EqualityNodeId t2classId = getEqualityNode(t2Id).getFind();
-  TriggerId t2TriggerId = d_nodeTriggers[t2Id];
+  TriggerId t2TriggerId = d_nodeTriggers[t2classId];
 
   Debug("equality") << "EqualityEngine::addTrigger(" << trigger << "): " << t1Id << " (" << t1classId << ") = " << t2Id << " (" << t2classId << ")" << std::endl;
 
@@ -836,6 +865,7 @@ bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2)
   Node equality1 = t1.eqNode(t2);
   addTerm(equality1);
   if (getEqualityNode(equality1).getFind() == getEqualityNode(d_false).getFind()) {
+    d_context->pop();
     return true;
   }
 
@@ -843,6 +873,7 @@ bool EqualityEngine<NotifyClass>::areDisequal(TNode t1, TNode t2)
   Node equality2 = t2.eqNode(t1);
   addTerm(equality2);
   if (getEqualityNode(equality2).getFind() == getEqualityNode(d_false).getFind()) {
+    d_context->pop();
     return true;
   }
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 58fa44358..e2462f244 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -236,9 +236,16 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
       rhs = d_true;
       break;
     case kind::NOT:
-      lhs = literal[0];
-      rhs = d_false;
-      break;
+      if (literal[0].getKind() == kind::EQUAL) {
+        // Disequalities
+        d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
+        return;
+      } else {
+        // Predicates
+        lhs = literal[0];
+        rhs = d_false;
+        break;
+      }
     case kind::CONST_BOOLEAN:
       // we get to explain true = false, since we set false to be the trigger of this
       lhs = d_true;
@@ -247,8 +254,8 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
     default:
       Unreachable();
   }
-  d_equalityEngine.getExplanation(lhs, rhs, assumptions);
-}/* TheoryUF::explain() */
+  d_equalityEngine.explainEquality(lhs, rhs, assumptions);
+}
 
 Node TheoryUF::explain(TNode literal) {
   Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;