Refactored the equality engine in order to remove theory-specific logic from equality path reconstruction

7 files changed, 224 insertions, 182 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 94ddf452a..77c69c9ec 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -287,6 +287,8 @@ libcvc4_la_SOURCES = \
 	theory/arrays/array_info.cpp \
 	theory/arrays/static_fact_manager.h \
 	theory/arrays/static_fact_manager.cpp \
+	theory/arrays/array_proof_reconstruction.cpp \
+	theory/arrays/array_proof_reconstruction.h \
 	theory/quantifiers/theory_quantifiers_type_rules.h \
 	theory/quantifiers/theory_quantifiers.h \
 	theory/quantifiers/quantifiers_rewriter.h \
diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
new file mode 100644
index 000000000..b2e8c3ab3
--- /dev/null
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -0,0 +1,121 @@
+/*********************                                                        */
+/*! \file array_proof_reconstruction.h
+ ** \verbatim
+ **
+ ** \brief Array-specific proof construction logic to be used during the
+ ** equality engine's path reconstruction
+ **/
+
+#include "theory/arrays/array_proof_reconstruction.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+ArrayProofReconstruction::ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine)
+  : d_equalityEngine(equalityEngine) {
+}
+
+void ArrayProofReconstruction::notify(eq::MergeReasonType reasonType, Node reason, Node a, Node b,
+                                      std::vector<TNode>& equalities, eq::EqProof* proof) const {
+
+  Debug("pf::array") << "ArrayProofReconstruction::notify( "
+                     << reason << ", " << a << ", " << b << std::endl;
+
+
+  switch (reasonType) {
+
+  case eq::MERGED_ARRAYS_EXT: {
+    if (proof) {
+      // Todo: here we assume that a=b is an assertion. We should probably call explain()
+      // recursively, to explain this.
+      eq::EqProof* childProof = new eq::EqProof;
+      childProof->d_node = reason;
+      proof->d_children.push_back(childProof);
+    }
+    break;
+  }
+
+  case eq::MERGED_ARRAYS_ROW: {
+    // ROW rules mean that (i==k) OR ((a[i]:=t)[k] == a[k])
+    // The equality here will be either (i == k) because ((a[i]:=t)[k] != a[k]),
+    // or ((a[i]:=t)[k] == a[k]) because (i != k).
+
+    if (proof) {
+      if (a.getNumChildren() == 2) {
+        // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k).
+
+        // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be
+        // false in the first case and true in the second case.
+        bool currentNodeIsUnchangedArray;
+
+        Assert(a.getNumChildren() == 2);
+        Assert(b.getNumChildren() == 2);
+
+        if (a[0].getKind() == kind::VARIABLE || a[0].getKind() == kind::SKOLEM) {
+          currentNodeIsUnchangedArray = true;
+        } else if (b[0].getKind() == kind::VARIABLE || b[0].getKind() == kind::SKOLEM) {
+          currentNodeIsUnchangedArray = false;
+        } else {
+          Assert(a[0].getKind() == kind::STORE);
+          Assert(b[0].getKind() == kind::STORE);
+
+          if (a[0][0] == b[0]) {
+            currentNodeIsUnchangedArray = false;
+          } else if (b[0][0] == a[0]) {
+            currentNodeIsUnchangedArray = true;
+          } else {
+            Unreachable();
+          }
+        }
+
+        Node indexOne = currentNodeIsUnchangedArray ? a[1] : a[0][1];
+        Node indexTwo = currentNodeIsUnchangedArray ? b[0][1] : b[1];
+
+        // Some assertions to ensure that the theory of arrays behaves as expected
+        Assert(a[1] == b[1]);
+        if (currentNodeIsUnchangedArray) {
+          Assert(a[0] == b[0][0]);
+        } else {
+          Assert(a[0][0] == b[0]);
+        }
+
+        Debug("pf::ee") << "Getting explanation for ROW guard: "
+                        << indexOne << " != " << indexTwo << std::endl;
+
+        eq::EqProof* childProof = new eq::EqProof;
+        d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof);
+        proof->d_children.push_back(childProof);
+      } else {
+        // This is the case of  (i == k) because ((a[i]:=t)[k] != a[k]),
+
+        Node indexOne = a;
+        Node indexTwo = b;
+
+        Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl
+                        << "The reason for the edge is: " << reason << std::endl;
+
+        Assert(reason.getNumChildren() == 2);
+        Debug("pf::ee") << "Getting explanation for ROW guard: " << reason[1] << std::endl;
+
+        eq::EqProof* childProof = new eq::EqProof;
+        d_equalityEngine->explainEquality(reason[1][0], reason[1][1], false, equalities, childProof);
+        proof->d_children.push_back(childProof);
+      }
+    }
+    break;
+  }
+
+  case eq::MERGED_ARRAYS_ROW1: {
+    // No special handling required at this time
+    break;
+  }
+
+  default:
+    break;
+  }
+}
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h
new file mode 100644
index 000000000..8afc0d3f7
--- /dev/null
+++ b/src/theory/arrays/array_proof_reconstruction.h
@@ -0,0 +1,40 @@
+/*********************                                                        */
+/*! \file array_proof_reconstruction.h
+ ** \verbatim
+ **
+ ** \brief Array-specific proof construction logic to be used during the
+ ** equality engine's path reconstruction
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
+#define __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H
+
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+/**
+ * A callback class to be invoked whenever the equality engine traverses
+ * an "array-owned" edge during path reconstruction.
+ */
+
+class ArrayProofReconstruction : public eq::PathReconstructionNotify {
+public:
+  ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine);
+
+  void notify(eq::MergeReasonType reasonType, Node reason, Node a, Node b,
+              std::vector<TNode>& equalities, eq::EqProof* proof) const;
+
+private:
+  const eq::EqualityEngine* d_equalityEngine;
+}; /* class ArrayProofReconstruction */
+
+}/* CVC4::theory::arrays namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__ARRAYS__ARRAY_PROOF_RECONSTRUCTION_H */
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index fcde18b66..37854ee90 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -99,7 +99,8 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
       d_defValues(c),
       d_readTableContext(new context::Context()),
       d_arrayMerges(c),
