Switching EqProof to use shared_ptr everywhere. (#1217)

This clarifies the memory ownership of EqProofs.

7 files changed, 94 insertions, 62 deletions

diff --git a/src/theory/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
index 471084d6f..29dfe9b47 100644
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -17,6 +17,8 @@
 
 #include "theory/arrays/array_proof_reconstruction.h"
 
+#include <memory>
+
 namespace CVC4 {
 namespace theory {
 namespace arrays {
@@ -37,18 +39,18 @@ void ArrayProofReconstruction::setExtMergeTag(unsigned tag) {
   d_reasonExt = tag;
 }
 
-void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a, Node b,
-                                      std::vector<TNode>& equalities, eq::EqProof* proof) const {
-
+void ArrayProofReconstruction::notify(
+    unsigned 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;
 
 
   if (reasonType == d_reasonExt) {
     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;
+      // Todo: here we assume that a=b is an assertion. We should probably call
+      // explain() recursively, to explain this.
+      std::shared_ptr<eq::EqProof> childProof = std::make_shared<eq::EqProof>();
       childProof->d_node = reason;
       proof->d_children.push_back(childProof);
     }
@@ -101,12 +103,13 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
         Debug("pf::ee") << "Getting explanation for ROW guard: "
                         << indexOne << " != " << indexTwo << std::endl;
 
+        std::shared_ptr<eq::EqProof> childProof =
+            std::make_shared<eq::EqProof>();
+        d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities,
+                                          childProof.get());
 
-        eq::EqProof* childProof = new eq::EqProof;
-        d_equalityEngine->explainEquality(indexOne, indexTwo, false, equalities, childProof);
-
-        // It could be that the guard condition is a constant disequality. In this case,
-        // we need to change it to a different format.
+        // It could be that the guard condition is a constant disequality. In
+        // this case, we need to change it to a different format.
         bool haveNegChild = false;
         for (unsigned i = 0; i < childProof->d_children.size(); ++i) {
           if (childProof->d_children[i]->d_node.getKind() == kind::NOT)
@@ -145,13 +148,15 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
             }
           }
 
-          eq::EqProof* constantDisequalityProof = new eq::EqProof;
+          std::shared_ptr<eq::EqProof> constantDisequalityProof =
+              std::make_shared<eq::EqProof>();
           constantDisequalityProof->d_id = theory::eq::MERGED_THROUGH_CONSTANTS;
           constantDisequalityProof->d_node =
             NodeManager::currentNM()->mkNode(kind::EQUAL, constantOne, constantTwo).negate();
 
           // Middle is where we need to insert the new disequality
-          std::vector<eq::EqProof *>::iterator middle = childProof->d_children.begin();
+          std::vector<std::shared_ptr<eq::EqProof>>::iterator middle =
+              childProof->d_children.begin();
           ++middle;
 
           childProof->d_children.insert(middle, constantDisequalityProof);
@@ -174,8 +179,10 @@ void ArrayProofReconstruction::notify(unsigned reasonType, Node reason, Node a,
         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);
+        std::shared_ptr<eq::EqProof> childProof =
+            std::make_shared<eq::EqProof>();
+        d_equalityEngine->explainEquality(reason[1][0], reason[1][1], false,
+                                          equalities, childProof.get());
         proof->d_children.push_back(childProof);
       }
     }
diff --git a/src/theory/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h
index c5ba21569..1b06dc524 100644
--- a/src/theory/arrays/array_proof_reconstruction.h
+++ b/src/theory/arrays/array_proof_reconstruction.h
@@ -34,7 +34,8 @@ public:
   ArrayProofReconstruction(const eq::EqualityEngine* equalityEngine);
 
   void notify(unsigned reasonType, Node reason, Node a, Node b,
-              std::vector<TNode>& equalities, eq::EqProof* proof) const;
+              std::vector<TNode>& equalities,
+              eq::EqProof* proof) const override;
 
   void setRowMergeTag(unsigned tag);
   void setRow1MergeTag(unsigned tag);
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index a17f506de..b43ba5591 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -17,6 +17,7 @@
 #include "theory/arrays/theory_arrays.h"
 
 #include <map>
+#include <memory>
 
 #include "expr/kind.h"
 #include "options/arrays_options.h"
