From: bdemsky <bdemsky@uci.edu>
Date: Fri, 25 Aug 2017 23:08:08 +0000 (-0700)
Subject: Reorg code
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c0e8b50c4010f03bec0d733ec3e677ce090577ba;p=satune.git

Reorg code
---

diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc
index 06668fd..05e2ae0 100644
--- a/src/ASTAnalyses/orderencoder.cc
+++ b/src/ASTAnalyses/orderencoder.cc
@@ -368,44 +368,3 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
 	}
 	delete iterator;
 }
-
-void orderAnalysis(CSolver *This) {
-	uint size = This->allOrders.getSize();
-	for (uint i = 0; i < size; i++) {
-		Order *order = This->allOrders.get(i);
-		
-		OrderGraph *graph;
-		if(order->graph == NULL){
-			graph= buildOrderGraph(order);
-			if (order->type == 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);
-			}
-		}else
-			graph = order->graph;
-		
-		bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
-
-		if (mustReachGlobal)
-			reachMustAnalysis(This, graph, false);
-
-		bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
-		
-		if (mustReachLocal) {
-			//This pair of analysis is also optional
-			if (order->type == PARTIAL) {
-				localMustAnalysisPartial(This, graph);
-			} else {
-				localMustAnalysisTotal(This, graph);
-			}
-		}
-
-		bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
-		
-		if (mustReachPrune)
-			removeMustBeTrueNodes(This, graph);
-		
-	}
-}
diff --git a/src/ASTAnalyses/orderencoder.h b/src/ASTAnalyses/orderencoder.h
index ad050bb..fa3089f 100644
--- a/src/ASTAnalyses/orderencoder.h
+++ b/src/ASTAnalyses/orderencoder.h
@@ -28,8 +28,6 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure);
 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph);
 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph);
-void orderAnalysis(CSolver *This);
-void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
 
 #endif/* ORDERGRAPHBUILDER_H */
 
diff --git a/src/ASTTransform/asttransform.cc b/src/ASTTransform/asttransform.cc
deleted file mode 100644
index 15b351a..0000000
--- a/src/ASTTransform/asttransform.cc
+++ /dev/null
@@ -1,45 +0,0 @@
-#include "asttransform.h"
-#include "order.h"
-#include "tunable.h"
-#include "csolver.h"
-#include "ordergraph.h"
-#include "orderencoder.h"
-#include "orderdecompose.h"
-#include "integerencoding.h"
-
-void ASTTransform(CSolver *This){
-	uint size = This->allOrders.getSize();
-	for (uint i = 0; i < size; i++) {
-		Order *order = This->allOrders.get(i);
-		bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
-		if (!doDecompose)
-			continue;
-		
-		OrderGraph *graph;
-		if(order->graph == NULL){
-			graph= buildOrderGraph(order);
-			if (order->type == 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);
-			}
-		}else{
-			graph = order->graph;
-		}		
-		//This is needed for splitorder
-		computeStronglyConnectedComponentGraph(graph);
-		decomposeOrder(This, order, graph);
-		
-		bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &onoff );
-		if(!doIntegerEncoding)
-			continue;
-		uint size = order->constraints.getSize();
-		for(uint i=0; i<size; i++){
-			orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
-		}
-	}
-	
-	
-}
-
diff --git a/src/ASTTransform/asttransform.h b/src/ASTTransform/asttransform.h
deleted file mode 100644
index f6482ea..0000000
--- a/src/ASTTransform/asttransform.h
+++ /dev/null
@@ -1,21 +0,0 @@
-/*
- * To change this license header, choose License Headers in Project Properties.
- * To change this template file, choose Tools | Templates
- * and open the template in the editor.
- */
-
-/* 
- * File:   asttransform.h
- * Author: hamed
- *
- * Created on August 24, 2017, 5:48 PM
- */
-
-#ifndef ASTTRANSFORM_H
-#define ASTTRANSFORM_H
-#include "classlist.h"
-
-void ASTTransform(CSolver *This); 
-
-#endif /* ASTTRANSFORM_H */
-
diff --git a/src/ASTTransform/orderdecompose.h b/src/ASTTransform/orderdecompose.h
index c91f8ff..b88fded 100644
--- a/src/ASTTransform/orderdecompose.h
+++ b/src/ASTTransform/orderdecompose.h
@@ -16,6 +16,7 @@
 #include "classlist.h"
 #include "structs.h"
 
+void orderAnalysis(CSolver *This);
 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph);
 
 #endif /* ORDERDECOMPOSE_H */
diff --git a/src/csolver.cc b/src/csolver.cc
index 43c780b..cdbb919 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -10,9 +10,8 @@
 #include "satencoder.h"
 #include "sattranslator.h"
 #include "tunable.h"
-#include "orderencoder.h"
 #include "polarityassignment.h"
-#include "asttransform.h"
+#include "orderdecompose.h"
 
 CSolver::CSolver() : unsat(false) {
 	tuner = allocTuner();
@@ -183,9 +182,8 @@ Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second)
 
 int CSolver::startEncoding() {
 	computePolarities(this);
-	ASTTransform(this);
-	naiveEncodingDecision(this);
 	orderAnalysis(this);
+	naiveEncodingDecision(this);
 	encodeAllSATEncoder(this, satEncoder);
 	int result = solveCNF(satEncoder->cnf);
 	model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize);