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 Vector<BooleanOrder *> *constraints = order->getConstraints();
16 uint constrSize = constraints->getSize();
17 for (uint j = 0; j < constrSize; j++) {
18 orderGraph->addOrderConstraintToOrderGraph(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 Vector<BooleanOrder *> *constraints = order->getConstraints();
28 uint constrSize = constraints->getSize();
29 for (uint j = 0; j < constrSize; j++) {
30 orderGraph->addMustOrderConstraintToOrderGraph(constraints->get(j));
35 void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
36 Polarity polarity = constr->polarity;
37 BooleanValue mustval = constr->boolVal;
41 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
42 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
43 _1to2->mustPos = true;
45 node1->addNewOutgoingEdge(_1to2);
46 node2->addNewIncomingEdge(_1to2);
47 if (constr->polarity == P_TRUE)
51 if (order->type == SATC_TOTAL) {
52 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
53 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
54 _2to1->mustPos = true;
56 node2->addNewOutgoingEdge(_2to1);
57 node1->addNewIncomingEdge(_2to1);
59 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
60 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
61 _1to2->mustNeg = true;
63 node1->addNewOutgoingEdge(_1to2);
64 node2->addNewIncomingEdge(_1to2);
69 //There is an unreachable order constraint if this assert fires
70 //Clients can easily do this, so don't do anything.
75 void OrderGraph::addEdge(uint64_t first, uint64_t second) {
76 OrderNode *node1 = getOrderNodeFromOrderGraph(first);
77 OrderNode *node2 = getOrderNodeFromOrderGraph(second);
78 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
80 _1to2->mustPos = true;
81 node1->addNewOutgoingEdge(_1to2);
82 node2->addNewIncomingEdge(_1to2);
85 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
86 BooleanValue mustval = constr->boolVal;
90 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
91 _1to2->mustPos = true;
93 node1->addNewOutgoingEdge(_1to2);
94 node2->addNewIncomingEdge(_1to2);
95 if (constr->boolVal == BV_MUSTBETRUE)
98 case BV_MUSTBEFALSE: {
99 if (order->type == SATC_TOTAL) {
100 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
101 _2to1->mustPos = true;
102 _2to1->polPos = true;
103 node2->addNewOutgoingEdge(_2to1);
104 node1->addNewIncomingEdge(_2to1);
106 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
107 _1to2->mustNeg = true;
108 _1to2->polNeg = true;
109 node1->addNewOutgoingEdge(_1to2);
110 node2->addNewIncomingEdge(_1to2);
120 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
121 OrderNode *node = new OrderNode(id);
122 OrderNode *tmp = (OrderNode *)nodes.get(node);
132 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
133 OrderNodeKey node(id);
134 OrderNode *tmp = (OrderNode *)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 nodes.resetAndDelete();
176 edges.resetAndDelete();
179 bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
180 HashsetOrderNode visited;
182 SetIteratorOrderEdge *iterator = source->outEdges.iterator();
184 while (iterator->hasNext()) {
185 OrderEdge *edge = iterator->next();
187 OrderNode *node = edge->sink;
188 if (!visited.contains(node)) {
189 if ( node == destination ) {
194 found = isTherePathVisit(visited, node, destination);
205 bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination) {
206 SetIteratorOrderEdge *iterator = current->outEdges.iterator();
208 while (iterator->hasNext()) {
209 OrderEdge *edge = iterator->next();
211 OrderNode *node = edge->sink;
212 if (node == destination) {
217 if (isTherePathVisit(visited, node, destination)) {
227 void OrderGraph::DFS(Vector<OrderNode *> *finishNodes) {
228 SetIteratorOrderNode *iterator = getNodes();
229 while (iterator->hasNext()) {
230 OrderNode *node = (OrderNode *)iterator->next();
231 if (node->status == NOTVISITED && !node->removed) {
232 node->status = VISITED;
233 DFSNodeVisit(node, finishNodes, false, false, 0);
234 node->status = FINISHED;
235 finishNodes->push(node);
241 void OrderGraph::DFSMust(Vector<OrderNode *> *finishNodes) {
242 SetIteratorOrderNode *iterator = getNodes();
243 while (iterator->hasNext()) {
244 OrderNode *node = (OrderNode *)iterator->next();
245 if (node->status == NOTVISITED && !node->removed) {
246 node->status = VISITED;
247 DFSNodeVisit(node, finishNodes, false, true, 0);
248 node->status = FINISHED;
249 finishNodes->push(node);
255 void OrderGraph::DFSReverse(Vector<OrderNode *> *finishNodes) {
256 uint size = finishNodes->getSize();
258 for (int i = size - 1; i >= 0; i--) {
259 OrderNode *node = finishNodes->get(i);
260 if (node->status == NOTVISITED) {
261 node->status = VISITED;
262 DFSNodeVisit(node, NULL, true, false, sccNum);
263 node->sccNum = sccNum;
264 node->status = FINISHED;
270 void OrderGraph::DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum) {
271 SetIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator();
272 while (iterator->hasNext()) {
273 OrderEdge *edge = iterator->next();
278 if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity
281 OrderNode *child = isReverse ? edge->source : edge->sink;
282 if (child->status == NOTVISITED) {
283 child->status = VISITED;
284 DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum);
285 child->status = FINISHED;
286 if (finishNodes != NULL) {
287 finishNodes->push(child);
290 child->sccNum = sccNum;
296 void OrderGraph::resetNodeInfoStatusSCC() {
297 SetIteratorOrderNode *iterator = getNodes();
298 while (iterator->hasNext()) {
299 ((OrderNode *)iterator->next())->status = NOTVISITED;
304 void OrderGraph::computeStronglyConnectedComponentGraph() {
305 Vector<OrderNode *> finishNodes;
307 resetNodeInfoStatusSCC();
308 DFSReverse(&finishNodes);
309 resetNodeInfoStatusSCC();
312 /** This function computes a source set for every nodes, the set of
313 nodes that can reach that node via pospolarity edges. It then
314 looks for negative polarity edges from nodes in the the source set
315 to determine whether we need to generate pseudoPos edges. */
317 void OrderGraph::completePartialOrderGraph() {
318 Vector<OrderNode *> finishNodes;
320 resetNodeInfoStatusSCC();
321 HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
323 Vector<OrderNode *> sccNodes;
325 uint size = finishNodes.getSize();
327 for (int i = size - 1; i >= 0; i--) {
328 OrderNode *node = finishNodes.get(i);
329 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
330 table->put(node, sources);
332 if (node->status == NOTVISITED) {
333 //Need to do reverse traversal here...
334 node->status = VISITED;
335 DFSNodeVisit(node, &sccNodes, true, false, sccNum);
336 node->status = FINISHED;
337 node->sccNum = sccNum;
341 //Compute in set for entire SCC
342 uint rSize = sccNodes.getSize();
343 for (uint j = 0; j < rSize; j++) {
344 OrderNode *rnode = sccNodes.get(j);
345 //Compute source sets
346 SetIteratorOrderEdge *iterator = rnode->inEdges.iterator();
347 while (iterator->hasNext()) {
348 OrderEdge *edge = iterator->next();
349 OrderNode *parent = edge->source;
351 sources->add(parent);
352 HashsetOrderNode *parent_srcs = (HashsetOrderNode *)table->get(parent);
353 sources->addAll(parent_srcs);
358 for (uint j = 0; j < rSize; j++) {
359 //Copy in set of entire SCC
360 OrderNode *rnode = sccNodes.get(j);
361 HashsetOrderNode *set = (j == 0) ? sources : sources->copy();
362 table->put(rnode, set);
364 //Use source sets to compute pseudoPos edges
365 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
366 while (iterator->hasNext()) {
367 OrderEdge *edge = iterator->next();
368 OrderNode *parent = edge->source;
369 ASSERT(parent != rnode);
370 if (edge->polNeg && parent->sccNum != rnode->sccNum &&
371 sources->contains(parent)) {
372 OrderEdge *newedge = getOrderEdgeFromOrderGraph(rnode, parent);
373 newedge->pseudoPos = true;
383 table->resetAndDeleteVals();
385 resetNodeInfoStatusSCC();