@@ -395,7 +396,8 @@ bool TheoryArrays::propagate(TNode literal)
 }/* TheoryArrays::propagate(TNode) */
 
 
-void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof) {
+void TheoryArrays::explain(TNode literal, std::vector<TNode>& assumptions,
+                           eq::EqProof* proof) {
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
@@ -831,16 +833,15 @@ Node TheoryArrays::explain(TNode literal) {
   return explanation;
 }
 
-Node TheoryArrays::explain(TNode literal, eq::EqProof *proof)
-{
+Node TheoryArrays::explain(TNode literal, eq::EqProof* proof) {
   ++d_numExplain;
-  Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::explain(" << literal << ")" << std::endl;
+  Debug("arrays") << spaces(getSatContext()->getLevel())
+                  << "TheoryArrays::explain(" << literal << ")" << std::endl;
   std::vector<TNode> assumptions;
   explain(literal, assumptions, proof);
   return mkAnd(assumptions);
 }
 
-
 /////////////////////////////////////////////////////////////////////////////
 // SHARING
 /////////////////////////////////////////////////////////////////////////////
@@ -2238,9 +2239,10 @@ bool TheoryArrays::dischargeLemmas()
 
 void TheoryArrays::conflict(TNode a, TNode b) {
   Debug("pf::array") << "TheoryArrays::Conflict called" << std::endl;
-  eq::EqProof* proof = d_proofsEnabled ? new eq::EqProof() : NULL;
+  std::shared_ptr<eq::EqProof> proof = d_proofsEnabled ?
+      std::make_shared<eq::EqProof>() : nullptr;
 
-  d_conflictNode = explain(a.eqNode(b), proof);
+  d_conflictNode = explain(a.eqNode(b), proof.get());
 
   if (!d_inCheckModel) {
     ProofArray* proof_array = NULL;
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 3ef9578ef..08d1618c2 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -195,7 +195,8 @@ class TheoryArrays : public Theory {
   bool propagate(TNode literal);
 
   /** Explain why this literal is true by adding assumptions */
-  void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof *proof);
+  void explain(TNode literal, std::vector<TNode>& assumptions,
+               eq::EqProof* proof);
 
   /** For debugging only- checks invariants about when things are preregistered*/
   context::CDHashSet<Node, NodeHashFunction > d_isPreRegistered;
@@ -207,7 +208,7 @@ class TheoryArrays : public Theory {
 
   void preRegisterTerm(TNode n);
   void propagate(Effort e);
-  Node explain(TNode n, eq::EqProof *proof);
+  Node explain(TNode n, eq::EqProof* proof);
   Node explain(TNode n);
 
   /////////////////////////////////////////////////////////////////////////////
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 1378b4edf..a9142c4ef 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -926,8 +926,12 @@ std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const {
   return out.str();
 }
 
-void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& equalities, EqProof * eqp) const {
-  Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2 << ", " << (polarity ? "true" : "false") << ")" << ", proof = " << (eqp ? "ON" : "OFF") << std::endl;
+void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
+                                     std::vector<TNode>& equalities,
+                                     EqProof* eqp) const {
+  Debug("equality") << d_name << "::eq::explainEquality(" << t1 << ", " << t2
+                    << ", " << (polarity ? "true" : "false") << ")"
+                    << ", proof = " << (eqp ? "ON" : "OFF") << std::endl;
 
   // The terms must be there already
   Assert(hasTerm(t1) && hasTerm(t2));;
@@ -953,21 +957,21 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
     for (unsigned i = reasonRef.mergesStart; i < reasonRef.mergesEnd; ++ i) {
 
       EqualityPair toExplain = d_deducedDisequalityReasons[i];
-      EqProof* eqpc = NULL;
+      std::shared_ptr<EqProof> eqpc;
 
       // If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x.
       if (eqp && toExplain.first != toExplain.second) {
-        eqpc = new EqProof;
+        eqpc = std::make_shared<EqProof>();
       }
 
-      getExplanation(toExplain.first, toExplain.second, equalities, eqpc);
+      getExplanation(toExplain.first, toExplain.second, equalities, eqpc.get());
 
       if (eqpc) {
         Debug("pf::ee") << "Child proof is:" << std::endl;
         eqpc->debug_print("pf::ee", 1);
 
         if (eqpc->d_id == eq::MERGED_THROUGH_TRANS) {
-          std::vector<EqProof *> orderedChildren;
+          std::vector<std::shared_ptr<EqProof>> orderedChildren;
           bool nullCongruenceFound = false;
           for (unsigned i = 0; i < eqpc->d_children.size(); ++i) {
             if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE &&
@@ -1002,10 +1006,9 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
         eqp->d_id = MERGED_THROUGH_CONSTANTS;
       } else if (eqp->d_children.size() == 1) {
         // The transitivity proof has just one child. Simplify.
-        EqProof* temp = eqp->d_children[0];
+        std::shared_ptr<EqProof> temp = eqp->d_children[0];
         eqp->d_children.clear();
         *eqp = *temp;
-        delete temp;
       }
 
       Debug("pf::ee") << "Disequality explanation final proof: " << std::endl;
@@ -1014,16 +1017,21 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
   }
 }
 
-void EqualityEngine::explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp) const {
-  Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")" << std::endl;
+void EqualityEngine::explainPredicate(TNode p, bool polarity,
+                                      std::vector<TNode>& assertions,
+                                      EqProof* eqp) const {
+  Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")"
+                    << std::endl;
   // Must have the term
   Assert(hasTerm(p));
   // Get the explanation
-  getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions, eqp);
+  getExplanation(getNodeId(p), polarity ? d_trueId : d_falseId, assertions,
+                 eqp);
 }
 
-void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const {
-
+void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id,
+                                    std::vector<TNode>& equalities,
+                                    EqProof* eqp) const {
   Debug("equality") << d_name << "::eq::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl;
 
   // We can only explain the nodes that got merged
@@ -1094,7 +1102,7 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
           Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl;
 
-          std::vector<EqProof *> eqp_trans;
+          std::vector<std::shared_ptr<EqProof>> eqp_trans;
 
           // Reconstruct the path
           do {
@@ -1109,10 +1117,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             Debug("equality") << d_name << "                     in currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl;
             Debug("equality") << d_name << "                     reason type = " << reasonType << std::endl;
 
-            EqProof* eqpc = NULL;
+            std::shared_ptr<EqProof> eqpc;;
             // Make child proof if a proof is being constructed
             if (eqp) {
-              eqpc = new EqProof;
+              eqpc = std::make_shared<EqProof>();
               eqpc->d_id = reasonType;
             }
 
@@ -1126,11 +1134,13 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
               Debug("equality") << push;
               Debug("equality") << "Explaining left hand side equalities" << std::endl;
-              EqProof * eqpc1 = eqpc ? new EqProof : NULL;
-              getExplanation(f1.a, f2.a, equalities, eqpc1);
+              std::shared_ptr<EqProof> eqpc1 =
+                  eqpc ? std::make_shared<EqProof>() : nullptr;
+              getExplanation(f1.a, f2.a, equalities, eqpc1.get());
               Debug("equality") << "Explaining right hand side equalities" << std::endl;
-              EqProof * eqpc2 = eqpc ? new EqProof : NULL;
-              getExplanation(f1.b, f2.b, equalities, eqpc2);
+              std::shared_ptr<EqProof> eqpc2 =
+                  eqpc ? std::make_shared<EqProof>() : nullptr;
+              getExplanation(f1.b, f2.b, equalities, eqpc2.get());
               if( eqpc ){
                 eqpc->d_children.push_back( eqpc1 );
                 eqpc->d_children.push_back( eqpc2 );
@@ -1173,8 +1183,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
               // Explain why a = b constant
               Debug("equality") << push;
-              EqProof * eqpc1 = eqpc ? new EqProof : NULL;
-              getExplanation(eq.a, eq.b, equalities, eqpc1);
+              std::shared_ptr<EqProof> eqpc1 =
+                  eqpc ? std::make_shared<EqProof>() : nullptr;
+              getExplanation(eq.a, eq.b, equalities, eqpc1.get());
               if( eqpc ){
                 eqpc->d_children.push_back( eqpc1 );
               }
@@ -1198,8 +1209,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               for (unsigned i = 0; i < interpreted.getNumChildren(); ++ i) {
                 EqualityNodeId childId = getNodeId(interpreted[i]);
                 Assert(isConstant(childId));
-                EqProof * eqpcc = eqpc ? new EqProof : NULL;
-                getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc);
+                std::shared_ptr<EqProof> eqpcc =
+                    eqpc ? std::make_shared<EqProof>() : nullptr;
+                getExplanation(childId, getEqualityNode(childId).getFind(),
+                               equalities, eqpcc.get());
                 if( eqpc ) {
                   eqpc->d_children.push_back( eqpcc );
 
@@ -1223,8 +1236,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               if (eqpc) {
                 //apply proof reconstruction processing (when eqpc is non-null)
                 if (d_pathReconstructionTriggers.find(reasonType) != d_pathReconstructionTriggers.end()) {
-                  d_pathReconstructionTriggers.find(reasonType)->second->notify(reasonType, reason, a, b,
-                                                                                equalities, eqpc);
+                  d_pathReconstructionTriggers.find(reasonType)
+                      ->second->notify(reasonType, reason, a, b, equalities,
+                                       eqpc.get());
                 }
                 if (reasonType == MERGED_THROUGH_EQUALITY) {
                   eqpc->d_node = reason;
@@ -1255,9 +1269,8 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
             if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
               if(eqpc->d_node.isNull()) {
                 Assert(eqpc->d_children.size() == 1);
-                EqProof *p = eqpc;
+                std::shared_ptr<EqProof> p = eqpc;
                 eqpc = p->d_children[0];
-                delete p;
               } else {
                 Assert(eqpc->d_children.empty());
               }
@@ -1270,7 +1283,6 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
           if (eqp) {
             if(eqp_trans.size() == 1) {
               *eqp = *eqp_trans[0];
-              delete eqp_trans[0];
             } else {
               eqp->d_id = MERGED_THROUGH_TRANS;
               eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 9638b9f09..a89e55312 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -21,6 +21,7 @@
 
 #include <deque>
 #include <queue>
+#include <memory>
 #include <unordered_map>
 #include <vector>
 
@@ -150,7 +151,8 @@ public:
   virtual ~PathReconstructionNotify() {}
 
   virtual void notify(unsigned reasonType, Node reason, Node a, Node b,
-                      std::vector<TNode>& equalities, EqProof* proof) const = 0;
+                      std::vector<TNode>& equalities,
+                      EqProof* proof) const = 0;
 };
 
 /**
@@ -506,7 +508,7 @@ private:
    * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere
    * else.
    */
-  void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof * eqp) const;
+  void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqProof* eqp) const;
 
   /**
    * Print the equality graph.
@@ -794,14 +796,17 @@ public:
    * Returns the reasons (added when asserting) that imply it
    * in the assertions vector.
    */
-  void explainEquality(TNode t1, TNode t2, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const;
+  void explainEquality(TNode t1, TNode t2, bool polarity,
+                       std::vector<TNode>& assertions,
+                       EqProof* eqp = nullptr) const;
 
   /**
    * Get an explanation of the predicate being true or false.
    * Returns the reasons (added when asserting) that imply imply it
    * in the assertions vector.
    */
-  void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions, EqProof * eqp = NULL) const;
+  void explainPredicate(TNode p, bool polarity, std::vector<TNode>& assertions,
+                        EqProof* eqp = nullptr) const;
 
   /**
    * Add term to the set of trigger terms with a corresponding tag. The notify class will get
@@ -925,8 +930,9 @@ public:
   EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
   unsigned d_id;
   Node d_node;
-  std::vector< EqProof * > d_children;
-  void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const;
+  std::vector<std::shared_ptr<EqProof>> d_children;
+  void debug_print(const char* c, unsigned tb = 0,
+                   PrettyPrinter* prettyPrinter = nullptr) const;
 };/* class EqProof */
 
 } // Namespace eq
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index e8cc3b385..170621603 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -17,6 +17,8 @@
 
 #include "theory/uf/theory_uf.h"
 
+#include <memory>
+
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
@@ -629,8 +631,9 @@ void TheoryUF::computeCareGraph() {
 }/* TheoryUF::computeCareGraph() */
 
 void TheoryUF::conflict(TNode a, TNode b) {
-  eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
-  d_conflictNode = explain(a.eqNode(b),pf);
+  std::shared_ptr<eq::EqProof> pf =
+      d_proofsEnabled ? std::make_shared<eq::EqProof>() : nullptr;
+  d_conflictNode = explain(a.eqNode(b), pf.get());
   ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
   d_out->conflict(d_conflictNode, puf);
   d_conflict = true;