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 a77a1a8418b086dd143c3e549034dde836d62988..13e26c07eca66a0cfa32c20b115340e0bbf07085 100644 (file)
--- a/src/ASTAnalyses/Order/orderanalysis.cc
+++ b/src/ASTAnalyses/Order/orderanalysis.cc
@@ -1,3 +1,5 @@
+#include <stdint.h>
+
 #include "orderanalysis.h"
 #include "structs.h"
 #include "csolver.h"
@@ -46,17 +48,17 @@ 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;
-
                if (child->status == NOTVISITED) {
                        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;
                }
@@ -80,70 +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,15 +236,16 @@ 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();
+                                       }
                                }
                        }
                        delete iterator;
                }
        }
 
-       table->resetanddelete();
+       table->resetAndDeleteVals();
        delete table;
 }
 
@@ -337,9 +277,8 @@ void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
                        if (invEdge != NULL) {
                                if (!invEdge->mustPos) {
                                        invEdge->polPos = false;
-                               } else {
+                               } else
                                        solver->setUnSAT();
-                               }
                                invEdge->mustNeg = true;
                                invEdge->polNeg = true;
                        }
@@ -360,16 +299,15 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
                if (edge->mustPos) {
                        if (!edge->mustNeg) {
                                edge->polNeg = false;
-                       } else
+                       } else {
                                solver->setUnSAT();
-
+                       }
                        OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
                        if (invEdge != NULL) {
                                if (!invEdge->mustPos)
                                        invEdge->polPos = false;
                                else
                                        solver->setUnSAT();
-
                                invEdge->mustNeg = true;
                                invEdge->polNeg = true;
                        }