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 order->graph = orderGraph;
16 uint constrSize = order->constraints.getSize();
17 for (uint j = 0; j < constrSize; j++) {
18 orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
23 //Builds only the subgraph for the must order graph.
24 OrderGraph *buildMustOrderGraph(Order *order) {
25 ASSERT(order->graph == NULL);
26 OrderGraph *orderGraph = new OrderGraph(order);
27 uint constrSize = order->constraints.getSize();
28 for (uint j = 0; j < constrSize; j++) {
29 orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
34 void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
35 Polarity polarity = constr->polarity;
36 BooleanValue mustval = constr->boolVal;
40 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
41 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
42 _1to2->mustPos = true;
44 node1->addNewOutgoingEdge(_1to2);
45 node2->addNewIncomingEdge(_1to2);
46 if (constr->polarity == P_TRUE)
50 if (order->type == SATC_TOTAL) {
51 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
52 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
53 _2to1->mustPos = true;
55 node2->addNewOutgoingEdge(_2to1);
56 node1->addNewIncomingEdge(_2to1);
58 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
59 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
60 _1to2->mustNeg = true;
62 node1->addNewOutgoingEdge(_1to2);
63 node2->addNewIncomingEdge(_1to2);
68 //There is an unreachable order constraint if this assert fires
69 //Clients can easily do this, so don't do anything.
74 void OrderGraph::addEdge(uint64_t first, uint64_t second) {
75 OrderNode *node1 = getOrderNodeFromOrderGraph(first);
76 OrderNode *node2 = getOrderNodeFromOrderGraph(second);
77 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
79 _1to2->mustPos = true;
80 node1->addNewOutgoingEdge(_1to2);
81 node2->addNewIncomingEdge(_1to2);
84 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
85 BooleanValue mustval = constr->boolVal;
89 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
90 _1to2->mustPos = true;
92 node1->addNewOutgoingEdge(_1to2);
93 node2->addNewIncomingEdge(_1to2);
94 if (constr->boolVal == BV_MUSTBETRUE)
97 case BV_MUSTBEFALSE: {
98 if (order->type == SATC_TOTAL) {
99 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
100 _2to1->mustPos = true;
101 _2to1->polPos = true;
102 node2->addNewOutgoingEdge(_2to1);
103 node1->addNewIncomingEdge(_2to1);
105 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
106 _1to2->mustNeg = true;
107 _1to2->polNeg = true;
108 node1->addNewOutgoingEdge(_1to2);
109 node2->addNewIncomingEdge(_1to2);
119 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
120 OrderNode *node = new OrderNode(id);
121 OrderNode *tmp = nodes.get(node);
132 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
134 OrderNode *tmp = nodes.get(&node);
138 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
139 OrderEdge *edge = new OrderEdge(begin, end);
140 OrderEdge *tmp = edges.get(edge);
150 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
151 OrderEdge edge(begin, end);
152 OrderEdge *tmp = edges.get(&edge);
156 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
157 OrderEdge inverseedge(edge->sink, edge->source);
158 OrderEdge *tmp = edges.get(&inverseedge);
162 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
163 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
164 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
165 addOrderEdge(from, to, bOrder);
168 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
169 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
170 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
171 addMustOrderEdge(from, to, bOrder);
174 OrderGraph::~OrderGraph() {
175 uint size=allNodes.getSize();
176 for(uint i=0;i<size;i++)
177 delete allNodes.get(i);
179 SetIteratorOrderEdge *eiterator = edges.iterator();
180 while (eiterator->hasNext()) {
181 OrderEdge *edge = eiterator->next();
187 bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
188 HashsetOrderNode visited;
190 SetIteratorOrderEdge *iterator = source->outEdges.iterator();
192 while (iterator->hasNext()) {
193 OrderEdge *edge = iterator->next();
195 OrderNode *node = edge->sink;
196 if (!visited.contains(node)) {
197 if ( node == destination ) {
202 found = isTherePathVisit(visited, node, destination);
213 bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination) {
214 SetIteratorOrderEdge *iterator = current->outEdges.iterator();
216 while (iterator->hasNext()) {
217 OrderEdge *edge = iterator->next();
219 OrderNode *node = edge->sink;
220 if (node == destination) {
225 if (isTherePathVisit(visited, node, destination)) {
235 void OrderGraph::DFS(Vector<OrderNode *> *finishNodes) {
236 SetIteratorOrderNode *iterator = getNodes();
237 while (iterator->hasNext()) {
238 OrderNode *node = iterator->next();
239 if (node->status == NOTVISITED) {
240 node->status = VISITED;
241 DFSNodeVisit(node, finishNodes, false, false, 0);
242 node->status = FINISHED;
243 finishNodes->push(node);
249 void OrderGraph::DFSMust(Vector<OrderNode *> *finishNodes) {
250 SetIteratorOrderNode *iterator = getNodes();
251 while (iterator->hasNext()) {
252 OrderNode *node = iterator->next();
253 if (node->status == NOTVISITED) {
254 node->status = VISITED;
255 DFSNodeVisit(node, finishNodes, false, true, 0);
256 node->status = FINISHED;
257 finishNodes->push(node);
263 void OrderGraph::DFSReverse(Vector<OrderNode *> *finishNodes) {
264 uint size = finishNodes->getSize();
266 for (int i = size - 1; i >= 0; i--) {
267 OrderNode *node = finishNodes->get(i);
268 if (node->status == NOTVISITED) {
269 node->status = VISITED;
270 DFSNodeVisit(node, NULL, true, false, sccNum);
271 node->sccNum = sccNum;
272 node->status = FINISHED;
278 void OrderGraph::DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
279 SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
280 while (iterator->hasNext()) {
281 OrderEdge *edge = iterator->next();
286 if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity
289 OrderNode *child = isReverse ? edge->source : edge->sink;
290 if (child->status == NOTVISITED) {
291 child->status = VISITED;
292 DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
293 child->status = FINISHED;
294 if (finishNodes != NULL) {
295 finishNodes->push(child);
298 child->sccNum = sccNum;
304 void OrderGraph::resetNodeInfoStatusSCC() {
305 SetIteratorOrderNode *iterator = getNodes();
306 while (iterator->hasNext()) {
307 iterator->next()->status = NOTVISITED;
312 void OrderGraph::computeStronglyConnectedComponentGraph() {
313 Vector<OrderNode *> finishNodes;
315 resetNodeInfoStatusSCC();
316 DFSReverse(&finishNodes);
317 resetNodeInfoStatusSCC();
320 /** This function computes a source set for every nodes, the set of
321 nodes that can reach that node via pospolarity edges. It then
322 looks for negative polarity edges from nodes in the the source set
323 to determine whether we need to generate pseudoPos edges. */
325 void OrderGraph::completePartialOrderGraph() {
326 Vector<OrderNode *> finishNodes;
328 resetNodeInfoStatusSCC();
329 HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
331 Vector<OrderNode *> sccNodes;
333 uint size = finishNodes.getSize();
335 for (int i = size - 1; i >= 0; i--) {
336 OrderNode *node = finishNodes.get(i);
337 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
338 table->put(node, sources);
340 if (node->status == NOTVISITED) {
341 //Need to do reverse traversal here...
342 node->status = VISITED;
343 DFSNodeVisit(node, &sccNodes, true, false, sccNum);
344 node->status = FINISHED;
345 node->sccNum = sccNum;
349 //Compute in set for entire SCC
350 uint rSize = sccNodes.getSize();
351 for (uint j = 0; j < rSize; j++) {
352 OrderNode *rnode = sccNodes.get(j);
353 //Compute source sets
354 SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
355 while (iterator->hasNext()) {
356 OrderEdge *edge = iterator->next();
357 OrderNode *parent = edge->source;
359 sources->add(parent);
360 HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
361 sources->addAll(parent_srcs);
366 for (uint j = 0; j < rSize; j++) {
367 //Copy in set of entire SCC
368 OrderNode *rnode = sccNodes.get(j);
369 HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
370 table->put(rnode, set);
372 //Use source sets to compute pseudoPos edges
373 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
374 while (iterator->hasNext()) {
375 OrderEdge *edge = iterator->next();
376 OrderNode *parent = edge->source;
377 ASSERT(parent != rnode);
378 if (edge->polNeg && parent->sccNum != rnode->sccNum &&
379 sources->contains(parent)) {
380 OrderEdge *newedge = getOrderEdgeFromOrderGraph(rnode, parent);
381 newedge->pseudoPos = true;
391 table->resetAndDeleteVals();
393 resetNodeInfoStatusSCC();