Switching EqProof to use shared_ptr everywhere. (#1217)

This clarifies the memory ownership of EqProofs.

1 files changed, 41 insertions, 29 deletions

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