Give vector more specific type

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 591bfe61ac0a8de6a56c6ef2b6943914f3675349..3ce75e4ad432bc071ebca41adde714877c99656c 100644 (file)
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -23,7 +23,7 @@ Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) {
        This->order=order;
        This->first=first;
        This->second=second;
-       pushVectorBoolean(&order->constraints, &This->base);
+       pushVectorBooleanOrder(&order->constraints, This);
        initDefVectorBoolean(GETBOOLEANPARENTS(This));
        return & This -> base;
 }

diff --git a/src/AST/order.c b/src/AST/order.c
index 92c52ae64069a575a64d538284333fa924fd4c9c..054de91ce833b9247a9b6fab80f74fcd2469dbaf 100644 (file)
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -6,7 +6,7 @@
 Order* allocOrder(OrderType type, Set * set){
        Order* This = (Order*)ourmalloc(sizeof(Order));
        This->set=set;
-       initDefVectorBoolean(& This->constraints);
+       initDefVectorBooleanOrder(& This->constraints);
        This->type=type;
        initOrderEncoding(& This->order, This);
        This->orderPairTable = NULL;
@@ -18,7 +18,7 @@ void initializeOrderHashTable(Order* This){
 }
 
 void addOrderConstraint(Order* This, BooleanOrder* constraint){
-       pushVectorBoolean( &This->constraints, (Boolean*) constraint);
+       pushVectorBooleanOrder( &This->constraints, constraint);
 }
 
 void setOrderEncodingType(Order* This, OrderEncodingType type){
@@ -26,7 +26,7 @@ void setOrderEncodingType(Order* This, OrderEncodingType type){
 }
 
 void deleteOrder(Order* This){
-       deleteVectorArrayBoolean(& This->constraints);
+       deleteVectorArrayBooleanOrder(& This->constraints);
        deleteOrderEncoding(& This->order);
        if(This->orderPairTable != NULL) {
                resetAndDeleteHashTableOrderPair(This->orderPairTable);

diff --git a/src/AST/order.h b/src/AST/order.h
index bb35603069b3bb857da0a46223cb24d7e890baa0..7a173b90f2bf73c26b106792683ac6641be0b8e9 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -11,7 +11,7 @@ struct Order {
        OrderType type;
        Set * set;
        HashTableOrderPair * orderPairTable;
-       VectorBoolean constraints;
+       VectorBooleanOrder constraints;
        OrderEncoding order;
 };
 

diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index 9c44ea7a66ffc43f7dbd2352e9a4be2d8ee13be5..459edd1498d6fe2416b957e5c894686893a0dc33 100644 (file)
--- a/src/Collections/structs.c
+++ b/src/Collections/structs.c
@@ -9,6 +9,7 @@
 VectorImpl(Table, Table *, 4);
 VectorImpl(Set, Set *, 4);
 VectorImpl(Boolean, Boolean *, 4);
+VectorImpl(BooleanOrder, BooleanOrder *, 4);
 VectorImpl(Function, Function *, 4);
 VectorImpl(Predicate, Predicate *, 4);
 VectorImpl(Element, Element *, 4);

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index 4343d34302178b2e45bd183f456f6f40d1984393..5713e89178749aeabfb5232ce54a0dcd093a520e 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -13,6 +13,7 @@ ArrayDef(Set, Set *);
 VectorDef(Table, Table *);
 VectorDef(Set, Set *);
 VectorDef(Boolean, Boolean *);
+VectorDef(BooleanOrder, BooleanOrder *);
 VectorDef(Function, Function *);
 VectorDef(Predicate, Predicate *);
 VectorDef(Element, Element *);

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index b87a982da0820f203b91c3ed6ff585a7872a29af..d15592132c65b3d3d59528b92a3a80f7c9bd003e 100644 (file)
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -9,9 +9,9 @@
 
 OrderGraph* buildOrderGraph(Order *order) {
        OrderGraph* orderGraph = allocOrderGraph(order);
-       uint constrSize = getSizeVectorBoolean(&order->constraints);
+       uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
        for(uint j=0; j<constrSize; j++){
-               addOrderConstraintToOrderGraph(orderGraph, getVectorBoolean(&order->constraints, j));
+               addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
        }
        return orderGraph;
 }
@@ -22,7 +22,7 @@ void DFS(OrderGraph* graph, VectorOrderNode* finishNodes) {
                OrderNode* node = nextOrderNode(iterator);
                if(node->status == NOTVISITED){
                        node->status = VISITED;
-                       DFSNodeVisit(node, finishNodes, false);
+                       DFSNodeVisit(node, finishNodes, false, 0);
                        node->status = FINISHED;
                        pushVectorOrderNode(finishNodes, node);
                }
@@ -32,18 +32,20 @@ void DFS(OrderGraph* graph, VectorOrderNode* finishNodes) {
 
 void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes) {
        uint size = getSizeVectorOrderNode(finishNodes);
+       uint sccNum=1;
        for(int i=size-1; i>=0; i--){
                OrderNode* node = getVectorOrderNode(finishNodes, i);
                if(node->status == NOTVISITED){
                        node->status = VISITED;
-                       DFSNodeVisit(node, NULL, true);
+                       DFSNodeVisit(node, NULL, true, sccNum);
+                       node->sccNum = sccNum;
                        node->status = FINISHED;
-                       pushVectorOrderNode(&graph->scc, node); 
+                       sccNum++;
                }
        }
 }
 
-void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool isReverse) {
+void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool isReverse, uint sccNum) {
        HSIteratorOrderEdge* iterator = isReverse?iteratorOrderEdge(node->inEdges):iteratorOrderEdge(node->outEdges);
        while(hasNextOrderEdge(iterator)){
                OrderEdge* edge = nextOrderEdge(iterator);
@@ -52,12 +54,14 @@ void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool isReverse)
                
                OrderNode* child = isReverse? edge->source: edge->sink;
 
-               if(child->status == NOTVISITED){
+               if(child->status == NOTVISITED) {
                        child->status = VISITED;
-                       DFSNodeVisit(child, finishNodes, isReverse);
+                       DFSNodeVisit(child, finishNodes, isReverse, sccNum);
                        child->status = FINISHED;
                        if(!isReverse)
                                pushVectorOrderNode(finishNodes, child); 
+                       else
+                               child->sccNum = sccNum;
                }
        }
        deleteIterOrderEdge(iterator);
@@ -246,6 +250,12 @@ void localMustAnalysisPartial(OrderGraph *graph) {
        deleteIterOrderEdge(iterator);
 }
 
+void decomposeOrder(Order *order, OrderGraph *graph) {
+       uint size=getSizeVectorBooleanOrder(&order->constraints);
+       for(uint i=0;i<size;i++) {
+       }
+}
+
 void orderAnalysis(CSolver* This) {
        uint size = getSizeVectorOrder(This->allOrders);
        for(uint i=0; i<size; i++){
@@ -268,10 +278,14 @@ void orderAnalysis(CSolver* This) {
                        localMustAnalysisTotal(graph);
                }
 
-               //This analysis is completely optional
+               //This optimization is completely optional
                removeMustBeTrueNodes(graph);
 
+               //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
+
+               decomposeOrder(order, graph);
+                       
                deleteOrderGraph(graph);
        }
 }

diff --git a/src/Encoders/orderencoder.h b/src/Encoders/orderencoder.h
index ca3e415c0c687660beaf5c86e536d97e8c8f555f..e25ee42994973bb46b6ec8f9f1e38b974ec62185 100644 (file)
--- a/src/Encoders/orderencoder.h
+++ b/src/Encoders/orderencoder.h
@@ -15,7 +15,7 @@ OrderGraph* buildOrderGraph(Order *order);
 void computeStronglyConnectedComponentGraph(OrderGraph* graph);
 void orderAnalysis(CSolver* solver);
 void initializeNodeInfoSCC(OrderGraph* graph);
-void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool isReverse);
+void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, bool isReverse, uint sccNum);
 void DFS(OrderGraph* graph, VectorOrderNode* finishNodes);
 void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes);
 void completePartialOrderGraph(OrderGraph* graph);
@@ -30,6 +30,7 @@ void reachMustAnalysis(OrderGraph *graph);
 void localMustAnalysisTotal(OrderGraph *graph);
 void localMustAnalysisPartial(OrderGraph *graph);
 void orderAnalysis(CSolver* This);
+void decomposeOrder(Order *order, OrderGraph *graph);
 
 #endif /* ORDERGRAPHBUILDER_H */
 

diff --git a/src/Encoders/ordergraph.c b/src/Encoders/ordergraph.c
index 2510fab7a15c29744ff2d0f6ada155159387b77e..e6cb64e1ba3016dc3a4bd7ffd4ec5ca3a258fd39 100644 (file)
--- a/src/Encoders/ordergraph.c
+++ b/src/Encoders/ordergraph.c
@@ -9,13 +9,12 @@ OrderGraph* allocOrderGraph(Order *order) {
        OrderGraph* This = (OrderGraph*) ourmalloc(sizeof(OrderGraph));
        This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
        This->order = order;
-       initDefVectorOrderNode(&This->scc);
        return This;
 }
 
-void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean* constr) {
-       Polarity polarity=constr->polarity;
-       BooleanValue mustval=constr->boolVal;
+void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, BooleanOrder* constr) {
+       Polarity polarity=constr->base.polarity;
+       BooleanValue mustval=constr->base.boolVal;
        Order* order=graph->order;
        switch(polarity) {
        case P_BOTHTRUEFALSE:
@@ -26,7 +25,7 @@ void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean
                _1to2->polPos = true;
                addNewOutgoingEdge(node1, _1to2);
                addNewIncomingEdge(node2, _1to2);
-               if(constr->polarity == P_TRUE)
+               if(constr->base.polarity == P_TRUE)
                        break;
        }
        case P_FALSE:{
@@ -83,11 +82,10 @@ OrderEdge* getInverseOrderEdge(OrderGraph* graph, OrderEdge *edge) {
        return tmp;
 }
 
-void addOrderConstraintToOrderGraph(OrderGraph* graph, Boolean* constr) {
-       BooleanOrder* bOrder = (BooleanOrder*) constr;
+void addOrderConstraintToOrderGraph(OrderGraph* graph, BooleanOrder* bOrder) {
        OrderNode* from = getOrderNodeFromOrderGraph(graph, bOrder->first);
        OrderNode* to = getOrderNodeFromOrderGraph(graph, bOrder->second);
-       addOrderEdge(graph, from, to, constr);
+       addOrderEdge(graph, from, to, bOrder);
 }
 
 void deleteOrderGraph(OrderGraph* graph){

diff --git a/src/Encoders/ordergraph.h b/src/Encoders/ordergraph.h
index 1848d2e7c197c6fc941b31c56d745b75ec6cbdf8..a30c9f94d302981874987d95a061e572202173ca 100644 (file)
--- a/src/Encoders/ordergraph.h
+++ b/src/Encoders/ordergraph.h
@@ -15,14 +15,13 @@ struct OrderGraph {
        HashSetOrderNode* nodes;
        HashSetOrderEdge* edges;
        Order* order;
-       VectorOrderNode scc;
 };
 
 OrderGraph* allocOrderGraph(Order *order);
-void addOrderConstraintToOrderGraph(OrderGraph* graph, Boolean* constr);
+void addOrderConstraintToOrderGraph(OrderGraph* graph, BooleanOrder* bOrder);
 OrderNode* getOrderNodeFromOrderGraph(OrderGraph* graph, uint64_t id);
 OrderEdge* getOrderEdgeFromOrderGraph(OrderGraph* graph, OrderNode* begin, OrderNode* end);
-void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean* constr);
+void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, BooleanOrder* constr);
 void deleteOrderGraph(OrderGraph* graph);
 OrderEdge* getInverseOrderEdge(OrderGraph* graph, OrderEdge *edge);
 #endif /* ORDERGRAPH_H */

diff --git a/src/Encoders/ordernode.c b/src/Encoders/ordernode.c
index 9f86b2be00ba36a5f15f448cb7c6d8d7bf1ce6d3..072e54c150a6b56fd284b7d64758807a2a5a4ff4 100644 (file)
--- a/src/Encoders/ordernode.c
+++ b/src/Encoders/ordernode.c
@@ -7,6 +7,7 @@ OrderNode* allocOrderNode(uint64_t id) {
        This->inEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
        This->outEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
        This->status=NOTVISITED;
+       This->sccNum=0;
        return This;
 }
 

diff --git a/src/Encoders/ordernode.h b/src/Encoders/ordernode.h
index 2e2ce9d4df3419acab89f8375d06ed62dc2db1c4..359b5bfee8f934f30eb6caf52866cfa8a9231fd0 100644 (file)
--- a/src/Encoders/ordernode.h
+++ b/src/Encoders/ordernode.h
@@ -22,6 +22,7 @@ struct OrderNode {
        HashSetOrderEdge* inEdges;
        HashSetOrderEdge* outEdges;
        NodeStatus status;
+       uint sccNum;
 };
 
 OrderNode* allocOrderNode(uint64_t id);