Fully convert ordergraph to objects
authorbdemsky <bdemsky@uci.edu>
Sat, 26 Aug 2017 20:31:58 +0000 (13:31 -0700)
committerbdemsky <bdemsky@uci.edu>
Sat, 26 Aug 2017 20:31:58 +0000 (13:31 -0700)
src/AST/order.cc
src/ASTAnalyses/orderencoder.cc
src/ASTAnalyses/ordergraph.cc
src/ASTAnalyses/ordergraph.h
src/ASTTransform/orderdecompose.cc
src/Backend/satorderencoder.cc
src/classlist.h

index cdc3d52..debd37c 100644 (file)
@@ -39,6 +39,6 @@ Order::~Order() {
                delete elementTable;
        }
        if (graph != NULL) {
-               deleteOrderGraph(graph);
+               delete graph;
        }
 }
index 8eb56ad..919fe18 100644 (file)
@@ -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 ...
-                       OrderEdge *newEdge =getOrderEdgeFromOrderGraph(graph, srcNode, sinkNode);
+                       OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
                        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)){
-                       bypassMustBeTrueNode(This,graph, node);
+                       bypassMustBeTrueNode(This, graph, node);
                }
        }
        delete iterator;
@@ -194,7 +194,7 @@ void completePartialOrderGraph(OrderGraph *graph) {
                                        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;
                                        }
                                }
@@ -252,7 +252,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
                        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)
@@ -322,7 +322,7 @@ void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
        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;
@@ -352,7 +352,7 @@ void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
                        } else
                                solver->unsat = true;
 
-                       OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
+                       OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
                        if (invEdge != NULL) {
                                if (!invEdge->mustPos)
                                        invEdge->polPos = false;
index d81218e..9942b74 100644 (file)
@@ -5,41 +5,38 @@
 #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 *orderGraph = allocOrderGraph(order);
+       OrderGraph *orderGraph = new OrderGraph(order);
        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) {
-       OrderGraph *orderGraph = allocOrderGraph(order);
+       OrderGraph *orderGraph = new OrderGraph(order);
        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;
 }
 
-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;
-       Order *order = graph->order;
        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;
@@ -50,14 +47,14 @@ void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boolean
        }
        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 {
-                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
                        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;
-       Order *order = graph->order;
        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);
@@ -88,13 +84,13 @@ void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boo
        }
        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 {
-                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+                       OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
                        _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 *tmp = graph->nodes->get(node);
+       OrderNode *tmp = nodes->get(node);
        if ( tmp != NULL) {
                delete node;
                node = tmp;
        } else {
-               graph->nodes->add(node);
+               nodes->add(node);
        }
        return node;
 }
 
-OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
+OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
        OrderNode node(id);
-       OrderNode *tmp = graph->nodes->get(&node);
+       OrderNode *tmp = nodes->get(&node);
        return tmp;
 }
 
-OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
+OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *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 {
-               graph->edges->add(edge);
+               edges->add(edge);
        }
        return edge;
 }
 
-OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
+OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
        OrderEdge edge(begin, end);
-       OrderEdge *tmp = graph->edges->get(&edge);
+       OrderEdge *tmp = edges->get(&edge);
        return tmp;
 }
 
-OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
+OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
        OrderEdge inverseedge(edge->sink, edge->source);
-       OrderEdge *tmp = graph->edges->get(&inverseedge);
+       OrderEdge *tmp = edges->get(&inverseedge);
        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;
 
-       HSIteratorOrderEdge *eiterator = graph->edges->iterator();
+       HSIteratorOrderEdge *eiterator = edges->iterator();
        while (eiterator->hasNext()) {
                OrderEdge *edge = eiterator->next();
                delete edge;
        }
        delete eiterator;
-       delete graph->nodes;
-       delete graph->edges;
-       ourfree(graph);
+       delete nodes;
+       delete edges;
 }
index 33f2b69..eba6dbd 100644 (file)
 #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;
 };
 
-OrderGraph *allocOrderGraph(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 */
 
index 1eadffd..7c8e45c 100644 (file)
@@ -54,7 +54,7 @@ void orderAnalysis(CSolver *This) {
                //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)
@@ -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);
-               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) {
-                       OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);                  
+                       OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);                  
                        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) {
-                               OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
+                               OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
                                if (edge->polNeg)
                                        partialcandidatevec.setExpand(from->sccNum, NULL);
                        }
index 6ec1f33..3a3260e 100644 (file)
@@ -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;
-               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)) {
-                       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;
                        }
-                       OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first);
+                       OrderEdge *invedge=graph->lookupOrderEdgeFromOrderGraph(second, first);
                        if (invedge != NULL) {
                                if (invedge->mustPos)
                                        return E_False;
index 993a147..33c1398 100644 (file)
@@ -56,9 +56,7 @@ class OrderEncoding;
 struct TableEntry;
 typedef struct TableEntry TableEntry;
 
-struct OrderGraph;
-typedef struct OrderGraph OrderGraph;
-
+class OrderGraph;
 class OrderNode;
 class OrderEdge;