2 * File: ordertransform.cc
5 * Created on August 28, 2017, 10:35 AM
8 #include "decomposeordertransform.h"
10 #include "orderedge.h"
11 #include "ordernode.h"
13 #include "mutableset.h"
14 #include "ordergraph.h"
16 #include "decomposeorderresolver.h"
18 #include "orderanalysis.h"
21 DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
26 DecomposeOrderTransform::~DecomposeOrderTransform() {
29 void DecomposeOrderTransform::doTransform() {
30 HashsetOrder *orders = solver->getActiveOrders()->copy();
31 SetIteratorOrder *orderit = orders->iterator();
32 while (orderit->hasNext()) {
33 Order *order = orderit->next();
35 if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
39 DecomposeOrderResolver *dor = new DecomposeOrderResolver(order);
40 order->setOrderResolver(dor);
42 OrderGraph *graph = buildOrderGraph(order);
43 if (order->type == SATC_PARTIAL) {
44 //Required to do SCC analysis for partial order graphs. It
45 //makes sure we don't incorrectly optimize graphs with negative
47 graph->completePartialOrderGraph();
50 bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
52 reachMustAnalysis(solver, graph, false);
54 bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
56 //This pair of analysis is also optional
57 if (order->type == SATC_PARTIAL) {
58 localMustAnalysisPartial(solver, graph);
60 localMustAnalysisTotal(solver, graph);
64 bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
67 removeMustBeTrueNodes(graph, dor);
70 bool pruneEdges = GETVARTUNABLE(solver->getTuner(), order->type, MUSTEDGEPRUNE, &onoff);
73 mustEdgePrune(graph, dor);
76 //This is needed for splitorder
77 graph->computeStronglyConnectedComponentGraph();
78 decomposeOrder(order, graph, dor);
86 void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) {
87 Vector<Order *> partialcandidatevec;
88 uint size = currOrder->constraints.getSize();
89 for (uint i = 0; i < size; i++) {
90 BooleanOrder *orderconstraint = currOrder->constraints.get(i);
91 OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
92 OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
93 OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
94 OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
95 if (from->removed || to->removed)
98 if (from->sccNum != to->sccNum) {
101 dor->mustOrderEdge(from->getID(), to->getID());
102 solver->replaceBooleanWithTrue(orderconstraint);
103 } else if (edge->polNeg) {
104 if (currOrder->type == SATC_TOTAL)
105 dor->mustOrderEdge(to->getID(), from->getID());
106 solver->replaceBooleanWithFalse(orderconstraint);
108 //This case should only be possible if constraint isn't in AST
109 //This can happen, so don't do anything
113 if (invedge != NULL) {
114 if (invedge->polPos) {
115 dor->mustOrderEdge(to->getID(), from->getID());
116 solver->replaceBooleanWithFalse(orderconstraint);
117 } else if (edge->polNeg) {
118 //This case shouldn't happen... If we have a partial order,
119 //then we should have our own edge...If we have a total
120 //order, then this edge should be positive...
123 //This case should only be possible if constraint isn't in AST
124 //This can happen, so don't do anything
130 //Build new order and change constraint's order
131 Order *neworder = NULL;
132 neworder = dor->getOrder(from->sccNum);
133 if (neworder == NULL) {
134 MutableSet *set = solver->createMutableSet(currOrder->set->getType());
135 neworder = solver->createOrder(currOrder->type, set);
136 dor->setOrder(from->sccNum, neworder);
137 if (currOrder->type == SATC_PARTIAL)
138 partialcandidatevec.setExpand(from->sccNum, neworder);
140 partialcandidatevec.setExpand(from->sccNum, NULL);
142 if (from->status != ADDEDTOSET) {
143 from->status = ADDEDTOSET;
144 ((MutableSet *)neworder->set)->addElementMSet(from->id);
146 if (to->status != ADDEDTOSET) {
147 to->status = ADDEDTOSET;
148 ((MutableSet *)neworder->set)->addElementMSet(to->id);
150 if (currOrder->type == SATC_PARTIAL) {
152 partialcandidatevec.setExpand(from->sccNum, NULL);
154 BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
155 solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
157 dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
160 solver->getActiveOrders()->remove(currOrder);
161 uint pcvsize = partialcandidatevec.getSize();
162 for (uint i = 0; i < pcvsize; i++) {
163 Order *neworder = partialcandidatevec.get(i);
164 if (neworder != NULL) {
165 neworder->type = SATC_TOTAL;
170 bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
171 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
172 while (iterator->hasNext()) {
173 OrderEdge *edge = iterator->next();
174 if (!edge->mustPos) {
180 iterator = node->outEdges.iterator();
181 while (iterator->hasNext()) {
182 OrderEdge *edge = iterator->next();
183 if (!edge->mustPos) {
192 void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
193 node->removed = true;
194 SetIteratorOrderEdge *iterin = node->inEdges.iterator();
195 while (iterin->hasNext()) {
196 OrderEdge *inEdge = iterin->next();
197 OrderNode *srcNode = inEdge->source;
198 srcNode->outEdges.remove(inEdge);
199 dor->mustOrderEdge(srcNode->getID(), node->getID());
200 BooleanEdge be = solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID());
201 solver->replaceBooleanWithTrue(be);
203 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
204 while (iterout->hasNext()) {
205 OrderEdge *outEdge = iterout->next();
206 OrderNode *sinkNode = outEdge->sink;
207 //Adding new edge to new sink and src nodes ...
208 if (srcNode == sinkNode) {
214 //Add new order constraint
215 BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
216 solver->addConstraint(orderconstraint);
219 OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
220 newEdge->mustPos = true;
221 newEdge->polPos = true;
222 if (newEdge->mustNeg)
224 srcNode->outEdges.add(newEdge);
225 sinkNode->inEdges.add(newEdge);
231 //Clean up old edges... Keep this later in case we don't have any in edges
232 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
233 while (iterout->hasNext()) {
234 OrderEdge *outEdge = iterout->next();
235 OrderNode *sinkNode = outEdge->sink;
236 dor->mustOrderEdge(node->getID(), sinkNode->getID());
237 sinkNode->inEdges.remove(outEdge);
238 BooleanEdge be2 = solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
239 solver->replaceBooleanWithTrue(be2);
244 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
245 SetIteratorOrderNode *iterator = graph->getNodes();
246 while (iterator->hasNext()) {
247 OrderNode *node = (OrderNode *)iterator->next();
250 if (isMustBeTrueNode(node)) {
251 bypassMustBeTrueNode(graph, node, dor);
257 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
258 SetIteratorOrderNode *iterator = graph->getNodes();
259 while (iterator->hasNext()) {
260 OrderNode *node = (OrderNode *)iterator->next();
263 attemptNodeMerge(graph, node, dor);
268 void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
269 SetIteratorOrderEdge *edgeit = node->outEdges.iterator();
270 while (edgeit->hasNext()) {
271 OrderEdge *outedge = edgeit->next();
272 //Only eliminate must edges
273 if (!outedge->mustPos)
275 OrderNode *dstnode = outedge->sink;
276 uint numOutEdges = node->outEdges.getSize();
277 uint numInEdges = dstnode->inEdges.getSize();
279 Need to avoid a situation where we create new reachability by
280 the merge. This can only happen if there is an extra in edge to
281 the dstnode and an extra out edge to our node.
284 if (numOutEdges == 1 || numInEdges == 1) {
285 /* Safe to do the Merge */
286 mergeNodes(graph, node, outedge, dstnode, dor);
288 //Throw away the iterator and start over
290 edgeit = node->outEdges.iterator();
296 void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
297 /* Fix up must edge between the two nodes */
298 node->outEdges.remove(edge);
299 dstnode->inEdges.remove(edge);
300 dor->mustOrderEdge(node->getID(), dstnode->getID());
302 BooleanEdge be = solver->orderConstraint(graph->getOrder(), node->getID(), dstnode->getID());
303 solver->replaceBooleanWithTrue(be);
305 /* Go through the incoming edges to the new node */
306 SetIteratorOrderEdge *inedgeit = dstnode->inEdges.iterator();
307 while (inedgeit->hasNext()) {
308 OrderEdge *inedge = inedgeit->next();
309 OrderNode *source = inedge->source;
310 //remove it from the source node
311 source->outEdges.remove(inedge);
312 //save the remapping that we did
313 dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
314 //create the new edge
315 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(source, node);
317 newedge->polPos |= inedge->polPos;
318 newedge->polNeg |= inedge->polNeg;
319 newedge->mustPos |= inedge->mustPos;
320 newedge->mustNeg |= inedge->mustNeg;
321 newedge->pseudoPos |= inedge->pseudoPos;
322 //add new edge to both
323 source->outEdges.add(newedge);
324 node->inEdges.add(newedge);
326 BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
327 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
328 solver->replaceBooleanWithBoolean(be, benew);
330 dstnode->inEdges.reset();
333 /* Go through the outgoing edges from the new node */
334 SetIteratorOrderEdge *outedgeit = dstnode->outEdges.iterator();
335 while (outedgeit->hasNext()) {
336 OrderEdge *outedge = outedgeit->next();
337 OrderNode *sink = outedge->sink;
338 //remove it from the sink node
339 sink->inEdges.remove(outedge);
340 //save the remapping that we did
341 dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
343 //create the new edge
344 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
346 newedge->polPos |= outedge->polPos;
347 newedge->polNeg |= outedge->polNeg;
348 newedge->mustPos |= outedge->mustPos;
349 newedge->mustNeg |= outedge->mustNeg;
350 newedge->pseudoPos |= outedge->pseudoPos;
351 //add new edge to both
352 sink->inEdges.add(newedge);
353 node->outEdges.add(newedge);
355 BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
356 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
357 solver->replaceBooleanWithBoolean(be, benew);
359 dstnode->outEdges.reset();
363 /* Mark destination as removed */
364 dstnode->removed = true;