-      d_inCheckModel(false)
+      d_inCheckModel(false),
+      d_proofReconstruction(&d_equalityEngine)
 {
   smtStatisticsRegistry()->registerStat(&d_numRow);
   smtStatisticsRegistry()->registerStat(&d_numExt);
@@ -127,6 +128,10 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u,
   if (d_useArrTable) {
     d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN);
   }
+
+  d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_ROW, &d_proofReconstruction);
+  d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_ROW1, &d_proofReconstruction);
+  d_equalityEngine.addPathReconstructionTrigger(eq::MERGED_ARRAYS_EXT, &d_proofReconstruction);
 }
 
 TheoryArrays::~TheoryArrays() {
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 2f69c52f9..6d2bb9e73 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -23,6 +23,7 @@
 #include "context/cdhashset.h"
 #include "context/cdqueue.h"
 #include "theory/arrays/array_info.h"
+#include "theory/arrays/array_proof_reconstruction.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 #include "util/statistics_registry.h"
@@ -430,6 +431,9 @@ class TheoryArrays : public Theory {
   bool d_inCheckModel;
   int d_topLevel;
 
+  /** An equality-engine callback for proof reconstruction */
+  ArrayProofReconstruction d_proofReconstruction;
+
   public:
 
   eq::EqualityEngine* getEqualityEngine() {
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 53347c365..48aee1c35 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -943,10 +943,6 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
     DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second;
 
     for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
-      EqualityPair toExplain = d_deducedDisequalityReasons[i];
-    }
-
-    for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
 
       EqualityPair toExplain = d_deducedDisequalityReasons[i];
       EqProof* eqpc = NULL;
@@ -956,15 +952,8 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
         eqpc = new EqProof;
       }
 
-      // Some edges have the form ((a == b) == false). Translate this into (not (a == b)).
-      // Assert(d_nodes[toExplain.first] != NodeManager::currentNM()->mkConst(false));
-
       getExplanation(toExplain.first, toExplain.second, equalities, eqpc);
 
-      // if (eqpc) {
-      //   eqp->d_children.push_back(eqpc);
-      // }
-
       if (eqpc) {
         Debug("pf::ee") << "Child proof is:" << std::endl;
         eqpc->debug_print("pf::ee", 1);
@@ -1101,6 +1090,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             currentNode = bfsQueue[currentIndex].nodeId;
             EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId();
             MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType();
+            Node reason = d_equalityEdges[currentEdge].getReason();
 
             Debug("equality") << d_name << "::eq::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl;
             Debug("equality") << d_name << "                     targetNode = " << d_nodes[edgeNode] << std::endl;
@@ -1113,6 +1103,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               eqpc = new EqProof;
               eqpc->d_id = reasonType;
             }
+
             // Add the actual equality to the vector
             switch (reasonType) {
             case MERGED_THROUGH_CONGRUENCE: {
@@ -1121,10 +1112,6 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               const FunctionApplication& f1 = d_applications[currentNode].original;
               const FunctionApplication& f2 = d_applications[edgeNode].original;
 
-              Debug("pf::ee") << "We need to prove two equalities:" << std::endl;
-              Debug("pf::ee") << "\tLHS: " << d_nodes[f1.a] << " = " << d_nodes[f2.a] << std::endl;
-              Debug("pf::ee") << "\tRHS: " << d_nodes[f1.b] << " = " << d_nodes[f2.b] << std::endl;
-
               Debug("equality") << push;
               Debug("equality") << "Explaining left hand side equalities" << std::endl;
               EqProof * eqpc1 = eqpc ? new EqProof : NULL;
@@ -1135,51 +1122,36 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               if( eqpc ){
                 eqpc->d_children.push_back( eqpc1 );
                 eqpc->d_children.push_back( eqpc2 );
-                Debug("pf::ee") << "Congruence : " << d_nodes[currentNode] << " " << d_nodes[edgeNode] << std::endl;
                 if( d_nodes[currentNode].getKind()==kind::EQUAL ){
                   //leave node null for now
                   eqpc->d_node = Node::null();
-                }else{
-                  Debug("pf::ee") << d_nodes[f1.a] << " / " << d_nodes[f2.a] << ", " << d_nodes[f1.b] << " / " << d_nodes[f2.b] << std::endl;
+                } else {
                   if(d_nodes[f1.a].getKind() == kind::APPLY_UF ||
                      d_nodes[f1.a].getKind() == kind::SELECT ||
                      d_nodes[f1.a].getKind() == kind::STORE) {
                     eqpc->d_node = d_nodes[f1.a];
                   } else {
-
-                    Debug("pf::ee") << "f1.a is: " << d_nodes[f1.a]
-                                    << ". kind is: " << d_nodes[f1.a].getKind() << std::endl;
-
                     if (d_nodes[f1.a].getKind() == kind::BUILTIN && d_nodes[f1.a].getConst<Kind>() == kind::SELECT) {
-                      Debug("pf::ee") << "f1.a getConst<kind> is: " << d_nodes[f1.a].getConst<Kind>() << std::endl;
-
                       eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_1, d_nodes[f1.b]);
-                      // The first child is a PARTIAL_SELECT_0. Give it a child so that we know what kind of (read) it is, when we dump to LFSC.
-                      Debug("pf::ee") << "eqpc->d_children[0]->d_node.getKind() == " << eqpc->d_children[0]->d_node.getKind() << std::endl;
+                      // The first child is a PARTIAL_SELECT_0.
+                      // Give it a child so that we know what kind of (read) it is, when we dump to LFSC.
                       Assert(eqpc->d_children[0]->d_node.getKind() == kind::PARTIAL_SELECT_0);
                       Assert(eqpc->d_children[0]->d_children.size() == 0);
 
-                      Debug("pf::ee") << "Dumping the equality proof before:" << std::endl;
-                      eqpc->debug_print("pf::ee", 1);
-
-                      eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0, d_nodes[f1.b]);
-
-                      Debug("pf::ee") << "Dumping the equality proof after:" << std::endl;
-                      eqpc->debug_print("pf::ee", 1);
-
-                      //eqpc->d_children[0]->d_node.append(d_nodes[f1.b]);
+                      eqpc->d_children[0]->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_SELECT_0,
+                                                                                     d_nodes[f1.b]);
                     } else {
                       eqpc->d_node = NodeManager::currentNM()->mkNode(kind::PARTIAL_APPLY_UF,
                                                                       ProofManager::currentPM()->mkOp(d_nodes[f1.a]),
                                                                       d_nodes[f1.b]);
                     }
-                    Debug("pf::ee") << "New d_node is: " << eqpc->d_node << std::endl;
                   }
                 }
               }
               Debug("equality") << pop;
               break;
             }
