From 8762646584718c6bc1988e8aabb38924f6d56952 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 16 Aug 2017 21:50:06 -0700
Subject: [PATCH] Finish order decompose function

---
 src/Collections/vector.h    |  6 ++++++
 src/Encoders/orderencoder.c | 28 +++++++++++++++++++++++++---
 src/Encoders/orderencoder.h |  2 +-
 src/Encoders/ordernode.h    |  2 +-
 4 files changed, 33 insertions(+), 5 deletions(-)

diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index f140fac..97a3fff 100644
--- 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 103b962..0988abc 100644
--- 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 c48a0f7..ae63cd6 100644
--- 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 a6eb4db..81e1993 100644
--- 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 {
-- 
2.34.1