some immediate bug fixes

diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
index 292761c46ba103836555379693c102235c2d771f..a19ec8d66736b6762bb9f6685bb3780452940acd 100644 (file)
--- a/src/theory/uf/equality_engine_impl.h
+++ b/src/theory/uf/equality_engine_impl.h
@@ -474,10 +474,10 @@ std::string EqualityEngine<NotifyClass>::edgesToString(EqualityEdgeId edgeId) co
 
 template <typename NotifyClass>
 void EqualityEngine<NotifyClass>::getExplanation(TNode t1, TNode t2, std::vector<TNode>& equalities) const {
-  Assert(getRepresentative(t1) == getRepresentative(t2));
-
   Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl;
 
+  Assert(getRepresentative(t1) == getRepresentative(t2));
+
   // Backtrack if necessary
   const_cast<EqualityEngine*>(this)->backtrack();
 

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 8caac6fb721df6cdea2a78b72527bcc5ce1c00ee..7688379d9ef4caefc60f0a8fcc69132b132be461 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -139,18 +139,15 @@ void TheoryUF::preRegisterTerm(TNode node) {
   }
 }
 
-bool TheoryUF::propagate(TNode atom, bool isTrue) {
-  Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ")" << std::endl;
+bool TheoryUF::propagate(TNode literal) {
+  Debug("uf") << "TheoryUF::propagate(" << literal  << ")" << std::endl;
 
   // If already in conflict, no more propagation
   if (d_conflict) {
-    Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << "): already in conflict" << std::endl;
+    Debug("uf") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
     return false;
   }
 
-  // The literal
-  TNode literal = isTrue ? (Node) atom : atom.notNode();
-
   // See if the literal has been asserted already
   bool satValue = false;
   bool isAsserted = literal == d_false || d_valuation.hasSatValue(literal, satValue);
@@ -158,13 +155,13 @@ bool TheoryUF::propagate(TNode atom, bool isTrue) {
   // If asserted, we're done or in conflict
   if (isAsserted) {
     if (satValue) {
-      Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => already known" << std::endl;
+      Debug("uf") << "TheoryUF::propagate(" << literal << ") => already known" << std::endl;
       return true;
     } else {
-      Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => conflict" << std::endl;
+      Debug("uf") << "TheoryUF::propagate(" << literal << ") => conflict" << std::endl;
       std::vector<TNode> assumptions;
       if (literal != d_false) {
-        TNode negatedLiteral = isTrue ? atom.notNode() : (Node) atom;
+        TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode();
         assumptions.push_back(negatedLiteral);
       }
       explain(literal, assumptions);
@@ -175,7 +172,7 @@ bool TheoryUF::propagate(TNode atom, bool isTrue) {
   }
 
   // Nothing, just enqueue it for propagation and mark it as asserted already
-  Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => enqueuing for propagation" << std::endl;
+  Debug("uf") << "TheoryUF::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
   d_literalsToPropagate.push_back(literal);
 
   return true;
@@ -195,6 +192,7 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
     case kind::NOT:
       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;

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index c77d5a8101880dce67700ec18769bddbe6c7be5f..eaab96f27a6ea31be1b94b9d00db94a48d053d71 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -44,10 +44,10 @@ public:
   public:
     NotifyClass(TheoryUF& uf): d_uf(uf) {}
 
-    bool notifyEquality(TNode eq) {
-      Debug("uf") << "NotifyClass::notifyEquality(" << eq << ")" << std::endl;
+    bool notifyEquality(TNode reason) {
+      Debug("uf") << "NotifyClass::notifyEquality(" << reason << ")" << std::endl;
       // Just forward to uf
-      return d_uf.propagate(eq, true);
+      return d_uf.propagate(reason);
     }
   };
 
@@ -69,10 +69,9 @@ private:
   Node d_conflictNode;
 
   /**
-   * Should be called to propagate the atom. If isTrue is true, the atom should be propagated,
-   * otherwise the negated atom should be propagated.
+   * Should be called to propagate the literal. 
    */
-  bool propagate(TNode atom, bool isTrue);
+  bool propagate(TNode literal);
 
   /**
    * Explain why this literal is true by adding assumptions