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

4 files changed, 171 insertions, 1 deletions

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() {