Fix some memory leaks

[satune.git] / src / ASTAnalyses / Order / orderanalysis.cc

diff --git a/src/ASTAnalyses/Order/orderanalysis.cc b/src/ASTAnalyses/Order/orderanalysis.cc
index ae3c7525b57f900d97c6d3e1577a7cc28c3ae12f..13e26c07eca66a0cfa32c20b115340e0bbf07085 100644 (file)
--- a/src/ASTAnalyses/Order/orderanalysis.cc
+++ b/src/ASTAnalyses/Order/orderanalysis.cc
@@ -48,7 +48,7 @@ void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReve
                        if (!edge->mustPos)
                                continue;
                } else
-               if (!edge->polPos && !edge->pseudoPos)  //Ignore edges that do not have positive polarity
+               if (!edge->polPos && !edge->pseudoPos)          //Ignore edges that do not have positive polarity
                        continue;
 
                OrderNode *child = isReverse ? edge->source : edge->sink;
@@ -56,8 +56,9 @@ void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReve
                        child->status = VISITED;
                        DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
                        child->status = FINISHED;
-                       if (finishNodes != NULL)
+                       if (finishNodes != NULL) {
                                finishNodes->push(child);
+                       }
                        if (isReverse)
                                child->sccNum = sccNum;
                }
@@ -81,69 +82,7 @@ void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
        resetNodeInfoStatusSCC(graph);
 }
 
-bool isMustBeTrueNode(OrderNode *node) {
-       SetIteratorOrderEdge *iterator = node->inEdges.iterator();
-       while (iterator->hasNext()) {
-               OrderEdge *edge = iterator->next();
-               if (!edge->mustPos) {
-                       delete iterator;
-                       return false;
-               }
-       }
-       delete iterator;
-       iterator = node->outEdges.iterator();
-       while (iterator->hasNext()) {
-               OrderEdge *edge = iterator->next();
-               if (!edge->mustPos) {
-                       delete iterator;
-                       return false;
-               }
-       }
-       delete iterator;
-       return true;
-}
-
-void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
-       SetIteratorOrderEdge *iterin = node->inEdges.iterator();
-       while (iterin->hasNext()) {
-               OrderEdge *inEdge = iterin->next();
-               OrderNode *srcNode = inEdge->source;
-               srcNode->outEdges.remove(inEdge);
-               SetIteratorOrderEdge *iterout = node->outEdges.iterator();
-               while (iterout->hasNext()) {
-                       OrderEdge *outEdge = iterout->next();
-                       OrderNode *sinkNode = outEdge->sink;
-                       sinkNode->inEdges.remove(outEdge);
-                       //Adding new edge to new sink and src nodes ...
-                       if(srcNode == sinkNode) {
-                               This->setUnSAT();
-                               delete iterout;
-                               delete iterin;
-                               return;
-                       }
-                       OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
-                       newEdge->mustPos = true;
-                       newEdge->polPos = true;
-                       if (newEdge->mustNeg)
-                               This->setUnSAT();
-                       srcNode->outEdges.add(newEdge);
-                       sinkNode->inEdges.add(newEdge);
-               }
-               delete iterout;
-       }
-       delete iterin;
-}
 
-void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
-       SetIteratorOrderNode *iterator = graph->getNodes();
-       while (iterator->hasNext()) {
-               OrderNode *node = iterator->next();
-               if (isMustBeTrueNode(node)) {
-                       bypassMustBeTrueNode(This, graph, node);
-               }
-       }
-       delete iterator;
-}
 
 /** This function computes a source set for every nodes, the set of
     nodes that can reach that node via pospolarity edges.  It then
@@ -216,7 +155,7 @@ void completePartialOrderGraph(OrderGraph *graph) {
                }
        }
 
-       table->resetanddelete();
+       table->resetAndDeleteVals();
        delete table;
        resetNodeInfoStatusSCC(graph);
 }
@@ -297,7 +236,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                                if (!edge->mustNeg && sources->contains(child)) {
                                        edge->mustNeg = true;
                                        edge->polNeg = true;
-                                       if (edge->mustPos){
+                                       if (edge->mustPos) {
                                                solver->setUnSAT();
                                        }
                                }
@@ -306,7 +245,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                }
        }
 
-       table->resetanddelete();
+       table->resetAndDeleteVals();
        delete table;
 }