removing true nodes from the OrderGraph

[satune.git] / src / Encoders / orderencoder.c

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index 066695ca0b9dfbeb9d67ec080efd8cc0865b9d69..32bd91092f16699200675b02911399527a2e6524 100644 (file)
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -82,8 +82,58 @@ void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
        deleteVectorArrayOrderNode(&finishNodes);
 }
 
-void removeMustBeTrueNodes(OrderGraph *graph) {
-       //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
+bool isMustBeTrueNode(OrderNode* node){
+       HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->inEdges);
+       while(hasNextOrderEdge(iterator)){
+               OrderEdge* edge = nextOrderEdge(iterator);
+               if(!edge->mustPos)
+                       return false;
+       }
+       deleteIterOrderEdge(iterator);
+       iterator = iteratorOrderEdge(node->outEdges);
+       while(hasNextOrderEdge(iterator)){
+               OrderEdge* edge = nextOrderEdge(iterator);
+               if(!edge->mustPos)
+                       return false;
+       }
+       deleteIterOrderEdge(iterator);
+       return true;
+}
+
+void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){
+       HSIteratorOrderEdge* iterin = iteratorOrderEdge(node->inEdges);
+       while(hasNextOrderEdge(iterin)){
+               OrderEdge* inEdge = nextOrderEdge(iterin);
+               OrderNode* srcNode = inEdge->source;
+               removeHashSetOrderEdge(srcNode->outEdges, inEdge);
+               HSIteratorOrderEdge* iterout = iteratorOrderEdge(node->outEdges);
+               while(hasNextOrderEdge(iterout)){
+                       OrderEdge* outEdge = nextOrderEdge(iterout);
+                       OrderNode* sinkNode = outEdge->sink;
+                       removeHashSetOrderEdge(sinkNode->inEdges, outEdge);
+                       //Adding new edge to new sink and src nodes ...
+                       OrderEdge *newEdge =getOrderEdgeFromOrderGraph(graph, srcNode, sinkNode);
+                       newEdge->mustPos = true;
+                       newEdge->polPos = true;
+                       if (newEdge->mustNeg)
+                               This->unsat = true;
+                       addHashSetOrderEdge(srcNode->outEdges, newEdge);
+                       addHashSetOrderEdge(sinkNode->inEdges, newEdge);
+               }
+               deleteIterOrderEdge(iterout);
+       }
+       deleteIterOrderEdge(iterin);
+}
+
+void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
+       HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
+       while(hasNextOrderNode(iterator)){
+               OrderNode* node = nextOrderNode(iterator);
+               if(isMustBeTrueNode(node)){
+                       bypassMustBeTrueNode(This,graph, node);
+               }
+       }
+       deleteIterOrderNode(iterator);
 }
 
 /** This function computes a source set for every nodes, the set of
@@ -160,6 +210,7 @@ void completePartialOrderGraph(OrderGraph *graph) {
        }
 
        resetAndDeleteHashTableNodeToNodeSet(table);
+       deleteHashTableNodeToNodeSet(table);
        resetNodeInfoStatusSCC(graph);
        deleteVectorArrayOrderNode(&sccNodes);
        deleteVectorArrayOrderNode(&finishNodes);
@@ -250,6 +301,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode
        }
 
        resetAndDeleteHashTableNodeToNodeSet(table);
+       deleteHashTableNodeToNodeSet(table);
 }
 
 /* This function finds edges that would form a cycle with must edges
@@ -327,12 +379,15 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
 
 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
        VectorOrder ordervec;
+       VectorOrder partialcandidatevec;
        initDefVectorOrder(&ordervec);
+       initDefVectorOrder(&partialcandidatevec);
        uint size = getSizeVectorBooleanOrder(&order->constraints);
        for (uint i = 0; i < size; i++) {
                BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
                OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
                OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
+               model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
                if (from->sccNum != to->sccNum) {
                        OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);                  
                        if (edge->polPos) {
@@ -353,6 +408,10 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                                neworder = allocOrder(order->type, set);
                                pushVectorOrder(This->allOrders, neworder);
                                setExpandVectorOrder(&ordervec, from->sccNum, neworder);
+                               if (order->type == PARTIAL)
+                                       setExpandVectorOrder(&partialcandidatevec, from->sccNum, neworder);
+                               else
+                                       setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
                        }
                        if (from->status != ADDEDTOSET) {
                                from->status = ADDEDTOSET;
@@ -362,11 +421,27 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                                to->status = ADDEDTOSET;
                                addElementMSet((MutableSet *)neworder->set, to->id);
                        }
+                       if (order->type == PARTIAL) {
+                               OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
+                               if (edge->polNeg)
+                                       setExpandVectorOrder(&partialcandidatevec, from->sccNum, NULL);
+                       }
                        orderconstraint->order = neworder;
                        addOrderConstraint(neworder, orderconstraint);
                }
        }
+
+       uint pcvsize=getSizeVectorOrder(&partialcandidatevec);
+       for(uint i=0;i<pcvsize;i++) {
+               Order * neworder=getVectorOrder(&partialcandidatevec, i);
+               if (neworder != NULL){
+                       neworder->type = TOTAL;
+                       model_print("i=%u\t", i);
+               }
+       }
+       
        deleteVectorArrayOrder(&ordervec);
+       deleteVectorArrayOrder(&partialcandidatevec);
 }
 
 void orderAnalysis(CSolver *This) {
@@ -405,7 +480,7 @@ void orderAnalysis(CSolver *This) {
                bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
                
                if (mustReachPrune)
-                       removeMustBeTrueNodes(graph);
+                       removeMustBeTrueNodes(This, graph);
                
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);