+
             case MERGED_THROUGH_REFLEXIVITY: {
               // x1 == x1
               Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl;
@@ -1198,6 +1170,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
               break;
             }
+
             case MERGED_THROUGH_CONSTANTS: {
               // f(c1, ..., cn) = c semantically, we can just ignore it
               Debug("equality") << d_name << "::eq::getExplanation(): due to constants, explain the constants" << std::endl;
@@ -1221,169 +1194,41 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               }
 
               Debug("equality") << pop;
-
-              break;
-            }
-            case MERGED_ARRAYS_EXT:
-
-              Debug("equality") << d_name << "::eq::getExplanation(): MERGED_ARRAYS_EXT" << std::endl;
-
-              if (eqpc) {
-                Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
-                Node b = d_nodes[currentNode];
-
-                // GK: todo: here we assume that a=b is an assertion. We should probably call explain()
-                // recursively, to explain this.
-
-                if (a == NodeManager::currentNM()->mkConst(false)) {
-                  eqpc->d_node = b.notNode();
-                } else if (b == NodeManager::currentNM()->mkConst(false)) {
-                  eqpc->d_node = a.notNode();
-                } else {
-                  eqpc->d_node = a.eqNode(b);
-                }
-
-                EqProof* eqpc1 = new EqProof;
-                eqpc1->d_node = d_equalityEdges[currentEdge].getReason();
-                eqpc->d_children.push_back( eqpc1 );
-
-                eqpc1->debug_print("pf::ee", 1);
-                eqpc->debug_print("pf::ee", 1);
-              }
-
-              // We push the reason into "equalities" because that's what the theory of arrays expects.
-              equalities.push_back(d_equalityEdges[currentEdge].getReason());
-              break;
-
-            case MERGED_ARRAYS_ROW: {
-              Debug("equality") << d_name << "::eq::getExplanation(): MERGED_ARRAYS_ROW" << std::endl;
-
-              // ROW rules mean that (i==k) OR ((a[i]:=t)[k] == a[k])
-              // The equality here will be either (i == k) because ((a[i]:=t)[k] != a[k]),
-              // or ((a[i]:=t)[k] == a[k]) because (i != k).
-
-              if (eqpc) {
-                if (d_nodes[currentNode].getNumChildren() == 2) {
-                  // This is the case of ((a[i]:=t)[k] == a[k]) because (i != k).
-
-                  // The edge is ((a[i]:=t)[k], a[k]), or (a[k], (a[i]:=t)[k]). This flag should be
-                  // false in the first case and true in the second case.
-                  bool currentNodeIsUnchangedArray;
-
-                  Assert(d_nodes[currentNode].getNumChildren() == 2);
-                  Assert(d_nodes[edgeNode].getNumChildren() == 2);
-
-                  if (d_nodes[currentNode][0].getKind() == kind::VARIABLE ||
-                      d_nodes[currentNode][0].getKind() == kind::SKOLEM) {
-                    currentNodeIsUnchangedArray = true;
-                  } else if (d_nodes[edgeNode][0].getKind() == kind::VARIABLE ||
-                             d_nodes[edgeNode][0].getKind() == kind::SKOLEM) {
-                    currentNodeIsUnchangedArray = false;
-                  } else {
-                    Assert(d_nodes[currentNode][0].getKind() == kind::STORE);
-                    Assert(d_nodes[edgeNode][0].getKind() == kind::STORE);
-
-                    if (d_nodes[currentNode][0][0] == d_nodes[edgeNode][0]) {
-                      currentNodeIsUnchangedArray = false;
-                    } else if (d_nodes[edgeNode][0][0] == d_nodes[currentNode][0]) {
-                      currentNodeIsUnchangedArray = true;
-                    } else {
-                      Unreachable();
-                    }
-                  }
-
-                  Node indexOne =
-                    currentNodeIsUnchangedArray ? d_nodes[currentNode][1] : d_nodes[currentNode][0][1];
-                  Node indexTwo =
-                    currentNodeIsUnchangedArray ? d_nodes[edgeNode][0][1] : d_nodes[edgeNode][1];
-
-                  // Some assertions to ensure that the theory of arrays behaves as expected
-                  Assert(d_nodes[currentNode][1] == d_nodes[edgeNode][1]);
-                  if (currentNodeIsUnchangedArray) {
-                    Assert(d_nodes[currentNode][0] == d_nodes[edgeNode][0][0]);
-                  } else {
-                    Assert(d_nodes[currentNode][0][0] == d_nodes[edgeNode][0]);
-                  }
-
-                  Debug("pf::ee") << "Getting explanation for ROW guard: "
-                                     << indexOne << " != " << indexTwo << std::endl;
-
-                  EqProof* eqpcc = eqpc ? new EqProof : NULL;
-                  explainEquality(indexOne, indexTwo, false, equalities, eqpcc);
-
-                  Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl;
-                  Debug("pf::ee") << "And the explanation of their disequality is: " << std::endl;
-                  eqpcc->debug_print("pf::ee", 1);
-                  eqpc->d_children.push_back(eqpcc);
-                } else {
-                  // This is the case of  (i == k) because ((a[i]:=t)[k] != a[k]),
-
-                  Debug("pf::ee") << "In the new case of ROW!" << std::endl;
-
-                  Node indexOne = d_nodes[currentNode];
-                  Node indexTwo = d_nodes[edgeNode];
-
-                  Debug("pf::ee") << "The two indices are: " << indexOne << ", " << indexTwo << std::endl;
-                  Debug("pf::ee") << "The reason for the edge is: " << d_equalityEdges[currentEdge].getReason()
-                                     << std::endl;
-
-                  Assert(d_equalityEdges[currentEdge].getReason().getNumChildren() == 2);
-                  Node reason = d_equalityEdges[currentEdge].getReason()[1];
-                  Debug("pf::ee") << "Getting explanation for ROW guard: " << reason << std::endl;
-
-                  EqProof* eqpcc = eqpc ? new EqProof : NULL;
-                  explainEquality(reason[0], reason[1], false, equalities, eqpcc);
-
-                  if (eqpc) {
-                    Debug("pf::ee") << "The guard's explanation is: " << std::endl;
-                    eqpcc->debug_print("pf::ee", 1);
-                    eqpc->d_children.push_back(eqpcc);
-                  }
-                }
-
-                Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
-                Node b = d_nodes[currentNode];
-
-                if (a == NodeManager::currentNM()->mkConst(false)) {
-                  eqpc->d_node = b.notNode();
-                } else if (b == NodeManager::currentNM()->mkConst(false)) {
-                  eqpc->d_node = a.notNode();
-                } else {
-                  eqpc->d_node = a.eqNode(b);
-                }
-              }
-
-              // We push the reason into "equalities" because that's what the theory of arrays expects.
-              equalities.push_back(d_equalityEdges[currentEdge].getReason());
               break;
             }
 
             default: {
               // Construct the equality
-              Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl;
+              Debug("equality") << d_name << "::eq::getExplanation(): adding: "
+                                << reason << std::endl;
               Debug("equality") << d_name << "::eq::getExplanation(): reason type = " << reasonType << std::endl;
 
+              Node a = d_nodes[currentNode];
+              Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
+
+              if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) {
+                d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b,
+                                                                              equalities, eqpc);
+              }
+
               if (eqpc) {
                 if (reasonType == MERGED_THROUGH_EQUALITY) {
-                  eqpc->d_node = d_equalityEdges[currentEdge].getReason();
+                  eqpc->d_node = reason;
                 } else {
-                  // The LFSC translator prefers (not (= a b)) over (= (a==b) false)
-
-                  Node a = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
-                  Node b = d_nodes[currentNode];
+                  // The LFSC translator prefers (not (= a b)) over (= (= a b) false)
 
                   if (a == NodeManager::currentNM()->mkConst(false)) {
                     eqpc->d_node = b.notNode();
                   } else if (b == NodeManager::currentNM()->mkConst(false)) {
                     eqpc->d_node = a.notNode();
                   } else {
-                    eqpc->d_node = a.eqNode(b);
+                    eqpc->d_node = b.eqNode(a);
                   }
-                  Debug("pf::ee") << "theory eq : " << eqpc->d_node << std::endl;
                 }
                 eqpc->d_id = reasonType;
               }
