From 9cb55c1cf260106cf90f7aa39b08157d113599bd Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Tue, 22 Aug 2017 22:38:45 -0700
Subject: [PATCH] Implement Partial->Total Conversion

---
 src/Encoders/orderencoder.c | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index 066695c..a43d39d 100644
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -327,7 +327,9 @@ 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);
@@ -353,6 +355,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 +368,25 @@ 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;
+	}
+	
 	deleteVectorArrayOrder(&ordervec);
+	deleteVectorArrayOrder(&partialcandidatevec);
 }
 
 void orderAnalysis(CSolver *This) {
-- 
2.34.1