Bug fixes

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

diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc
index 59b6ebc600a4737d02e1937fa2fe62e176e2b5f1..15c6de61bef29eb4463baa9891500367f30960ce 100644 (file)
--- a/src/ASTTransform/orderdecompose.cc
+++ b/src/ASTTransform/orderdecompose.cc
@@ -9,17 +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) {
-       uint size = This->allOrders.getSize();
+       Vector<Order *> *orders = This->getOrders();
+       uint size = orders->getSize();
        for (uint i = 0; i < size; i++) {
-               Order *order = This->allOrders.get(i);
-               bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
+               Order *order = orders->get(i);
+               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
@@ -29,13 +31,13 @@ void orderAnalysis(CSolver *This) {
                }
 
 
-               bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
+               bool mustReachGlobal = GETVARTUNABLE(This->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
 
                if (mustReachGlobal)
                        reachMustAnalysis(This, graph, false);
 
-               bool mustReachLocal=GETVARTUNABLE(This->tuner, 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) {
@@ -45,17 +47,27 @@ void orderAnalysis(CSolver *This) {
                        }
                }
 
-               bool mustReachPrune=GETVARTUNABLE(This->tuner, 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);
-               
-               deleteOrderGraph(graph);
+               delete graph;
+
+               /*
+                  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));
+                  }*/
+
        }
 }
 
@@ -65,15 +77,14 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
        uint size = order->constraints.getSize();
        for (uint i = 0; i < size; i++) {
                BooleanOrder *orderconstraint = order->constraints.get(i);
-               OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
-               OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
-               model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
+               OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
+               OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
                if (from->sccNum != to->sccNum) {
-                       OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);                  
+                       OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
                        if (edge->polPos) {
-                               replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
+                               This->replaceBooleanWithTrue(orderconstraint);
                        } else if (edge->polNeg) {
-                               replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
+                               This->replaceBooleanWithFalse(orderconstraint);
                        } else {
                                //This case should only be possible if constraint isn't in AST
                                ASSERT(0);
@@ -84,9 +95,8 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                        if (ordervec.getSize() > from->sccNum)
                                neworder = ordervec.get(from->sccNum);
                        if (neworder == NULL) {
-                               MutableSet *set = new MutableSet(order->set->type);
-                               neworder = new Order(order->type, set);
-                               This->allOrders.push(neworder);
+                               MutableSet *set = This->createMutableSet(order->set->type);
+                               neworder = This->createOrder(order->type, set);
                                ordervec.setExpand(from->sccNum, neworder);
                                if (order->type == PARTIAL)
                                        partialcandidatevec.setExpand(from->sccNum, neworder);
@@ -102,7 +112,7 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                                ((MutableSet *)neworder->set)->addElementMSet(to->id);
                        }
                        if (order->type == PARTIAL) {
-                               OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
+                               OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
                                if (edge->polNeg)
                                        partialcandidatevec.setExpand(from->sccNum, NULL);
                        }
@@ -111,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);
                }