Bug fixes

[satune.git] / src / ASTTransform / orderdecompose.cc

diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc
index 4962046a0e99685ce36b40480c1e0258add83a49..15c6de61bef29eb4463baa9891500367f30960ce 100644 (file)
--- a/src/ASTTransform/orderdecompose.cc
+++ b/src/ASTTransform/orderdecompose.cc
@@ -9,19 +9,19 @@
 #include "mutableset.h"
 #include "ops.h"
 #include "csolver.h"
-#include "orderencoder.h"
+#include "orderanalysis.h"
 #include "tunable.h"
 #include "integerencoding.h"
 
 void orderAnalysis(CSolver *This) {
-       Vector<Order *> * orders=This->getOrders();
+       Vector<Order *> *orders = This->getOrders();
        uint size = orders->getSize();
        for (uint i = 0; i < size; i++) {
                Order *order = orders->get(i);
-               bool doDecompose=GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff);
+               bool doDecompose = GETVARTUNABLE(This->getTuner(), order->type, DECOMPOSEORDER, &onoff);
                if (!doDecompose)
                        continue;
-               
+
                OrderGraph *graph = buildOrderGraph(order);
                if (order->type == PARTIAL) {
                        //Required to do SCC analysis for partial order graphs.  It
@@ -31,13 +31,13 @@ void orderAnalysis(CSolver *This) {
                }
 
 
-               bool mustReachGlobal=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
+               bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
 
                if (mustReachGlobal)
                        reachMustAnalysis(This, graph, false);
 
-               bool mustReachLocal=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
-               
+               bool mustReachLocal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
+
                if (mustReachLocal) {
                        //This pair of analysis is also optional
                        if (order->type == PARTIAL) {
@@ -47,26 +47,26 @@ void orderAnalysis(CSolver *This) {
                        }
                }
 
-               bool mustReachPrune=GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
-               
+               bool mustReachPrune = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+
                if (mustReachPrune)
                        removeMustBeTrueNodes(This, graph);
-               
+
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
                decomposeOrder(This, order, graph);
                delete graph;
-               
+
                /*
-                       OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need...
+                  OrderIntegerEncodingSATEncoder wants a private field that it really shoukldn't need...
 
-               bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon );
-               if(!doIntegerEncoding)
-                       continue;
-               uint size = order->constraints.getSize();
-               for(uint i=0; i<size; i++){
-                       orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
-                       }*/
+                  bool doIntegerEncoding = GETVARTUNABLE(This->getTuner(), order->order.type, ORDERINTEGERENCODING, &offon );
+                  if(!doIntegerEncoding)
+                  continue;
+                  uint size = order->constraints.getSize();
+                  for(uint i=0; i<size; i++){
+                  orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
+                  }*/
 
        }
 }
@@ -79,9 +79,8 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                BooleanOrder *orderconstraint = order->constraints.get(i);
                OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
                OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
-               model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
                if (from->sccNum != to->sccNum) {
-                       OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);                  
+                       OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
                        if (edge->polPos) {
                                This->replaceBooleanWithTrue(orderconstraint);
                        } else if (edge->polNeg) {
@@ -122,10 +121,10 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                }
        }
 
-       uint pcvsize=partialcandidatevec.getSize();
-       for(uint i=0;i<pcvsize;i++) {
-               Order * neworder=partialcandidatevec.get(i);
-               if (neworder != NULL){
+       uint pcvsize = partialcandidatevec.getSize();
+       for (uint i = 0; i < pcvsize; i++) {
+               Order *neworder = partialcandidatevec.get(i);
+               if (neworder != NULL) {
                        neworder->type = TOTAL;
                        model_print("i=%u\t", i);
                }