-              equalities.push_back(d_equalityEdges[currentEdge].getReason());
+
+              equalities.push_back(reason);
               break;
             }
             }
@@ -1859,13 +1704,19 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
   return false;
 }
 
-size_t EqualityEngine::getSize(TNode t)
-{
+size_t EqualityEngine::getSize(TNode t) {
   // Add the term
   addTermInternal(t);
   return getEqualityNode(getEqualityNode(t).getFind()).getSize();
 }
 
+
+void EqualityEngine::addPathReconstructionTrigger(MergeReasonType trigger, const PathReconstructionNotify* notify) {
+  // Currently we can only inform one callback per trigger
+  Assert(d_pathReconstructionTriggers.find(trigger) == d_pathReconstructionTriggers.end());
+  d_pathReconstructionTriggers[trigger] = notify;
+}
+
 void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
 {
   Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 9cfa16adf..97abfccf1 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -140,6 +140,18 @@ public:
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
 };/* class EqualityEngineNotifyNone */
 
+/**
+ * An interface for equality engine notifications during equality path reconstruction.
+ * Can be used to add theory-specific logic for, e.g., proof construction.
+ */
+class PathReconstructionNotify {
+public:
+
+  virtual ~PathReconstructionNotify() {}
+
+  virtual void notify(MergeReasonType reasonType, Node reason, Node a, Node b,
+                      std::vector<TNode>& equalities, EqProof* proof) const = 0;
+};
 
 /**
  * Class for keeping an incremental congruence closure over a set of terms. It provides
@@ -218,6 +230,9 @@ private:
   /** The map of kinds to be treated as interpreted function applications (for evaluation of constants) */
   KindMap d_congruenceKindsInterpreted;
 
+  /** Objects that need to be notified during equality path reconstruction */
+  std::map<MergeReasonType, const PathReconstructionNotify*> d_pathReconstructionTriggers;
+
   /** Map from nodes to their ids */
   __gnu_cxx::hash_map<TNode, EqualityNodeId, TNodeHashFunction> d_nodeIds;
 
@@ -833,6 +848,10 @@ public:
    */
   bool consistent() const { return !d_done; }
 
+  /**
+   * Marks an object for merge type based notification during equality path reconstruction.
+   */
+  void addPathReconstructionTrigger(MergeReasonType trigger, const PathReconstructionNotify* notify);
 };
 
 /**