Try to fix encapsulation

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

diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc
index 7c8e45c88655341f852fe4eadea131d09345fb2a..4962046a0e99685ce36b40480c1e0258add83a49 100644 (file)
--- a/src/ASTTransform/orderdecompose.cc
+++ b/src/ASTTransform/orderdecompose.cc
@@ -14,10 +14,11 @@
 #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;
                
@@ -30,12 +31,12 @@ 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
@@ -46,7 +47,7 @@ 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);
@@ -56,13 +57,16 @@ void orderAnalysis(CSolver *This) {
                decomposeOrder(This, order, graph);
                delete graph;
                
-               bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &offon );
+               /*
+                       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));
-               }
+                       }*/
 
        }
 }
@@ -79,9 +83,9 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                if (from->sccNum != to->sccNum) {
                        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);
@@ -92,10 +96,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);
-                               This->allSets.push(set);
-                               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);