Fully convert ordergraph to objects

diff --git a/src/AST/order.cc b/src/AST/order.cc
index cdc3d52c9efdea7d98d21002dccc4a6e2b183745..debd37cf69defe4107d34c8091a69c1f9d214a16 100644 (file)
--- a/src/AST/order.cc
+++ b/src/AST/order.cc
@@ -39,6 +39,6 @@ Order::~Order() {
                delete elementTable;
        }
        if (graph != NULL) {
                delete elementTable;
        }
        if (graph != NULL) {

-               deleteOrderGraph(graph);
+               delete graph;

        }
 }
        }
 }

diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc
index 8eb56adf664559a58d33cb23f3b3a2fd690f2cbf..919fe1843f95e5ca9312d2fdfa01d27b3c5fc588 100644 (file)
--- a/src/ASTAnalyses/orderencoder.cc
+++ b/src/ASTAnalyses/orderencoder.cc
@@ -110,7 +110,7 @@ void bypassMustBeTrueNode(CSolver *This, OrderGraph* graph, OrderNode* node){
                        OrderNode* sinkNode = outEdge->sink;
                        sinkNode->inEdges.remove(outEdge);
                        //Adding new edge to new sink and src nodes ...
                        OrderNode* sinkNode = outEdge->sink;
                        sinkNode->inEdges.remove(outEdge);
                        //Adding new edge to new sink and src nodes ...

-                       OrderEdge *newEdge =getOrderEdgeFromOrderGraph(graph, srcNode, sinkNode);
+                       OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);

                        newEdge->mustPos = true;
                        newEdge->polPos = true;
                        if (newEdge->mustNeg)
                        newEdge->mustPos = true;
                        newEdge->polPos = true;
                        if (newEdge->mustNeg)


@@ -128,7 +128,7 @@ void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) {
        while(iterator->hasNext()) {
                OrderNode* node = iterator->next();
                if(isMustBeTrueNode(node)){
        while(iterator->hasNext()) {
                OrderNode* node = iterator->next();
                if(isMustBeTrueNode(node)){

-                       bypassMustBeTrueNode(This,graph, node);
+                       bypassMustBeTrueNode(This, graph, node);

                }
        }
        delete iterator;
                }
        }
        delete iterator;


@@ -194,7 +194,7 @@ void completePartialOrderGraph(OrderGraph *graph) {
                                        ASSERT(parent != rnode);
                                        if (edge->polNeg && parent->sccNum != rnode->sccNum &&
                                                        sources->contains(parent)) {
                                        ASSERT(parent != rnode);
                                        if (edge->polNeg && parent->sccNum != rnode->sccNum &&
                                                        sources->contains(parent)) {

-                                               OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, rnode, parent);
+                                               OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);

                                                newedge->pseudoPos = true;
                                        }
                                }
                                                newedge->pseudoPos = true;
                                        }
                                }


