From: bdemsky <bdemsky@uci.edu>
Date: Fri, 25 Aug 2017 02:30:37 +0000 (-0700)
Subject: Move Files
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=ac1280eb468f2d2e0080b0506f12c3afba2fd507;p=satune.git

Move Files
---

diff --git a/src/ASTAnalyses/orderedge.cc b/src/ASTAnalyses/orderedge.cc
new file mode 100644
index 0000000..c4632da
--- /dev/null
+++ b/src/ASTAnalyses/orderedge.cc
@@ -0,0 +1,19 @@
+#include "orderedge.h"
+#include "ordergraph.h"
+
+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;
+	This->pseudoPos = false;
+	return This;
+}
+
+void deleteOrderEdge(OrderEdge *This) {
+	ourfree(This);
+}
+
diff --git a/src/ASTAnalyses/orderedge.h b/src/ASTAnalyses/orderedge.h
new file mode 100644
index 0000000..21fa903
--- /dev/null
+++ b/src/ASTAnalyses/orderedge.h
@@ -0,0 +1,32 @@
+/*
+ * File:   orderedge.h
+ * Author: hamed
+ *
+ * Created on August 7, 2017, 3:44 PM
+ */
+
+#ifndef ORDEREDGE_H
+#define ORDEREDGE_H
+#include "classlist.h"
+#include "mymemory.h"
+
+struct OrderEdge {
+	OrderNode *source;
+	OrderNode *sink;
+	unsigned int polPos : 1;
+	unsigned int polNeg : 1;
+	unsigned int mustPos : 1;
+	unsigned int mustNeg : 1;
+	unsigned int pseudoPos : 1;
+};
+
+OrderEdge *allocOrderEdge(OrderNode *begin, OrderNode *end);
+void deleteOrderEdge(OrderEdge *This);
+void setPseudoPos(OrderGraph *graph, OrderEdge *edge);
+void setMustPos(OrderGraph *graph, OrderEdge *edge);
+void setMustNeg(OrderGraph *graph, OrderEdge *edge);
+void setPolPos(OrderGraph *graph, OrderEdge *edge);
+void setPolNeg(OrderGraph *graph, OrderEdge *edge);
+
+#endif/* ORDEREDGE_H */
+
diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc
new file mode 100644
index 0000000..0871a41
--- /dev/null
+++ b/src/ASTAnalyses/ordergraph.cc
@@ -0,0 +1,182 @@
+#include "ordergraph.h"
+#include "ordernode.h"
+#include "boolean.h"
+#include "orderedge.h"
+#include "ordergraph.h"
+#include "order.h"
+
+OrderGraph *allocOrderGraph(Order *order) {
+	OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
+	This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+	This->edges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+	This->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->polarity;
+	BooleanValue mustval = constr->boolVal;
+	Order *order = graph->order;
+	switch (polarity) {
+	case P_BOTHTRUEFALSE:
+	case P_TRUE: {
+		OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+		if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
+			_1to2->mustPos = true;
+		_1to2->polPos = 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);
+			if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
+				_2to1->mustPos = true;
+			_2to1->polPos = true;
+			addNewOutgoingEdge(node2, _2to1);
+			addNewIncomingEdge(node1, _2to1);
+		} else {
+			OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+			if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
+				_1to2->mustNeg = true;
+			_1to2->polNeg = true;
+			addNewOutgoingEdge(node1, _1to2);
+			addNewIncomingEdge(node2, _1to2);
+		}
+		break;
+	}
+	case P_UNDEFINED:
+		//There is an unreachable order constraint if this assert fires
+		ASSERT(0);
+	}
+}
+
+void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+	BooleanValue mustval = constr->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->boolVal == 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);
+	if ( tmp != NULL) {
+		deleteOrderNode(node);
+		node = tmp;
+	} else {
+		addHashSetOrderNode(graph->nodes, node);
+	}
+	return node;
+}
+
+OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
+	OrderNode node = {id, NULL, NULL, NOTVISITED, 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);
+	if ( tmp != NULL ) {
+		deleteOrderEdge(edge);
+		edge = tmp;
+	} else {
+		addHashSetOrderEdge(graph->edges, edge);
+	}
+	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);
+	return tmp;
+}
+
+void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
+	OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
+	OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
+	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)) {
+		OrderNode *node = nextOrderNode(iterator);
+		deleteOrderNode(node);
+	}
+	deleteIterOrderNode(iterator);
+
+	HSIteratorOrderEdge *eiterator = iteratorOrderEdge(graph->edges);
+	while (hasNextOrderEdge(eiterator)) {
+		OrderEdge *edge = nextOrderEdge(eiterator);
+		deleteOrderEdge(edge);
+	}
+	deleteIterOrderEdge(eiterator);
+	deleteHashSetOrderNode(graph->nodes);
+	deleteHashSetOrderEdge(graph->edges);
+	ourfree(graph);
+}
diff --git a/src/ASTAnalyses/ordergraph.h b/src/ASTAnalyses/ordergraph.h
new file mode 100644
index 0000000..33f2b69
--- /dev/null
+++ b/src/ASTAnalyses/ordergraph.h
@@ -0,0 +1,34 @@
+/*
+ * File:   ordergraph.h
+ * Author: hamed
+ *
+ * Created on August 7, 2017, 3:42 PM
+ */
+
+#ifndef ORDERGRAPH_H
+#define ORDERGRAPH_H
+#include "classlist.h"
+#include "structs.h"
+#include "mymemory.h"
+
+struct OrderGraph {
+	HashSetOrderNode *nodes;
+	HashSetOrderEdge *edges;
+	Order *order;
+};
+
+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/ASTAnalyses/ordernode.cc b/src/ASTAnalyses/ordernode.cc
new file mode 100644
index 0000000..c0bd096
--- /dev/null
+++ b/src/ASTAnalyses/ordernode.cc
@@ -0,0 +1,28 @@
+#include "ordernode.h"
+#include "orderedge.h"
+
+OrderNode *allocOrderNode(uint64_t id) {
+	OrderNode *This = (OrderNode *) ourmalloc(sizeof(OrderNode));
+	This->id = 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;
+}
+
+void addNewIncomingEdge(OrderNode *node, OrderEdge *edge) {
+	ASSERT(!containsHashSetOrderEdge(node->inEdges, edge));	// Only for testing ... Should be removed after testing
+	addHashSetOrderEdge(node->inEdges, edge);
+}
+
+void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge) {
+	ASSERT(!containsHashSetOrderEdge(node->outEdges, edge));
+	addHashSetOrderEdge(node->outEdges, edge);
+}
+
+void deleteOrderNode(OrderNode *node) {
+	deleteHashSetOrderEdge(node->inEdges);
+	deleteHashSetOrderEdge(node->outEdges);
+	ourfree(node);
+}
diff --git a/src/ASTAnalyses/ordernode.h b/src/ASTAnalyses/ordernode.h
new file mode 100644
index 0000000..81e1993
--- /dev/null
+++ b/src/ASTAnalyses/ordernode.h
@@ -0,0 +1,34 @@
+
+/*
+ * File:   ordernode.h
+ * Author: hamed
+ *
+ * Created on August 7, 2017, 3:43 PM
+ */
+
+#ifndef ORDERNODE_H
+#define ORDERNODE_H
+
+#include "classlist.h"
+#include "mymemory.h"
+#include "structs.h"
+#include "orderedge.h"
+
+enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET};
+typedef enum NodeStatus NodeStatus;
+
+struct OrderNode {
+	uint64_t id;
+	HashSetOrderEdge *inEdges;
+	HashSetOrderEdge *outEdges;
+	NodeStatus status;
+	uint sccNum;
+};
+
+OrderNode *allocOrderNode(uint64_t id);
+void addNewIncomingEdge(OrderNode *node, OrderEdge *edge);
+void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge);
+void deleteOrderNode(OrderNode *node);
+
+#endif/* ORDERNODE_H */
+
diff --git a/src/ASTAnalyses/polarityassignment.cc b/src/ASTAnalyses/polarityassignment.cc
new file mode 100644
index 0000000..bf787ea
--- /dev/null
+++ b/src/ASTAnalyses/polarityassignment.cc
@@ -0,0 +1,152 @@
+#include "polarityassignment.h"
+#include "csolver.h"
+
+void computePolarities(CSolver *This) {
+	HSIteratorBoolean *iterator=iteratorBoolean(This->constraints);
+	while(hasNextBoolean(iterator)) {
+		Boolean *boolean = nextBoolean(iterator);
+		updatePolarity(boolean, P_TRUE);
+		updateMustValue(boolean, BV_MUSTBETRUE);
+		computePolarityAndBooleanValue(boolean);
+	}
+	deleteIterBoolean(iterator);
+}
+
+void updatePolarity(Boolean *This, Polarity polarity) {
+	This->polarity = (Polarity) (This->polarity | polarity);
+}
+
+void updateMustValue(Boolean *This, BooleanValue value) {
+	This->boolVal = (BooleanValue) (This->boolVal | value);
+}
+
+void computePolarityAndBooleanValue(Boolean *This) {
+	switch (GETBOOLEANTYPE(This)) {
+	case BOOLEANVAR:
+	case ORDERCONST:
+		return;
+	case PREDICATEOP:
+		return computePredicatePolarityAndBooleanValue((BooleanPredicate *)This);
+	case LOGICOP:
+		return computeLogicOpPolarityAndBooleanValue((BooleanLogic *)This);
+	default:
+		ASSERT(0);
+	}
+}
+
+void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
+	if (This->undefStatus != NULL) {
+		updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
+		computePolarityAndBooleanValue(This->undefStatus);
+	}
+}
+
+void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
+	computeLogicOpBooleanValue(This);
+	computeLogicOpPolarity(This);
+	uint size = getSizeArrayBoolean(&This->inputs);
+	for (uint i = 0; i < size; i++) {
+		computePolarityAndBooleanValue(getArrayBoolean(&This->inputs, i));
+	}
+}
+
+Polarity negatePolarity(Polarity This) {
+	switch (This) {
+	case P_UNDEFINED:
+	case P_BOTHTRUEFALSE:
+		return This;
+	case P_TRUE:
+		return P_FALSE;
+	case P_FALSE:
+		return P_TRUE;
+	default:
+		ASSERT(0);
+	}
+}
+
+BooleanValue negateBooleanValue(BooleanValue This) {
+	switch (This) {
+	case BV_UNDEFINED:
+	case BV_UNSAT:
+		return This;
+	case BV_MUSTBETRUE:
+		return BV_MUSTBEFALSE;
+	case BV_MUSTBEFALSE:
+		return BV_MUSTBETRUE;
+	default:
+		ASSERT(0);
+	}
+}
+
+void computeLogicOpPolarity(BooleanLogic *This) {
+	Polarity parentpolarity = GETBOOLEANPOLARITY(This);
+	switch (This->op) {
+	case L_AND:
+	case L_OR: {
+		uint size = getSizeArrayBoolean(&This->inputs);
+		for (uint i = 0; i < size; i++) {
+			Boolean *tmp = getArrayBoolean(&This->inputs, i);
+			updatePolarity(tmp, parentpolarity);
+		}
+		break;
+	}
+	case L_NOT: {
+		Boolean *tmp = getArrayBoolean(&This->inputs, 0);
+		updatePolarity(tmp, negatePolarity(parentpolarity));
+		break;
+	}
+	case L_XOR: {
+		updatePolarity(getArrayBoolean(&This->inputs, 0), P_BOTHTRUEFALSE);
+		updatePolarity(getArrayBoolean(&This->inputs, 1), P_BOTHTRUEFALSE);
+		break;
+	}
+	case L_IMPLIES: {
+		Boolean *left = getArrayBoolean(&This->inputs, 0);
+		updatePolarity(left, negatePolarity( parentpolarity));
+		Boolean *right = getArrayBoolean(&This->inputs, 1);
+		updatePolarity(right, parentpolarity);
+		break;
+	}
+	default:
+		ASSERT(0);
+	}
+}
+
+void computeLogicOpBooleanValue(BooleanLogic *This) {
+	BooleanValue parentbv = GETBOOLEANVALUE(This);
+	switch (This->op) {
+	case L_AND: {
+		if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
+			uint size = getSizeArrayBoolean(&This->inputs);
+			for (uint i = 0; i < size; i++) {
+				updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
+			}
+		}
+		return;
+	}
+	case L_OR: {
+		if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
+			uint size = getSizeArrayBoolean(&This->inputs);
+			for (uint i = 0; i < size; i++) {
+				updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
+			}
+		}
+		return;
+	}
+	case L_NOT:
+		updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
+		return;
+	case L_IMPLIES:
+		//implies is really an or with the first term negated
+		if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
+			uint size = getSizeArrayBoolean(&This->inputs);
+			updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
+			updateMustValue(getArrayBoolean(&This->inputs, 1), parentbv);
+		}
+		return;
+	case L_XOR:
+		return;
+	default:
+		ASSERT(0);
+	}
+}
diff --git a/src/ASTAnalyses/polarityassignment.h b/src/ASTAnalyses/polarityassignment.h
new file mode 100644
index 0000000..6621d77
--- /dev/null
+++ b/src/ASTAnalyses/polarityassignment.h
@@ -0,0 +1,27 @@
+/*
+ * File:   polarityassignment.h
+ * Author: hamed
+ *
+ * Created on August 6, 2017, 12:18 PM
+ */
+
+#ifndef POLARITYASSIGNMENT_H
+#define POLARITYASSIGNMENT_H
+#include "classlist.h"
+#include "mymemory.h"
+#include "common.h"
+#include "ops.h"
+#include "boolean.h"
+
+void computePolarities(CSolver *This);
+void updatePolarity(Boolean *This, Polarity polarity);
+void updateMustValue(Boolean *This, BooleanValue value);
+void computePolarityAndBooleanValue(Boolean *boolean);
+void computePredicatePolarityAndBooleanValue(BooleanPredicate *This);
+void computeLogicOpPolarityAndBooleanValue(BooleanLogic *boolean);
+Polarity negatePolarity(Polarity This);
+BooleanValue negateBooleanValue(BooleanValue This);
+void computeLogicOpPolarity(BooleanLogic *boolean);
+void computeLogicOpBooleanValue(BooleanLogic *boolean);
+
+#endif/* POLARITYASSIGNMENT_H */
diff --git a/src/Encoders/orderedge.cc b/src/Encoders/orderedge.cc
deleted file mode 100644
index c4632da..0000000
--- a/src/Encoders/orderedge.cc
+++ /dev/null
@@ -1,19 +0,0 @@
-#include "orderedge.h"
-#include "ordergraph.h"
-
-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;
-	This->pseudoPos = false;
-	return This;
-}
-
-void deleteOrderEdge(OrderEdge *This) {
-	ourfree(This);
-}
-
diff --git a/src/Encoders/orderedge.h b/src/Encoders/orderedge.h
deleted file mode 100644
index 21fa903..0000000
--- a/src/Encoders/orderedge.h
+++ /dev/null
@@ -1,32 +0,0 @@
-/*
- * File:   orderedge.h
- * Author: hamed
- *
- * Created on August 7, 2017, 3:44 PM
- */
-
-#ifndef ORDEREDGE_H
-#define ORDEREDGE_H
-#include "classlist.h"
-#include "mymemory.h"
-
-struct OrderEdge {
-	OrderNode *source;
-	OrderNode *sink;
-	unsigned int polPos : 1;
-	unsigned int polNeg : 1;
-	unsigned int mustPos : 1;
-	unsigned int mustNeg : 1;
-	unsigned int pseudoPos : 1;
-};
-
-OrderEdge *allocOrderEdge(OrderNode *begin, OrderNode *end);
-void deleteOrderEdge(OrderEdge *This);
-void setPseudoPos(OrderGraph *graph, OrderEdge *edge);
-void setMustPos(OrderGraph *graph, OrderEdge *edge);
-void setMustNeg(OrderGraph *graph, OrderEdge *edge);
-void setPolPos(OrderGraph *graph, OrderEdge *edge);
-void setPolNeg(OrderGraph *graph, OrderEdge *edge);
-
-#endif/* ORDEREDGE_H */
-
diff --git a/src/Encoders/ordergraph.cc b/src/Encoders/ordergraph.cc
deleted file mode 100644
index 0871a41..0000000
--- a/src/Encoders/ordergraph.cc
+++ /dev/null
@@ -1,182 +0,0 @@
-#include "ordergraph.h"
-#include "ordernode.h"
-#include "boolean.h"
-#include "orderedge.h"
-#include "ordergraph.h"
-#include "order.h"
-
-OrderGraph *allocOrderGraph(Order *order) {
-	OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
-	This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
-	This->edges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
-	This->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->polarity;
-	BooleanValue mustval = constr->boolVal;
-	Order *order = graph->order;
-	switch (polarity) {
-	case P_BOTHTRUEFALSE:
-	case P_TRUE: {
-		OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
-		if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
-			_1to2->mustPos = true;
-		_1to2->polPos = 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);
-			if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
-				_2to1->mustPos = true;
-			_2to1->polPos = true;
-			addNewOutgoingEdge(node2, _2to1);
-			addNewIncomingEdge(node1, _2to1);
-		} else {
-			OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
-			if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
-				_1to2->mustNeg = true;
-			_1to2->polNeg = true;
-			addNewOutgoingEdge(node1, _1to2);
-			addNewIncomingEdge(node2, _1to2);
-		}
-		break;
-	}
-	case P_UNDEFINED:
-		//There is an unreachable order constraint if this assert fires
-		ASSERT(0);
-	}
-}
-
-void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
-	BooleanValue mustval = constr->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->boolVal == 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);
-	if ( tmp != NULL) {
-		deleteOrderNode(node);
-		node = tmp;
-	} else {
-		addHashSetOrderNode(graph->nodes, node);
-	}
-	return node;
-}
-
-OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
-	OrderNode node = {id, NULL, NULL, NOTVISITED, 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);
-	if ( tmp != NULL ) {
-		deleteOrderEdge(edge);
-		edge = tmp;
-	} else {
-		addHashSetOrderEdge(graph->edges, edge);
-	}
-	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);
-	return tmp;
-}
-
-void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
-	OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
-	OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
-	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)) {
-		OrderNode *node = nextOrderNode(iterator);
-		deleteOrderNode(node);
-	}
-	deleteIterOrderNode(iterator);
-
-	HSIteratorOrderEdge *eiterator = iteratorOrderEdge(graph->edges);
-	while (hasNextOrderEdge(eiterator)) {
-		OrderEdge *edge = nextOrderEdge(eiterator);
-		deleteOrderEdge(edge);
-	}
-	deleteIterOrderEdge(eiterator);
-	deleteHashSetOrderNode(graph->nodes);
-	deleteHashSetOrderEdge(graph->edges);
-	ourfree(graph);
-}
diff --git a/src/Encoders/ordergraph.h b/src/Encoders/ordergraph.h
deleted file mode 100644
index 33f2b69..0000000
--- a/src/Encoders/ordergraph.h
+++ /dev/null
@@ -1,34 +0,0 @@
-/*
- * File:   ordergraph.h
- * Author: hamed
- *
- * Created on August 7, 2017, 3:42 PM
- */
-
-#ifndef ORDERGRAPH_H
-#define ORDERGRAPH_H
-#include "classlist.h"
-#include "structs.h"
-#include "mymemory.h"
-
-struct OrderGraph {
-	HashSetOrderNode *nodes;
-	HashSetOrderEdge *edges;
-	Order *order;
-};
-
-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/Encoders/ordernode.cc b/src/Encoders/ordernode.cc
deleted file mode 100644
index c0bd096..0000000
--- a/src/Encoders/ordernode.cc
+++ /dev/null
@@ -1,28 +0,0 @@
-#include "ordernode.h"
-#include "orderedge.h"
-
-OrderNode *allocOrderNode(uint64_t id) {
-	OrderNode *This = (OrderNode *) ourmalloc(sizeof(OrderNode));
-	This->id = 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;
-}
-
-void addNewIncomingEdge(OrderNode *node, OrderEdge *edge) {
-	ASSERT(!containsHashSetOrderEdge(node->inEdges, edge));	// Only for testing ... Should be removed after testing
-	addHashSetOrderEdge(node->inEdges, edge);
-}
-
-void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge) {
-	ASSERT(!containsHashSetOrderEdge(node->outEdges, edge));
-	addHashSetOrderEdge(node->outEdges, edge);
-}
-
-void deleteOrderNode(OrderNode *node) {
-	deleteHashSetOrderEdge(node->inEdges);
-	deleteHashSetOrderEdge(node->outEdges);
-	ourfree(node);
-}
diff --git a/src/Encoders/ordernode.h b/src/Encoders/ordernode.h
deleted file mode 100644
index 81e1993..0000000
--- a/src/Encoders/ordernode.h
+++ /dev/null
@@ -1,34 +0,0 @@
-
-/*
- * File:   ordernode.h
- * Author: hamed
- *
- * Created on August 7, 2017, 3:43 PM
- */
-
-#ifndef ORDERNODE_H
-#define ORDERNODE_H
-
-#include "classlist.h"
-#include "mymemory.h"
-#include "structs.h"
-#include "orderedge.h"
-
-enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET};
-typedef enum NodeStatus NodeStatus;
-
-struct OrderNode {
-	uint64_t id;
-	HashSetOrderEdge *inEdges;
-	HashSetOrderEdge *outEdges;
-	NodeStatus status;
-	uint sccNum;
-};
-
-OrderNode *allocOrderNode(uint64_t id);
-void addNewIncomingEdge(OrderNode *node, OrderEdge *edge);
-void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge);
-void deleteOrderNode(OrderNode *node);
-
-#endif/* ORDERNODE_H */
-
diff --git a/src/Encoders/polarityassignment.cc b/src/Encoders/polarityassignment.cc
deleted file mode 100644
index bf787ea..0000000
--- a/src/Encoders/polarityassignment.cc
+++ /dev/null
@@ -1,152 +0,0 @@
-#include "polarityassignment.h"
-#include "csolver.h"
-
-void computePolarities(CSolver *This) {
-	HSIteratorBoolean *iterator=iteratorBoolean(This->constraints);
-	while(hasNextBoolean(iterator)) {
-		Boolean *boolean = nextBoolean(iterator);
-		updatePolarity(boolean, P_TRUE);
-		updateMustValue(boolean, BV_MUSTBETRUE);
-		computePolarityAndBooleanValue(boolean);
-	}
-	deleteIterBoolean(iterator);
-}
-
-void updatePolarity(Boolean *This, Polarity polarity) {
-	This->polarity = (Polarity) (This->polarity | polarity);
-}
-
-void updateMustValue(Boolean *This, BooleanValue value) {
-	This->boolVal = (BooleanValue) (This->boolVal | value);
-}
-
-void computePolarityAndBooleanValue(Boolean *This) {
-	switch (GETBOOLEANTYPE(This)) {
-	case BOOLEANVAR:
-	case ORDERCONST:
-		return;
-	case PREDICATEOP:
-		return computePredicatePolarityAndBooleanValue((BooleanPredicate *)This);
-	case LOGICOP:
-		return computeLogicOpPolarityAndBooleanValue((BooleanLogic *)This);
-	default:
-		ASSERT(0);
-	}
-}
-
-void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
-	if (This->undefStatus != NULL) {
-		updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
-		computePolarityAndBooleanValue(This->undefStatus);
-	}
-}
-
-void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
-	computeLogicOpBooleanValue(This);
-	computeLogicOpPolarity(This);
-	uint size = getSizeArrayBoolean(&This->inputs);
-	for (uint i = 0; i < size; i++) {
-		computePolarityAndBooleanValue(getArrayBoolean(&This->inputs, i));
-	}
-}
-
-Polarity negatePolarity(Polarity This) {
-	switch (This) {
-	case P_UNDEFINED:
-	case P_BOTHTRUEFALSE:
-		return This;
-	case P_TRUE:
-		return P_FALSE;
-	case P_FALSE:
-		return P_TRUE;
-	default:
-		ASSERT(0);
-	}
-}
-
-BooleanValue negateBooleanValue(BooleanValue This) {
-	switch (This) {
-	case BV_UNDEFINED:
-	case BV_UNSAT:
-		return This;
-	case BV_MUSTBETRUE:
-		return BV_MUSTBEFALSE;
-	case BV_MUSTBEFALSE:
-		return BV_MUSTBETRUE;
-	default:
-		ASSERT(0);
-	}
-}
-
-void computeLogicOpPolarity(BooleanLogic *This) {
-	Polarity parentpolarity = GETBOOLEANPOLARITY(This);
-	switch (This->op) {
-	case L_AND:
-	case L_OR: {
-		uint size = getSizeArrayBoolean(&This->inputs);
-		for (uint i = 0; i < size; i++) {
-			Boolean *tmp = getArrayBoolean(&This->inputs, i);
-			updatePolarity(tmp, parentpolarity);
-		}
-		break;
-	}
-	case L_NOT: {
-		Boolean *tmp = getArrayBoolean(&This->inputs, 0);
-		updatePolarity(tmp, negatePolarity(parentpolarity));
-		break;
-	}
-	case L_XOR: {
-		updatePolarity(getArrayBoolean(&This->inputs, 0), P_BOTHTRUEFALSE);
-		updatePolarity(getArrayBoolean(&This->inputs, 1), P_BOTHTRUEFALSE);
-		break;
-	}
-	case L_IMPLIES: {
-		Boolean *left = getArrayBoolean(&This->inputs, 0);
-		updatePolarity(left, negatePolarity( parentpolarity));
-		Boolean *right = getArrayBoolean(&This->inputs, 1);
-		updatePolarity(right, parentpolarity);
-		break;
-	}
-	default:
-		ASSERT(0);
-	}
-}
-
-void computeLogicOpBooleanValue(BooleanLogic *This) {
-	BooleanValue parentbv = GETBOOLEANVALUE(This);
-	switch (This->op) {
-	case L_AND: {
-		if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
-			uint size = getSizeArrayBoolean(&This->inputs);
-			for (uint i = 0; i < size; i++) {
-				updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
-			}
-		}
-		return;
-	}
-	case L_OR: {
-		if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
-			uint size = getSizeArrayBoolean(&This->inputs);
-			for (uint i = 0; i < size; i++) {
-				updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
-			}
-		}
-		return;
-	}
-	case L_NOT:
-		updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
-		return;
-	case L_IMPLIES:
-		//implies is really an or with the first term negated
-		if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
-			uint size = getSizeArrayBoolean(&This->inputs);
-			updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
-			updateMustValue(getArrayBoolean(&This->inputs, 1), parentbv);
-		}
-		return;
-	case L_XOR:
-		return;
-	default:
-		ASSERT(0);
-	}
-}
diff --git a/src/Encoders/polarityassignment.h b/src/Encoders/polarityassignment.h
deleted file mode 100644
index 6621d77..0000000
--- a/src/Encoders/polarityassignment.h
+++ /dev/null
@@ -1,27 +0,0 @@
-/*
- * File:   polarityassignment.h
- * Author: hamed
- *
- * Created on August 6, 2017, 12:18 PM
- */
-
-#ifndef POLARITYASSIGNMENT_H
-#define POLARITYASSIGNMENT_H
-#include "classlist.h"
-#include "mymemory.h"
-#include "common.h"
-#include "ops.h"
-#include "boolean.h"
-
-void computePolarities(CSolver *This);
-void updatePolarity(Boolean *This, Polarity polarity);
-void updateMustValue(Boolean *This, BooleanValue value);
-void computePolarityAndBooleanValue(Boolean *boolean);
-void computePredicatePolarityAndBooleanValue(BooleanPredicate *This);
-void computeLogicOpPolarityAndBooleanValue(BooleanLogic *boolean);
-Polarity negatePolarity(Polarity This);
-BooleanValue negateBooleanValue(BooleanValue This);
-void computeLogicOpPolarity(BooleanLogic *boolean);
-void computeLogicOpBooleanValue(BooleanLogic *boolean);
-
-#endif/* POLARITYASSIGNMENT_H */
diff --git a/src/Makefile b/src/Makefile
index 7a45513..c2d10b7 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -4,14 +4,14 @@ PHONY += directories
 MKDIR_P = mkdir -p
 OBJ_DIR = bin
 
-CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc)
+CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc)
 
-HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h)
+HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h)
 
 OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o)
 
 CFLAGS := -Wall -g -O0
-CFLAGS += -IAST -ICollections -IBackend -I. -IEncoders -ITuner
+CFLAGS += -IAST -IASTTransform -IASTAnalyses -ICollections -IBackend -I. -IEncoders -ITuner
 LDFLAGS := -ldl -lrt -rdynamic
 SHARED := -shared
 
@@ -30,6 +30,8 @@ directories: ${OBJ_DIR}
 ${OBJ_DIR}:
 	${MKDIR_P} ${OBJ_DIR}
 	${MKDIR_P} ${OBJ_DIR}/AST
+	${MKDIR_P} ${OBJ_DIR}/ASTAnalyses
+	${MKDIR_P} ${OBJ_DIR}/ASTTransform
 	${MKDIR_P} ${OBJ_DIR}/Tuner
 	${MKDIR_P} ${OBJ_DIR}/Collections
 	${MKDIR_P} ${OBJ_DIR}/Backend