New Resolver Design for Decompose Order

diff --git a/src/ASTAnalyses/Order/orderanalysis.cc b/src/ASTAnalyses/Order/orderanalysis.cc
index abec0c05a34eefbe191827e72852a0a62445b3db..c8c7e36d67a4e7bde00aab324b51b539770ac01b 100644 (file)
--- a/src/ASTAnalyses/Order/orderanalysis.cc
+++ b/src/ASTAnalyses/Order/orderanalysis.cc
@@ -39,6 +39,8 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                        SetIteratorOrderNode *srciterator = sources->iterator();
                        while (srciterator->hasNext()) {
                                OrderNode *srcnode = srciterator->next();
+                               if (srcnode->removed)
+                                       continue;
                                OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
                                newedge->mustPos = true;
                                newedge->polPos = true;

diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc
index d518b1ba12cb9d1c183091d0432d49a4f67d1005..85a020789be949c0fca91c23d835a7f0cb55bcdb 100644 (file)
--- a/src/ASTAnalyses/Order/ordergraph.cc
+++ b/src/ASTAnalyses/Order/ordergraph.cc
@@ -12,7 +12,6 @@ OrderGraph::OrderGraph(Order *_order) :
 OrderGraph *buildOrderGraph(Order *order) {
        ASSERT(order->graph == NULL);
        OrderGraph *orderGraph = new OrderGraph(order);
-       order->graph = orderGraph;
        uint constrSize = order->constraints.getSize();
        for (uint j = 0; j < constrSize; j++) {
                orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
@@ -124,7 +123,6 @@ OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
                node = tmp;
        } else {
                nodes.add(node);
-               allNodes.push(node);
        }
        return node;
 }
@@ -172,16 +170,8 @@ void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 }
 
 OrderGraph::~OrderGraph() {
-       uint size=allNodes.getSize();
-       for(uint i=0;i<size;i++)
-               delete allNodes.get(i);
-
-       SetIteratorOrderEdge *eiterator = edges.iterator();
-       while (eiterator->hasNext()) {
-               OrderEdge *edge = eiterator->next();
-               delete edge;
-       }
-       delete eiterator;
+       nodes.resetAndDelete();
+       edges.resetAndDelete();
 }
 
 bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
@@ -236,7 +226,7 @@ void OrderGraph::DFS(Vector<OrderNode *> *finishNodes) {
        SetIteratorOrderNode *iterator = getNodes();
        while (iterator->hasNext()) {
                OrderNode *node = iterator->next();
-               if (node->status == NOTVISITED) {
+               if (node->status == NOTVISITED && !node->removed) {
                        node->status = VISITED;
                        DFSNodeVisit(node, finishNodes, false, false, 0);
                        node->status = FINISHED;
@@ -250,7 +240,7 @@ void OrderGraph::DFSMust(Vector<OrderNode *> *finishNodes) {
        SetIteratorOrderNode *iterator = getNodes();
        while (iterator->hasNext()) {
                OrderNode *node = iterator->next();
-               if (node->status == NOTVISITED) {
+               if (node->status == NOTVISITED && !node->removed) {
                        node->status = VISITED;
                        DFSNodeVisit(node, finishNodes, false, true, 0);
                        node->status = FINISHED;

diff --git a/src/ASTAnalyses/Order/ordergraph.h b/src/ASTAnalyses/Order/ordergraph.h
index fc829668787cd5e94a89f05bf9b79cc8484eb281..e7e958ee63311917bea1f29f569fb1a8bca39937 100644 (file)
--- a/src/ASTAnalyses/Order/ordergraph.h
+++ b/src/ASTAnalyses/Order/ordergraph.h
@@ -35,12 +35,10 @@ public:
        void computeStronglyConnectedComponentGraph();
        void resetNodeInfoStatusSCC();
        void completePartialOrderGraph();
-       void removeNode(OrderNode *node) {nodes.remove(node);}
        
        CMEMALLOC;
 private:
        HashsetOrderNode nodes;
-       Vector<OrderNode *> allNodes;
        HashsetOrderEdge edges;
        Order *order;
        void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum);

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 01a667d9eb0c32c83432e9eae083c4a275911698..4c95db88c3196cf0db0559422affd7d01fd26c07 100644 (file)
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -81,7 +81,7 @@ void DecomposeOrderTransform::doTransform() {
 }
 
 
-void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) {
+void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) {
        Vector<Order *> partialcandidatevec;
        uint size = currOrder->constraints.getSize();
        for (uint i = 0; i < size; i++) {
@@ -203,18 +203,21 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
                OrderNode *srcNode = inEdge->source;
                srcNode->outEdges.remove(inEdge);
                edgesRemoved->add(inEdge);
+               bool removeOutgoingEdges = !iterin->hasNext();
+
                SetIteratorOrderEdge *iterout = node->outEdges.iterator();
                while (iterout->hasNext()) {
                        OrderEdge *outEdge = iterout->next();
                        OrderNode *sinkNode = outEdge->sink;
-                       sinkNode->inEdges.remove(outEdge);
-                       edgesRemoved->add(outEdge);
+                       if (removeOutgoingEdges) {
+                               sinkNode->inEdges.remove(outEdge);
+                               edgesRemoved->add(outEdge);
+                       }
                        //Adding new edge to new sink and src nodes ...
                        if (srcNode == sinkNode) {
                                solver->setUnSAT();
                                delete iterout;
                                delete iterin;
-                               graph->removeNode(node);
                                return;
                        }
                        //Add new order constraint
@@ -233,7 +236,6 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode
                delete iterout;
        }
        delete iterin;
-       graph->removeNode(node);
 }
 
 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {

diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
index 148235adf1f67dc971ab255f626a6a4782ae3aad..74d5eba90d3251903c200335cbfb9908cdcb7819 100644 (file)
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -16,7 +16,6 @@ int main(int numargs, char **argv) {
 
        solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b1, solver->applyLogicalOperation(SATC_NOT, b2)));
        solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b2, solver->applyLogicalOperation(SATC_NOT, b1)));
-       solver->serialize();
        if (solver->solve() == 1) {
                printf("SAT\n");
                printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",

diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
index 0e652d8d6e813169979e2a10fdb7a6479e754f7e..c2e9db45dc0ccb4ff8d9fe4aa1eb605873e958d8 100644 (file)
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -79,6 +79,8 @@ void DecomposeOrderResolver::buildGraph() {
                        bool isEdge = suborder->encoding.resolver->resolveOrder(doredge->newfirst, doredge->newsecond);
                        if (isEdge)
                                graph->addEdge(doredge->origfirst, doredge->origsecond);
+                       else if (order->type == SATC_TOTAL)
+                               graph->addEdge(doredge->origsecond, doredge->origfirst);
                }
        }
        delete iterator;
@@ -92,9 +94,15 @@ bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
                buildGraph();
 
        OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
-       ASSERT(from != NULL);
+       if (from == NULL) {
+               ASSERT(order->type != SATC_TOTAL);
+               return false;
+       }
        OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
-       ASSERT(to != NULL);
+       if (to == NULL) {
+               ASSERT(order->type != SATC_TOTAL);
+               return false;
+       }
        switch (order->type) {
        case SATC_TOTAL:
                return from->sccNum < to->sccNum;