X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FEncoders%2Forderencoder.c;h=0988abcc7e4e559e3ef4c63998e0b93431ebae17;hp=103b96204bbabefabcf6a4dda160fd5711ca93ca;hb=8762646584718c6bc1988e8aabb38924f6d56952;hpb=4221735881b9d1cd53ef410d9448efd2d12a51ad

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);
 	}