From ae9f38b4b72822a5a73909a795043bfcbb534e2f Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Tue, 22 Aug 2017 16:36:07 -0700
Subject: [PATCH] Add option to optimize edges in final encoding

---
 src/AST/order.c               |  1 +
 src/AST/order.h               |  1 +
 src/Backend/satencoder.c      |  3 +-
 src/Backend/satencoder.h      |  3 +-
 src/Backend/satorderencoder.c | 44 +++++++++++++++++----
 src/Backend/satorderencoder.h |  2 +-
 src/Encoders/orderencoder.c   | 10 -----
 src/Encoders/orderencoder.h   |  1 -
 src/Encoders/ordergraph.c     | 73 +++++++++++++++++++++++++++++++++++
 src/Encoders/ordergraph.h     |  6 +++
 src/Tuner/tunable.h           |  4 +-
 src/csolver.c                 |  2 +-
 12 files changed, 127 insertions(+), 23 deletions(-)

diff --git a/src/AST/order.c b/src/AST/order.c
index fde8c1f..3e0f73e 100644
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -10,6 +10,7 @@ Order *allocOrder(OrderType type, Set *set) {
 	This->type = type;
 	initOrderEncoding(&This->order, This);
 	This->orderPairTable = NULL;
+	This->graph = NULL;
 	return This;
 }
 
diff --git a/src/AST/order.h b/src/AST/order.h
index 53bf878..c5a03a8 100644
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -11,6 +11,7 @@ struct Order {
 	OrderType type;
 	Set *set;
 	HashTableOrderPair *orderPairTable;
+	OrderGraph *graph;
 	VectorBooleanOrder constraints;
 	OrderEncoding order;
 };
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index f380fdd..f5362b8 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -15,8 +15,9 @@
 
 //TODO: Should handle sharing of AST Nodes without recoding them a second time
 
-SATEncoder *allocSATEncoder() {
+SATEncoder *allocSATEncoder(CSolver *solver) {
 	SATEncoder *This = ourmalloc(sizeof (SATEncoder));
+	This->solver = solver;
 	This->varcount = 1;
 	This->cnf = createCNF();
 	return This;
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 8db6239..dee131d 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -9,13 +9,14 @@
 struct SATEncoder {
 	uint varcount;
 	CNF *cnf;
+	CSolver *solver;
 };
 
 #include "satelemencoder.h"
 #include "satorderencoder.h"
 #include "satfunctableencoder.h"
 
-SATEncoder *allocSATEncoder();
+SATEncoder *allocSATEncoder(CSolver *solver);
 void deleteSATEncoder(SATEncoder *This);
 void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This);
 Edge getNewVarSATEncoder(SATEncoder *This);
diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index 0b2622d..c3ee2a2 100644
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -2,8 +2,13 @@
 #include "structs.h"
 #include "common.h"
 #include "order.h"
+#include "csolver.h"
 #include "orderpair.h"
 #include "set.h"
+#include "tunable.h"
+#include "orderencoder.h"
+#include "ordergraph.h"
+#include "orderedge.h"
 
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
 	switch ( constraint->order->type) {
@@ -17,7 +22,29 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
 	return E_BOGUS;
 }
 
-Edge getPairConstraint(SATEncoder *This, HashTableOrderPair *table, OrderPair *pair) {
+Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
+	if (order->graph != NULL) {
+		OrderGraph *graph=order->graph;
+		OrderNode *first=lookupOrderNodeFromOrderGraph(graph, pair->first);
+		OrderNode *second=lookupOrderNodeFromOrderGraph(graph, pair->second);
+		if ((first != NULL) && (second != NULL)) {
+			OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
+			if (edge != NULL) {
+				if (edge->mustPos)
+					return E_True;
+				else if (edge->mustNeg)
+					return E_False;
+			}
+			OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, first, second);
+			if (invedge != NULL) {
+				if (invedge->mustPos)
+					return E_False;
+				else if (invedge->mustNeg)
+					return E_True;
+			}
+		}
+	}
+	HashTableOrderPair *table = order->orderPairTable;
 	bool negate = false;
 	OrderPair flipped;
 	if (pair->first < pair->second) {
@@ -41,11 +68,15 @@ Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
 	ASSERT(boolOrder->order->type == TOTAL);
 	if (boolOrder->order->orderPairTable == NULL) {
 		initializeOrderHashTable(boolOrder->order);
+		bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+		if (doOptOrderStructure) {
+			boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
+			reachMustAnalysis(This->solver, boolOrder->order->graph, true);
+		}
 		createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
 	}
-	HashTableOrderPair *orderPairTable = boolOrder->order->orderPairTable;
 	OrderPair pair = {boolOrder->first, boolOrder->second, E_NULL};
-	Edge constraint = getPairConstraint(This, orderPairTable, &pair);
+	Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
 	return constraint;
 }
 
@@ -56,20 +87,19 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
 #endif
 	ASSERT(order->type == TOTAL);
 	VectorInt *mems = order->set->members;
-	HashTableOrderPair *table = order->orderPairTable;
 	uint size = getSizeVectorInt(mems);
 	for (uint i = 0; i < size; i++) {
 		uint64_t valueI = getVectorInt(mems, i);
 		for (uint j = i + 1; j < size; j++) {
 			uint64_t valueJ = getVectorInt(mems, j);
 			OrderPair pairIJ = {valueI, valueJ};
-			Edge constIJ = getPairConstraint(This, table, &pairIJ);
+			Edge constIJ = getPairConstraint(This, order, &pairIJ);
 			for (uint k = j + 1; k < size; k++) {
 				uint64_t valueK = getVectorInt(mems, k);
 				OrderPair pairJK = {valueJ, valueK};
 				OrderPair pairIK = {valueI, valueK};
-				Edge constIK = getPairConstraint(This, table, &pairIK);
-				Edge constJK = getPairConstraint(This, table, &pairJK);
+				Edge constIK = getPairConstraint(This, order, &pairIK);
+				Edge constJK = getPairConstraint(This, order, &pairJK);
 				addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
 			}
 		}
diff --git a/src/Backend/satorderencoder.h b/src/Backend/satorderencoder.h
index 53d7415..e3342bf 100644
--- a/src/Backend/satorderencoder.h
+++ b/src/Backend/satorderencoder.h
@@ -2,7 +2,7 @@
 #define SATORDERENCODER_H
 
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-Edge getPairConstraint(SATEncoder *This, HashTableOrderPair *table, OrderPair *pair);
+Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair);
 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
 void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order);
diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index e97a17b..e172d18 100644
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -9,15 +9,6 @@
 #include "mutableset.h"
 #include "tunable.h"
 
-OrderGraph *buildOrderGraph(Order *order) {
-	OrderGraph *orderGraph = allocOrderGraph(order);
-	uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
-	for (uint j = 0; j < constrSize; j++) {
-		addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
-	}
-	return orderGraph;
-}
-
 void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
 	HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
 	while (hasNextOrderNode(iterator)) {
@@ -398,7 +389,6 @@ void orderAnalysis(CSolver *This) {
 	uint size = getSizeVectorOrder(This->allOrders);
 	for (uint i = 0; i < size; i++) {
 		Order *order = getVectorOrder(This->allOrders, i);
-		TunableDesc onoff={9, 1, 1};
 		bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
 		if (!doDecompose)
 			continue;
diff --git a/src/Encoders/orderencoder.h b/src/Encoders/orderencoder.h
index b0c13ac..67a56b9 100644
--- a/src/Encoders/orderencoder.h
+++ b/src/Encoders/orderencoder.h
@@ -11,7 +11,6 @@
 #include "structs.h"
 #include "mymemory.h"
 
-OrderGraph *buildOrderGraph(Order *order);
 void computeStronglyConnectedComponentGraph(OrderGraph *graph);
 void orderAnalysis(CSolver *solver);
 void initializeNodeInfoSCC(OrderGraph *graph);
diff --git a/src/Encoders/ordergraph.c b/src/Encoders/ordergraph.c
index c47a16f..f920076 100644
--- a/src/Encoders/ordergraph.c
+++ b/src/Encoders/ordergraph.c
@@ -13,6 +13,25 @@ OrderGraph *allocOrderGraph(Order *order) {
 	return This;
 }
 
+OrderGraph *buildOrderGraph(Order *order) {
+	OrderGraph *orderGraph = allocOrderGraph(order);
+	uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
+	for (uint j = 0; j < constrSize; j++) {
+		addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
+	}
+	return orderGraph;
+}
+
+//Builds only the subgraph for the must order graph.
+OrderGraph *buildMustOrderGraph(Order *order) {
+	OrderGraph *orderGraph = allocOrderGraph(order);
+	uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
+	for (uint j = 0; j < constrSize; j++) {
+		addMustOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
+	}
+	return orderGraph;
+}
+
 void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
 	Polarity polarity = constr->base.polarity;
 	BooleanValue mustval = constr->base.boolVal;
@@ -53,6 +72,42 @@ void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boolean
 	}
 }
 
+void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+	BooleanValue mustval = constr->base.boolVal;
+	Order *order = graph->order;
+	switch (mustval) {
+	case BV_UNSAT:
+	case BV_MUSTBETRUE: {
+		OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+		_1to2->mustPos = true;
+		_1to2->polPos = true;
+		addNewOutgoingEdge(node1, _1to2);
+		addNewIncomingEdge(node2, _1to2);
+		if (constr->base.polarity == BV_MUSTBETRUE)
+			break;
+	}
+	case BV_MUSTBEFALSE: {
+		if (order->type == TOTAL) {
+			OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+			_2to1->mustPos = true;
+			_2to1->polPos = true;
+			addNewOutgoingEdge(node2, _2to1);
+			addNewIncomingEdge(node1, _2to1);
+		} else {
+			OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+			_1to2->mustNeg = true;
+			_1to2->polNeg = true;
+			addNewOutgoingEdge(node1, _1to2);
+			addNewIncomingEdge(node2, _1to2);
+		}
+		break;
+	}
+	case BV_UNDEFINED:
+		//Do Nothing
+		break;
+	}
+}
+
 OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
 	OrderNode *node = allocOrderNode(id);
 	OrderNode *tmp = getHashSetOrderNode(graph->nodes, node);
@@ -65,6 +120,12 @@ OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
 	return node;
 }
 
+OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
+	OrderNode node = {id, NULL, NULL, 0, 0};
+	OrderNode *tmp = getHashSetOrderNode(graph->nodes, &node);
+	return tmp;
+}
+
 OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
 	OrderEdge *edge = allocOrderEdge(begin, end);
 	OrderEdge *tmp = getHashSetOrderEdge(graph->edges, edge);
@@ -77,6 +138,12 @@ OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, Order
 	return edge;
 }
 
+OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
+	OrderEdge edge = {begin, end, 0, 0, 0, 0, 0};
+	OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &edge);
+	return tmp;
+}
+
 OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
 	OrderEdge inverseedge = {edge->sink, edge->source, false, false, false, false, false};
 	OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &inverseedge);
@@ -89,6 +156,12 @@ void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
 	addOrderEdge(graph, from, to, bOrder);
 }
 
+void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
+	OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
+	OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
+	addMustOrderEdge(graph, from, to, bOrder);
+}
+
 void deleteOrderGraph(OrderGraph *graph) {
 	HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
 	while (hasNextOrderNode(iterator)) {
diff --git a/src/Encoders/ordergraph.h b/src/Encoders/ordergraph.h
index 5540d73..33f2b69 100644
--- a/src/Encoders/ordergraph.h
+++ b/src/Encoders/ordergraph.h
@@ -18,10 +18,16 @@ struct OrderGraph {
 };
 
 OrderGraph *allocOrderGraph(Order *order);
+OrderGraph *buildOrderGraph(Order *order);
+OrderGraph *buildMustOrderGraph(Order *order);
 void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
+void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
 OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
 OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
+OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
+OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
 void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+void addMustOrderEdge(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/Tuner/tunable.h b/src/Tuner/tunable.h
index 66c4638..cbd9f29 100644
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -21,6 +21,8 @@ int getVarTunable(Tuner *This, VarType vartype, TunableParam param, TunableDesc
 #define GETTUNABLE(This, param, descriptor) getTunable(This, param, descriptor)
 #define GETVARTUNABLE(This, vartype, param, descriptor) getTunable(This, param, descriptor)
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE};
+static TunableDesc onoff={0, 1, 1};
+static TunableDesc offon={0, 1, 0};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE};
 typedef enum Tunables Tunables;
 #endif
diff --git a/src/csolver.c b/src/csolver.c
index fbc8691..e9c9526 100644
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -24,8 +24,8 @@ CSolver *allocCSolver() {
 	This->allTables = allocDefVectorTable();
 	This->allOrders = allocDefVectorOrder();
 	This->allFunctions = allocDefVectorFunction();
-	This->satEncoder = allocSATEncoder();
 	This->tuner = allocTuner();
+	This->satEncoder = allocSATEncoder(This);
 	return This;
 }
 
-- 
2.34.1