@@ -252,7 +252,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                        HSIteratorOrderNode *srciterator = sources->iterator();
                        while (srciterator->hasNext()) {
                                OrderNode *srcnode = srciterator->next();
                        HSIteratorOrderNode *srciterator = sources->iterator();
                        while (srciterator->hasNext()) {
                                OrderNode *srcnode = srciterator->next();

-                               OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
+                               OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);

                                newedge->mustPos = true;
                                newedge->polPos = true;
                                if (newedge->mustNeg)
                                newedge->mustPos = true;
                                newedge->polPos = true;
                                if (newedge->mustNeg)


@@ -322,7 +322,7 @@ void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
        while (iterator->hasNext()) {
                OrderEdge *edge = iterator->next();
                if (edge->mustPos) {
        while (iterator->hasNext()) {
                OrderEdge *edge = iterator->next();
                if (edge->mustPos) {

-                       OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
+                       OrderEdge *invEdge = graph->getInverseOrderEdge(edge);

                        if (invEdge != NULL) {
                                if (!invEdge->mustPos) {
                                        invEdge->polPos = false;
                        if (invEdge != NULL) {
                                if (!invEdge->mustPos) {
                                        invEdge->polPos = false;


@@ -352,7 +352,7 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
                        } else
                                solver->unsat = true;
 
                        } else
                                solver->unsat = true;
 

-                       OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
+                       OrderEdge *invEdge = graph->getInverseOrderEdge(edge);

                        if (invEdge != NULL) {
                                if (!invEdge->mustPos)
                                        invEdge->polPos = false;
                        if (invEdge != NULL) {
                                if (!invEdge->mustPos)
                                        invEdge->polPos = false;

diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc
index d81218e7e514e37c7fb2f40eafeece31f2c61cf9..9942b740fec5ee4841fd351de943231aa94f1528 100644 (file)
--- a/src/ASTAnalyses/ordergraph.cc
+++ b/src/ASTAnalyses/ordergraph.cc
@@ -5,41 +5,38 @@
 #include "ordergraph.h"
 #include "order.h"
 
 #include "ordergraph.h"
 #include "order.h"
 

-OrderGraph *allocOrderGraph(Order *order) {
-       OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
-       This->nodes = new HashSetOrderNode();
-       This->edges = new HashSetOrderEdge();
-       This->order = order;
-       return This;
+OrderGraph::OrderGraph(Order *_order) :
+       nodes(new HashSetOrderNode()),
+       edges(new HashSetOrderEdge()),
+       order(_order) {

 }
 
 OrderGraph *buildOrderGraph(Order *order) {
 }
 
 OrderGraph *buildOrderGraph(Order *order) {

-       OrderGraph *orderGraph = allocOrderGraph(order);
+       OrderGraph *orderGraph = new OrderGraph(order);

        uint constrSize = order->constraints.getSize();
        for (uint j = 0; j < constrSize; j++) {
        uint constrSize = order->constraints.getSize();
        for (uint j = 0; j < constrSize; j++) {

-               addOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
+               orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));

        }
        return orderGraph;
 }
 
 //Builds only the subgraph for the must order graph.
 OrderGraph *buildMustOrderGraph(Order *order) {
        }
        return orderGraph;
 }
 
 //Builds only the subgraph for the must order graph.
 OrderGraph *buildMustOrderGraph(Order *order) {

-       OrderGraph *orderGraph = allocOrderGraph(order);
+       OrderGraph *orderGraph = new OrderGraph(order);

        uint constrSize = order->constraints.getSize();
        for (uint j = 0; j < constrSize; j++) {
        uint constrSize = order->constraints.getSize();
        for (uint j = 0; j < constrSize; j++) {

-               addMustOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
+               orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));

        }
        return orderGraph;
 }
 
        }
        return orderGraph;
 }
 

-void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {

        Polarity polarity = constr->polarity;
        BooleanValue mustval = constr->boolVal;
        Polarity polarity = constr->polarity;
        BooleanValue mustval = constr->boolVal;

-       Order *order = graph->order;

        switch (polarity) {
        case P_BOTHTRUEFALSE:
        case P_TRUE: {
        switch (polarity) {
        case P_BOTHTRUEFALSE:
        case P_TRUE: {

-               OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+               OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);

                if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
                        _1to2->mustPos = true;
                _1to2->polPos = true;
                if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
                        _1to2->mustPos = true;
                _1to2->polPos = true;


@@ -50,14 +47,14 @@ void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boolean
        }
        case P_FALSE: {
                if (order->type == TOTAL) {
        }
        case P_FALSE: {
                if (order->type == TOTAL) {

-                       OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+                       OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);

                        if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
                                _2to1->mustPos = true;
                        _2to1->polPos = true;
                        node2->addNewOutgoingEdge(_2to1);
                        node1->addNewIncomingEdge(_2to1);
                } else {
                        if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
                                _2to1->mustPos = true;
                        _2to1->polPos = true;
                        node2->addNewOutgoingEdge(_2to1);
                        node1->addNewIncomingEdge(_2to1);
                } else {

-                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);

                        if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
                                _1to2->mustNeg = true;
                        _1to2->polNeg = true;
                        if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
                                _1to2->mustNeg = true;
                        _1to2->polNeg = true;


@@ -72,13 +69,12 @@ void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boolean
        }
 }
 
        }
 }
 

-void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {

        BooleanValue mustval = constr->boolVal;
        BooleanValue mustval = constr->boolVal;

-       Order *order = graph->order;

        switch (mustval) {
        case BV_UNSAT:
        case BV_MUSTBETRUE: {
        switch (mustval) {
        case BV_UNSAT:
        case BV_MUSTBETRUE: {

-               OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+               OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);

                _1to2->mustPos = true;
                _1to2->polPos = true;
                node1->addNewOutgoingEdge(_1to2);
                _1to2->mustPos = true;
                _1to2->polPos = true;
                node1->addNewOutgoingEdge(_1to2);


@@ -88,13 +84,13 @@ void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boo
        }
        case BV_MUSTBEFALSE: {
                if (order->type == TOTAL) {
        }
        case BV_MUSTBEFALSE: {
                if (order->type == TOTAL) {

-                       OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+                       OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);

                        _2to1->mustPos = true;
                        _2to1->polPos = true;
                        node2->addNewOutgoingEdge(_2to1);
                        node1->addNewIncomingEdge(_2to1);
                } else {
                        _2to1->mustPos = true;
                        _2to1->polPos = true;
                        node2->addNewOutgoingEdge(_2to1);
                        node1->addNewIncomingEdge(_2to1);
                } else {

-                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);

                        _1to2->mustNeg = true;
                        _1to2->polNeg = true;
                        node1->addNewOutgoingEdge(_1to2);
                        _1to2->mustNeg = true;
                        _1to2->polNeg = true;
                        node1->addNewOutgoingEdge(_1to2);


@@ -108,75 +104,74 @@ void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boo
        }
 }
 
        }
 }
 

-OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
+OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {

        OrderNode *node = new OrderNode(id);
        OrderNode *node = new OrderNode(id);

-       OrderNode *tmp = graph->nodes->get(node);
+       OrderNode *tmp = nodes->get(node);

        if ( tmp != NULL) {
                delete node;
                node = tmp;
        } else {
        if ( tmp != NULL) {
                delete node;
                node = tmp;
        } else {

-               graph->nodes->add(node);
+               nodes->add(node);

        }
        return node;
 }
 
        }
        return node;
 }
 

-OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
+OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {

        OrderNode node(id);
        OrderNode node(id);

-       OrderNode *tmp = graph->nodes->get(&node);
+       OrderNode *tmp = nodes->get(&node);

        return tmp;
 }
 
        return tmp;
 }
 

-OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
+OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {

        OrderEdge *edge = new OrderEdge(begin, end);
        OrderEdge *edge = new OrderEdge(begin, end);

-       OrderEdge *tmp = graph->edges->get(edge);
+       OrderEdge *tmp = edges->get(edge);

        if ( tmp != NULL ) {
                delete edge;
                edge = tmp;
        } else {
        if ( tmp != NULL ) {
                delete edge;
                edge = tmp;
        } else {

-               graph->edges->add(edge);
+               edges->add(edge);

        }
        return edge;
 }
 
        }
        return edge;
 }
 

-OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
+OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {

        OrderEdge edge(begin, end);
        OrderEdge edge(begin, end);

-       OrderEdge *tmp = graph->edges->get(&edge);
+       OrderEdge *tmp = edges->get(&edge);

        return tmp;
 }
 
        return tmp;
 }
 

-OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
+OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {

        OrderEdge inverseedge(edge->sink, edge->source);
        OrderEdge inverseedge(edge->sink, edge->source);

-       OrderEdge *tmp = graph->edges->get(&inverseedge);
+       OrderEdge *tmp = edges->get(&inverseedge);

        return tmp;
 }
 
        return tmp;
 }
 

