X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FASTTransform%2Fdecomposeordertransform.cc;h=3791b100fe6358f0ee39b3e2cce90a4410408526;hb=533b3ebef5176bdabe3e6dea4d384a5d1640dbad;hp=262497e257b0060ef0a26675def7b6b10b1425bf;hpb=6aa24e6f78c78f5ccccf00980b7e76a201bead86;p=satune.git

diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 262497e..3791b10 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -1,7 +1,7 @@
-/* 
+/*
  * File:   ordertransform.cc
  * Author: hamed
- * 
+ *
  * Created on August 28, 2017, 10:35 AM
  */
 
@@ -13,21 +13,69 @@
 #include "mutableset.h"
 #include "ordergraph.h"
 #include "csolver.h"
+#include "decomposeorderresolver.h"
+#include "tunable.h"
+#include "orderanalysis.h"
 
 
-DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver)
-	:Transform(_solver)
+DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
+	: Transform(_solver)
 {
 }
 
 DecomposeOrderTransform::~DecomposeOrderTransform() {
 }
 
-bool DecomposeOrderTransform::canExecuteTransform(){
-	return canExecutePass(solver, currOrder->type, DECOMPOSEORDER, &onoff);
+void DecomposeOrderTransform::doTransform() {
+	HashsetOrder *orders = solver->getActiveOrders()->copy();
+	SetIteratorOrder * orderit=orders->iterator();
+	while(orderit->hasNext()) {
+		Order *order = orderit->next();
+
+		if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
+			continue;
+		}
+
+		OrderGraph *graph = buildOrderGraph(order);
+		if (order->type == SATC_PARTIAL) {
+			//Required to do SCC analysis for partial order graphs.  It
+			//makes sure we don't incorrectly optimize graphs with negative
+			//polarity edges
+			completePartialOrderGraph(graph);
+		}
+
+		bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
+
+		if (mustReachGlobal)
+			reachMustAnalysis(solver, graph, false);
+
+		bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
+
+		if (mustReachLocal) {
+			//This pair of analysis is also optional
+			if (order->type == SATC_PARTIAL) {
+				localMustAnalysisPartial(solver, graph);
+			} else {
+				localMustAnalysisTotal(solver, graph);
+			}
+		}
+
+		
+		bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+
+		if (mustReachPrune)
+			removeMustBeTrueNodes(solver, graph);
+		
+		//This is needed for splitorder
+		computeStronglyConnectedComponentGraph(graph);
+		decomposeOrder(order, graph);
+	}
+	delete orderit;
+	delete orders;
 }
 
-void DecomposeOrderTransform::doTransform(){
+
+void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) {
 	Vector<Order *> ordervec;
 	Vector<Order *> partialcandidatevec;
 	uint size = currOrder->constraints.getSize();
@@ -35,16 +83,34 @@ void DecomposeOrderTransform::doTransform(){
 		BooleanOrder *orderconstraint = currOrder->constraints.get(i);
 		OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
 		OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
-		model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
 		if (from->sccNum != to->sccNum) {
-			OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
-			if (edge->polPos) {
-				solver->replaceBooleanWithTrue(orderconstraint);
-			} else if (edge->polNeg) {
-				solver->replaceBooleanWithFalse(orderconstraint);
+			OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
+			if (edge != NULL) {
+				if (edge->polPos) {
+					solver->replaceBooleanWithTrue(orderconstraint);
+				} else if (edge->polNeg) {
+					solver->replaceBooleanWithFalse(orderconstraint);
+				} else {
+					//This case should only be possible if constraint isn't in AST
+					//This can happen, so don't do anything
+					;
+				}
 			} else {
-				//This case should only be possible if constraint isn't in AST
-				ASSERT(0);
+				OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
+				if (invedge != NULL) {
+					if (invedge->polPos) {
+						solver->replaceBooleanWithFalse(orderconstraint);
+					} else if (edge->polNeg) {
+						//This case shouldn't happen...  If we have a partial order,
+						//then we should have our own edge...If we have a total
+						//order, then this edge should be positive...
+						ASSERT(0);
+					} else {
+						//This case should only be possible if constraint isn't in AST
+						//This can happen, so don't do anything
+						;
+					}
+				}
 			}
 		} else {
 			//Build new order and change constraint's order
@@ -77,13 +143,13 @@ void DecomposeOrderTransform::doTransform(){
 			neworder->addOrderConstraint(orderconstraint);
 		}
 	}
-
+	currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
+	solver->getActiveOrders()->remove(currOrder);
 	uint pcvsize = partialcandidatevec.getSize();
 	for (uint i = 0; i < pcvsize; i++) {
 		Order *neworder = partialcandidatevec.get(i);
 		if (neworder != NULL) {
 			neworder->type = SATC_TOTAL;
-			model_print("i=%u\t", i);
 		}
 	}
 }