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::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
75 BooleanValue mustval = constr->boolVal;
79 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
80 _1to2->mustPos = true;
82 node1->addNewOutgoingEdge(_1to2);
83 node2->addNewIncomingEdge(_1to2);
84 if (constr->boolVal == BV_MUSTBETRUE)
87 case BV_MUSTBEFALSE: {
88 if (order->type == SATC_TOTAL) {
89 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
90 _2to1->mustPos = true;
92 node2->addNewOutgoingEdge(_2to1);
93 node1->addNewIncomingEdge(_2to1);
95 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
96 _1to2->mustNeg = true;
98 node1->addNewOutgoingEdge(_1to2);
99 node2->addNewIncomingEdge(_1to2);
109 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
110 OrderNode *node = new OrderNode(id);
111 OrderNode *tmp = nodes.get(node);
122 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
124 OrderNode *tmp = nodes.get(&node);
128 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
129 OrderEdge *edge = new OrderEdge(begin, end);
130 OrderEdge *tmp = edges.get(edge);
140 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
141 OrderEdge edge(begin, end);
142 OrderEdge *tmp = edges.get(&edge);
146 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
147 OrderEdge inverseedge(edge->sink, edge->source);
148 OrderEdge *tmp = edges.get(&inverseedge);
152 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
153 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
154 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
155 addOrderEdge(from, to, bOrder);
158 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
159 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
160 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
161 addMustOrderEdge(from, to, bOrder);
164 OrderGraph::~OrderGraph() {
165 uint size=allNodes.getSize();
166 for(uint i=0;i<size;i++)
167 delete allNodes.get(i);
169 SetIteratorOrderEdge *eiterator = edges.iterator();
170 while (eiterator->hasNext()) {
171 OrderEdge *edge = eiterator->next();
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 = iterator->next();
229 if (node->status == NOTVISITED) {
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 = iterator->next();
243 if (node->status == NOTVISITED) {
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 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();