-void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
-       OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
-       OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
-       addOrderEdge(graph, from, to, bOrder);
+void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
+       OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
+       OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
+       addOrderEdge(from, to, bOrder);

 }
 
 }
 

-void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
-       OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
-       OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
-       addMustOrderEdge(graph, from, to, bOrder);
+void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
+       OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
+       OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
+       addMustOrderEdge(from, to, bOrder);

 }
 
 }
 

-void deleteOrderGraph(OrderGraph *graph) {
-       HSIteratorOrderNode *iterator = graph->nodes->iterator();
+OrderGraph::~OrderGraph() {
+       HSIteratorOrderNode *iterator = nodes->iterator();

        while (iterator->hasNext()) {
                OrderNode *node = iterator->next();
                delete node;
        }
        delete iterator;
 
        while (iterator->hasNext()) {
                OrderNode *node = iterator->next();
                delete node;
        }
        delete iterator;
 

-       HSIteratorOrderEdge *eiterator = graph->edges->iterator();
+       HSIteratorOrderEdge *eiterator = edges->iterator();

        while (eiterator->hasNext()) {
                OrderEdge *edge = eiterator->next();
                delete edge;
        }
        delete eiterator;
        while (eiterator->hasNext()) {
                OrderEdge *edge = eiterator->next();
                delete edge;
        }
        delete eiterator;

-       delete graph->nodes;
-       delete graph->edges;
-       ourfree(graph);
+       delete nodes;
+       delete edges;

 }
 }

diff --git a/src/ASTAnalyses/ordergraph.h b/src/ASTAnalyses/ordergraph.h
index 33f2b69cab59121f7e0033c0a3d44e2b6ba12d4d..eba6dbdeb615cd090828f53217d77b0cece45643 100644 (file)
--- a/src/ASTAnalyses/ordergraph.h
+++ b/src/ASTAnalyses/ordergraph.h
@@ -11,24 +11,25 @@
 #include "structs.h"
 #include "mymemory.h"
 
 #include "structs.h"
 #include "mymemory.h"
 

