From 2426f634bc43aae499fe658dba55fb525862658c Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Wed, 16 Aug 2017 00:22:07 -0700
Subject: [PATCH] Give vector more specific type

---
 src/AST/boolean.c           |  2 +-
 src/AST/order.c             |  6 +++---
 src/AST/order.h             |  2 +-
 src/Collections/structs.c   |  1 +
 src/Collections/structs.h   |  1 +
 src/Encoders/orderencoder.c | 32 +++++++++++++++++++++++---------
 src/Encoders/orderencoder.h |  3 ++-
 src/Encoders/ordergraph.c   | 14 ++++++--------
 src/Encoders/ordergraph.h   |  5 ++---
 src/Encoders/ordernode.c    |  1 +
 src/Encoders/ordernode.h    |  1 +
 11 files changed, 42 insertions(+), 26 deletions(-)

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 591bfe6..3ce75e4 100644
--- 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 92c52ae..054de91 100644
--- 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 bb35603..7a173b9 100644
--- 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 9c44ea7..459edd1 100644
--- 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 4343d34..5713e89 100644
--- 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 b87a982..d155921 100644
--- 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 ca3e415..e25ee42 100644
--- 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 2510fab..e6cb64e 100644
--- 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 1848d2e..a30c9f9 100644
--- 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 9f86b2b..072e54c 100644
--- 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 2e2ce9d..359b5bf 100644
--- 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);
-- 
2.34.1