1 #include "ordergraph.h"
5 #include "ordergraph.h"
8 OrderGraph::OrderGraph(Order *_order) :
12 OrderGraph *buildOrderGraph(Order *order) {
13 ASSERT(order->graph == NULL);
14 OrderGraph *orderGraph = new OrderGraph(order);
15 uint constrSize = order->constraints.getSize();
16 for (uint j = 0; j < constrSize; j++) {
17 orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
22 //Builds only the subgraph for the must order graph.
23 OrderGraph *buildMustOrderGraph(Order *order) {
24 ASSERT(order->graph == NULL);
25 OrderGraph *orderGraph = new OrderGraph(order);
26 uint constrSize = order->constraints.getSize();
27 for (uint j = 0; j < constrSize; j++) {
28 orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
33 void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
34 Polarity polarity = constr->polarity;
35 BooleanValue mustval = constr->boolVal;
39 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
40 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
41 _1to2->mustPos = true;
43 node1->addNewOutgoingEdge(_1to2);
44 node2->addNewIncomingEdge(_1to2);
45 if (constr->polarity == P_TRUE)
49 if (order->type == SATC_TOTAL) {
50 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
51 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
52 _2to1->mustPos = true;
54 node2->addNewOutgoingEdge(_2to1);
55 node1->addNewIncomingEdge(_2to1);
57 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
58 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
59 _1to2->mustNeg = true;
61 node1->addNewOutgoingEdge(_1to2);
62 node2->addNewIncomingEdge(_1to2);
67 //There is an unreachable order constraint if this assert fires
68 //Clients can easily do this, so don't do anything.
73 void OrderGraph::addEdge(uint64_t first, uint64_t second) {
74 OrderNode *node1 = getOrderNodeFromOrderGraph(first);
75 OrderNode *node2 = getOrderNodeFromOrderGraph(second);
76 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
78 _1to2->mustPos = true;
79 node1->addNewOutgoingEdge(_1to2);
80 node2->addNewIncomingEdge(_1to2);
83 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
84 BooleanValue mustval = constr->boolVal;
88 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
89 _1to2->mustPos = true;
91 node1->addNewOutgoingEdge(_1to2);
92 node2->addNewIncomingEdge(_1to2);
93 if (constr->boolVal == BV_MUSTBETRUE)
96 case BV_MUSTBEFALSE: {
97 if (order->type == SATC_TOTAL) {
98 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
99 _2to1->mustPos = true;
100 _2to1->polPos = true;
101 node2->addNewOutgoingEdge(_2to1);
102 node1->addNewIncomingEdge(_2to1);
104 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
105 _1to2->mustNeg = true;
106 _1to2->polNeg = true;
107 node1->addNewOutgoingEdge(_1to2);
108 node2->addNewIncomingEdge(_1to2);
118 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
119 OrderNode *node = new OrderNode(id);
120 OrderNode *tmp = (OrderNode *)nodes.get(node);
130 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
131 OrderNodeKey node(id);
132 OrderNode *tmp = (OrderNode *)nodes.get(&node);
136 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
137 OrderEdge *edge = new OrderEdge(begin, end);
138 OrderEdge *tmp = edges.get(edge);
148 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
149 OrderEdge edge(begin, end);
150 OrderEdge *tmp = edges.get(&edge);
154 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
155 OrderEdge inverseedge(edge->sink, edge->source);
156 OrderEdge *tmp = edges.get(&inverseedge);
160 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
161 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
162 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
163 addOrderEdge(from, to, bOrder);
166 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
167 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
168 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
169 addMustOrderEdge(from, to, bOrder);
172 OrderGraph::~OrderGraph() {
173 nodes.resetAndDelete();
174 edges.resetAndDelete();
177 bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
178 HashsetOrderNode visited;
180 SetIteratorOrderEdge *iterator = source->outEdges.iterator();
182 while (iterator->hasNext()) {
183 OrderEdge *edge = iterator->next();
185 OrderNode *node = edge->sink;
186 if (!visited.contains(node)) {
187 if ( node == destination ) {
192 found = isTherePathVisit(visited, node, destination);
203 bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination) {
204 SetIteratorOrderEdge *iterator = current->outEdges.iterator();
206 while (iterator->hasNext()) {
207 OrderEdge *edge = iterator->next();
209 OrderNode *node = edge->sink;
210 if (node == destination) {
215 if (isTherePathVisit(visited, node, destination)) {
225 void OrderGraph::DFS(Vector<OrderNode *> *finishNodes) {
226 SetIteratorOrderNode *iterator = getNodes();
227 while (iterator->hasNext()) {
228 OrderNode *node = (OrderNode *)iterator->next();
229 if (node->status == NOTVISITED && !node->removed) {
230 node->status = VISITED;
231 DFSNodeVisit(node, finishNodes, false, false, 0);
232 node->status = FINISHED;
233 finishNodes->push(node);
239 void OrderGraph::DFSMust(Vector<OrderNode *> *finishNodes) {
240 SetIteratorOrderNode *iterator = getNodes();
241 while (iterator->hasNext()) {
242 OrderNode *node = (OrderNode *)iterator->next();
243 if (node->status == NOTVISITED && !node->removed) {
244 node->status = VISITED;
245 DFSNodeVisit(node, finishNodes, false, true, 0);
246 node->status = FINISHED;
247 finishNodes->push(node);
253 void OrderGraph::DFSReverse(Vector<OrderNode *> *finishNodes) {
254 uint size = finishNodes->getSize();
256 for (int i = size - 1; i >= 0; i--) {
257 OrderNode *node = finishNodes->get(i);
258 if (node->status == NOTVISITED) {
259 node->status = VISITED;
260 DFSNodeVisit(node, NULL, true, false, sccNum);
261 node->sccNum = sccNum;
262 node->status = FINISHED;
268 void OrderGraph::DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
269 SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
270 while (iterator->hasNext()) {
271 OrderEdge *edge = iterator->next();
276 if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity
279 OrderNode *child = isReverse ? edge->source : edge->sink;
280 if (child->status == NOTVISITED) {
281 child->status = VISITED;
282 DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
283 child->status = FINISHED;
284 if (finishNodes != NULL) {
285 finishNodes->push(child);
288 child->sccNum = sccNum;
294 void OrderGraph::resetNodeInfoStatusSCC() {
295 SetIteratorOrderNode *iterator = getNodes();
296 while (iterator->hasNext()) {
297 ((OrderNode *)iterator->next())->status = NOTVISITED;
302 void OrderGraph::computeStronglyConnectedComponentGraph() {
303 Vector<OrderNode *> finishNodes;
305 resetNodeInfoStatusSCC();
306 DFSReverse(&finishNodes);
307 resetNodeInfoStatusSCC();
310 /** This function computes a source set for every nodes, the set of
311 nodes that can reach that node via pospolarity edges. It then
312 looks for negative polarity edges from nodes in the the source set
313 to determine whether we need to generate pseudoPos edges. */
315 void OrderGraph::completePartialOrderGraph() {
316 Vector<OrderNode *> finishNodes;
318 resetNodeInfoStatusSCC();
319 HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
321 Vector<OrderNode *> sccNodes;
323 uint size = finishNodes.getSize();
325 for (int i = size - 1; i >= 0; i--) {
326 OrderNode *node = finishNodes.get(i);
327 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
328 table->put(node, sources);
330 if (node->status == NOTVISITED) {
331 //Need to do reverse traversal here...
332 node->status = VISITED;
333 DFSNodeVisit(node, &sccNodes, true, false, sccNum);
334 node->status = FINISHED;
335 node->sccNum = sccNum;
339 //Compute in set for entire SCC
340 uint rSize = sccNodes.getSize();
341 for (uint j = 0; j < rSize; j++) {
342 OrderNode *rnode = sccNodes.get(j);
343 //Compute source sets
344 SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
345 while (iterator->hasNext()) {
346 OrderEdge *edge = iterator->next();
347 OrderNode *parent = edge->source;
349 sources->add(parent);
350 HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
351 sources->addAll(parent_srcs);
356 for (uint j = 0; j < rSize; j++) {
357 //Copy in set of entire SCC
358 OrderNode *rnode = sccNodes.get(j);
359 HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
360 table->put(rnode, set);
362 //Use source sets to compute pseudoPos edges
363 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
364 while (iterator->hasNext()) {
365 OrderEdge *edge = iterator->next();
366 OrderNode *parent = edge->source;
367 ASSERT(parent != rnode);
368 if (edge->polNeg && parent->sccNum != rnode->sccNum &&
369 sources->contains(parent)) {
370 OrderEdge *newedge = getOrderEdgeFromOrderGraph(rnode, parent);
371 newedge->pseudoPos = true;
381 table->resetAndDeleteVals();
383 resetNodeInfoStatusSCC();