Finish order decompose function

diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index f140fac7937055a92790ebdfef3594fc6a0a0cb9..97a3fff18c9286642b7ae325467a7b4dbc4f9dbd 100644 (file)
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -16,6 +16,7 @@
        type lastVector ## name(Vector ## name * vector);                      \
        void popVector ## name(Vector ## name * vector);                       \
        type getVector ## name(Vector ## name * vector, uint index);           \
+       void setExpandVector ## name(Vector ## name * vector, uint index, type item);   \
        void setVector ## name(Vector ## name * vector, uint index, type item); \
        uint getSizeVector ## name(Vector ## name * vector);                   \
        void setSizeVector ## name(Vector ## name * vector, uint size);        \
@@ -72,6 +73,11 @@
        type getVector ## name(Vector ## name * vector, uint index) {         \
                return vector->array[index];                                        \
        }                                                                     \
+       void setExpandVector ## name(Vector ## name * vector, uint index, type item) { \
+               if (index>=vector->size)                                                                                                                                                                                \
+                       setSizeVector ## name(vector, index + 1);                                                                                                       \
+               setVector ## name(vector, index, item);                                                                                                                 \
+       }                                                                                                                                                                                                                                                                                       \
        void setVector ## name(Vector ## name * vector, uint index, type item) { \
                vector->array[index] = item;                                          \
        }                                                                     \

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index 103b96204bbabefabcf6a4dda160fd5711ca93ca..0988abcc7e4e559e3ef4c63998e0b93431ebae17 100644 (file)
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -6,6 +6,7 @@
 #include "order.h"
 #include "ordernode.h"
 #include "rewriter.h"
+#include "mutableset.h"
 
 OrderGraph *buildOrderGraph(Order *order) {
        OrderGraph *orderGraph = allocOrderGraph(order);
@@ -264,7 +265,9 @@ void localMustAnalysisPartial(OrderGraph *graph) {
        deleteIterOrderEdge(iterator);
 }
 
-void decomposeOrder(Order *order, OrderGraph *graph) {
+void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
+       VectorOrder ordervec;
+       initDefVectorOrder(&ordervec);
        uint size = getSizeVectorBooleanOrder(&order->constraints);
        for (uint i = 0; i < size; i++) {
                BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
@@ -279,9 +282,28 @@ void decomposeOrder(Order *order, OrderGraph *graph) {
                        replaceBooleanWithFalse((Boolean *)orderconstraint);
                } else {
                        //Build new order and change constraint's order
-
+                       Order * neworder = NULL;
+                       if (getSizeVectorOrder(&ordervec) > from->sccNum)
+                               neworder = getVectorOrder(&ordervec, from->sccNum);
+                       if (neworder == NULL) {
+                               Set * set = (Set *) allocMutableSet(order->set->type);
+                               neworder = allocOrder(order->type, set);
+                               pushVectorOrder(This->allOrders, neworder);
+                               setExpandVectorOrder(&ordervec, from->sccNum, neworder);
+                       }
+                       if (from->status != ADDEDTOSET) {
+                               from->status = ADDEDTOSET;
+                               addElementMSet((MutableSet *)neworder->set, from->id);
+                       }
+                       if (to->status != ADDEDTOSET) {
+                               to->status = ADDEDTOSET;
+                               addElementMSet((MutableSet *)neworder->set, to->id);
+                       }
+                       orderconstraint->order = neworder;
+                       addOrderConstraint(neworder, orderconstraint);
                }
        }
+       deleteVectorArrayOrder(&ordervec);
 }
 
 void orderAnalysis(CSolver *This) {
@@ -312,7 +334,7 @@ void orderAnalysis(CSolver *This) {
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
 
-               decomposeOrder(order, graph);
+               decomposeOrder(This, order, graph);
 
                deleteOrderGraph(graph);
        }

diff --git a/src/Encoders/orderencoder.h b/src/Encoders/orderencoder.h
index c48a0f7d3e6e50e841ab4ce596d986f7c0077a6e..ae63cd682b7c9a4edd4d31059ff9fa272517254d 100644 (file)
--- a/src/Encoders/orderencoder.h
+++ b/src/Encoders/orderencoder.h
@@ -30,7 +30,7 @@ void reachMustAnalysis(OrderGraph *graph);
 void localMustAnalysisTotal(OrderGraph *graph);
 void localMustAnalysisPartial(OrderGraph *graph);
 void orderAnalysis(CSolver *This);
-void decomposeOrder(Order *order, OrderGraph *graph);
+void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
 
 #endif/* ORDERGRAPHBUILDER_H */
 

diff --git a/src/Encoders/ordernode.h b/src/Encoders/ordernode.h
index a6eb4db84145251a863ddf21a237bb3225db5a1d..81e199348435cdc34534df69dba6223d3a22be51 100644 (file)
--- a/src/Encoders/ordernode.h
+++ b/src/Encoders/ordernode.h
@@ -14,7 +14,7 @@
 #include "structs.h"
 #include "orderedge.h"
 
-enum NodeStatus {NOTVISITED, VISITED, FINISHED};
+enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET};
 typedef enum NodeStatus NodeStatus;
 
 struct OrderNode {