From: bdemsky Date: Sat, 26 Aug 2017 20:31:58 +0000 (-0700) Subject: Fully convert ordergraph to objects X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=574767abf9fc7095bb2418e797dbefe90990510d Fully convert ordergraph to objects --- diff --git a/src/AST/order.cc b/src/AST/order.cc index cdc3d52..debd37c 100644 --- a/src/AST/order.cc +++ b/src/AST/order.cc @@ -39,6 +39,6 @@ Order::~Order() { delete elementTable; } if (graph != NULL) { - deleteOrderGraph(graph); + delete graph; } } diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc index 8eb56ad..919fe18 100644 --- 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 ... - 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, Vectoriterator(); 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; diff --git a/src/ASTAnalyses/ordergraph.cc b/src/ASTAnalyses/ordergraph.cc index d81218e..9942b74 100644 --- a/src/ASTAnalyses/ordergraph.cc +++ b/src/ASTAnalyses/ordergraph.cc @@ -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; } diff --git a/src/ASTAnalyses/ordergraph.h b/src/ASTAnalyses/ordergraph.h index 33f2b69..eba6dbd 100644 --- a/src/ASTAnalyses/ordergraph.h +++ b/src/ASTAnalyses/ordergraph.h @@ -11,24 +11,25 @@ #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 */ diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc index 1eadffd..7c8e45c 100644 --- 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); - 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); } diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index 6ec1f33..3a3260e 100644 --- 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; - 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; diff --git a/src/classlist.h b/src/classlist.h index 993a147..33c1398 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -56,9 +56,7 @@ class OrderEncoding; struct TableEntry; typedef struct TableEntry TableEntry; -struct OrderGraph; -typedef struct OrderGraph OrderGraph; - +class OrderGraph; class OrderNode; class OrderEdge;