Reorg code

diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc
index 06668fd39c4466990c58c63b95924337c31a7397..05e2ae00f22765690b92726b13f3513cf5de0102 100644 (file)
--- 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 ad050bb7ac33e380c1ae2a6fcd957c65e58eb553..fa3089fccd9cde7fc4951c393779921ab905b792 100644 (file)
--- 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 (file)
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 (file)
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 c91f8ffb31b71bef04988b7cdd60fcd3fe7a5740..b88fdede56e8491d841f990c61a1d18124ca7c8a 100644 (file)
--- 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 43c780bf29d8ccc87244dbc639383c4add02481e..cdbb919eac5c48fb80bbeab7fc259de3907b2a34 100644 (file)
--- 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);