From: bdemsky <bdemsky@uci.edu>
Date: Tue, 15 Aug 2017 00:11:30 +0000 (-0700)
Subject: Build graph
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=53f1d02751830f89c0faa6ebeaa2a1b737e61577;p=satune.git

Build graph
---

diff --git a/src/Encoders/orderedge.c b/src/Encoders/orderedge.c
index d8466af..02f09e9 100644
--- a/src/Encoders/orderedge.c
+++ b/src/Encoders/orderedge.c
@@ -4,6 +4,10 @@ OrderEdge* allocOrderEdge(OrderNode* source, OrderNode* sink) {
 	OrderEdge* This = (OrderEdge*) ourmalloc(sizeof(OrderEdge));
 	This->source = source;
 	This->sink = sink;
+	This->polPos = false;
+	This->polNeg = false;
+	This->mustPos = false;
+	This->mustNeg = false;
 	return This;
 }
 
diff --git a/src/Encoders/orderedge.h b/src/Encoders/orderedge.h
index 52501af..8785a0c 100644
--- a/src/Encoders/orderedge.h
+++ b/src/Encoders/orderedge.h
@@ -9,11 +9,14 @@
 #define ORDEREDGE_H
 #include "classlist.h"
 #include "mymemory.h"
-#include "ordernode.h"
 
 struct OrderEdge {
 	OrderNode* source;
 	OrderNode* sink;
+	unsigned int polPos:1;
+	unsigned int polNeg:1;
+	unsigned int mustPos:1;
+	unsigned int mustNeg:1;
 };
 
 OrderEdge* allocOrderEdge(OrderNode* begin, OrderNode* end);
diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index 8ac2649..1fc80d1 100644
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -44,7 +44,7 @@ OrderEncoder* buildOrderGraphs(CSolver* This) {
 }
 
 OrderGraph* buildOrderGraph(Order *order) {
-	OrderGraph* orderGraph = allocOrderGraph();
+	OrderGraph* orderGraph = allocOrderGraph(order);
 	uint constrSize = getSizeVectorBoolean(&order->constraints);
 	for(uint j=0; j<constrSize; j++){
 		addOrderConstraintToOrderGraph(orderGraph, getVectorBoolean(&order->constraints, j));
diff --git a/src/Encoders/ordergraph.c b/src/Encoders/ordergraph.c
index f2f8bd0..5aa1c0d 100644
--- a/src/Encoders/ordergraph.c
+++ b/src/Encoders/ordergraph.c
@@ -2,33 +2,54 @@
 #include "ordernode.h"
 #include "boolean.h"
 #include "orderedge.h"
+#include "ordergraph.h"
+#include "order.h"
 
-OrderGraph* allocOrderGraph() {
+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) {
-	switch(constr->polarity){
-		case P_BOTHTRUEFALSE:
-		case P_TRUE:{
-			OrderEdge* _1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
-			addNewOutgoingEdge(node1, _1to2);
-			addNewIncomingEdge(node2, _1to2);
-			if(constr->polarity == P_TRUE)
-				break;
-		}
-		case P_FALSE:{
+	Polarity polarity=constr->polarity;
+	BooleanValue mustval=constr->boolVal;
+	Order* order=graph->order;
+	switch(polarity) {
+	case P_BOTHTRUEFALSE:
+	case P_TRUE:{
+		OrderEdge* _1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+		_1to2->polPos=true;
+		if (mustval==BV_MUSTBETRUE || mustval == BV_UNSAT)
+			_1to2->mustPos=true;
+		addNewOutgoingEdge(node1, _1to2);
+		addNewIncomingEdge(node2, _1to2);
+		if(constr->polarity == P_TRUE)
+			break;
+	}
+	case P_FALSE:{
+		if (order->type==TOTAL) {
 			OrderEdge* _2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+			_2to1->polPos=true;
+			if (mustval==BV_MUSTBEFALSE || mustval == BV_UNSAT)
+				_2to1->mustPos=true;
 			addNewOutgoingEdge(node2, _2to1);
 			addNewIncomingEdge(node1, _2to1);
-			break;
+		} else {
+			OrderEdge* _1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+			_1to2->polNeg=true;
+			if (mustval==BV_MUSTBEFALSE || mustval == BV_UNSAT)
+				_1to2->mustNeg=true;
+			addNewOutgoingEdge(node1, _1to2);
+			addNewIncomingEdge(node2, _1to2);
 		}
-		default:
-			ASSERT(0);
-				
+		break;
+	}
+	case P_UNDEFINED:
+		//There is an unreachable order constraint if this assert fires
+		ASSERT(0);
 	}
 }
 
diff --git a/src/Encoders/ordergraph.h b/src/Encoders/ordergraph.h
index 3f94442..34aadfa 100644
--- a/src/Encoders/ordergraph.h
+++ b/src/Encoders/ordergraph.h
@@ -14,10 +14,11 @@
 struct OrderGraph {
 	HashSetOrderNode* nodes;
 	HashSetOrderEdge* edges;
+	Order* order;
 	VectorOrderNode scc;
 };
 
-OrderGraph* allocOrderGraph();
+OrderGraph* allocOrderGraph(Order *order);
 void addOrderConstraintToOrderGraph(OrderGraph* graph, Boolean* constr);
 OrderNode* getOrderNodeFromOrderGraph(OrderGraph* graph, uint64_t id);
 OrderEdge* getOrderEdgeFromOrderGraph(OrderGraph* graph, OrderNode* begin, OrderNode* end);