-struct OrderGraph {
+class OrderGraph {
+ public:
+       OrderGraph(Order *order);
+       ~OrderGraph();
+       void addOrderConstraintToOrderGraph(BooleanOrder *bOrder);
+       void addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder);
+       OrderNode *getOrderNodeFromOrderGraph(uint64_t id);
+       OrderEdge *getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
+       OrderNode *lookupOrderNodeFromOrderGraph(uint64_t id);
+       OrderEdge *lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
+       void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+       void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+       OrderEdge *getInverseOrderEdge(OrderEdge *edge);

        HashSetOrderNode *nodes;
        HashSetOrderEdge *edges;
        Order *order;
 };
 
        HashSetOrderNode *nodes;
        HashSetOrderEdge *edges;
        Order *order;
 };
 

-OrderGraph *allocOrderGraph(Order *order);

 OrderGraph *buildOrderGraph(Order *order);
 OrderGraph *buildMustOrderGraph(Order *order);
 OrderGraph *buildOrderGraph(Order *order);
 OrderGraph *buildMustOrderGraph(Order *order);

-void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
-void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
-OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
-OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
-OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
-OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
-void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
-void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
-void deleteOrderGraph(OrderGraph *graph);
-OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge);

 #endif/* ORDERGRAPH_H */
 
 #endif/* ORDERGRAPH_H */
 

diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc
index 1eadffd71058cd925ebff6f1fd84c075c94de17f..7c8e45c88655341f852fe4eadea131d09345fb2a 100644 (file)
--- a/src/ASTTransform/orderdecompose.cc
+++ b/src/ASTTransform/orderdecompose.cc
@@ -54,7 +54,7 @@ void orderAnalysis(CSolver *This) {
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
                decomposeOrder(This, order, graph);
                //This is needed for splitorder
                computeStronglyConnectedComponentGraph(graph);
                decomposeOrder(This, order, graph);

-               deleteOrderGraph(graph);
+               delete graph;

                
                bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &offon );
                if(!doIntegerEncoding)
                
                bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &offon );
                if(!doIntegerEncoding)


@@ -73,11 +73,11 @@ 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);
        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);
+               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) {
                model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
                if (from->sccNum != to->sccNum) {

-                       OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);                  
+                       OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);                  

                        if (edge->polPos) {
                                replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
                        } else if (edge->polNeg) {
                        if (edge->polPos) {
                                replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
                        } else if (edge->polNeg) {


@@ -111,7 +111,7 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                                ((MutableSet *)neworder->set)->addElementMSet(to->id);
                        }
                        if (order->type == PARTIAL) {
                                ((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);
                        }
                                if (edge->polNeg)
                                        partialcandidatevec.setExpand(from->sccNum, NULL);
                        }

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 6ec1f33f3e38c4e2592eb67a82e16c45142e44c9..3a3260e7bddb7f3d91bb92a7d8fc2ce976525d3a 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -28,17 +28,17 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
 Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
        if (order->graph != NULL) {
                OrderGraph *graph=order->graph;
 Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
        if (order->graph != NULL) {
                OrderGraph *graph=order->graph;

-               OrderNode *first=lookupOrderNodeFromOrderGraph(graph, _first);
-               OrderNode *second=lookupOrderNodeFromOrderGraph(graph, _second);
+               OrderNode *first=graph->lookupOrderNodeFromOrderGraph(_first);
+               OrderNode *second=graph->lookupOrderNodeFromOrderGraph(_second);

                if ((first != NULL) && (second != NULL)) {
                if ((first != NULL) && (second != NULL)) {

-                       OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
+                       OrderEdge *edge=graph->lookupOrderEdgeFromOrderGraph(first, second);

                        if (edge != NULL) {
                                if (edge->mustPos)
                                        return E_True;
                                else if (edge->mustNeg)
                                        return E_False;
                        }
                        if (edge != NULL) {
                                if (edge->mustPos)
                                        return E_True;
                                else if (edge->mustNeg)
                                        return E_False;
                        }

-                       OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first);
+                       OrderEdge *invedge=graph->lookupOrderEdgeFromOrderGraph(second, first);

                        if (invedge != NULL) {
                                if (invedge->mustPos)
                                        return E_False;
                        if (invedge != NULL) {
                                if (invedge->mustPos)
                                        return E_False;

diff --git a/src/classlist.h b/src/classlist.h
index 993a14733bfb0590d3bdd055c7e2295e65c57351..33c1398a9f54072137a99caf1e693f069541b2b2 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -56,9 +56,7 @@ class OrderEncoding;
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 

-struct OrderGraph;
-typedef struct OrderGraph OrderGraph;
-
+class OrderGraph;

 class OrderNode;
 class OrderEdge;
 
 class OrderNode;
 class OrderEdge;