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);
156 dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
159 solver->getActiveOrders()->remove(currOrder);
160 uint pcvsize = partialcandidatevec.getSize();
161 for (uint i = 0; i < pcvsize; i++) {
162 Order *neworder = partialcandidatevec.get(i);
163 if (neworder != NULL) {
164 neworder->type = SATC_TOTAL;
169 bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
170 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
171 while (iterator->hasNext()) {
172 OrderEdge *edge = iterator->next();
173 if (!edge->mustPos) {
179 iterator = node->outEdges.iterator();
180 while (iterator->hasNext()) {
181 OrderEdge *edge = iterator->next();
182 if (!edge->mustPos) {
191 void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
192 node->removed = true;
193 SetIteratorOrderEdge *iterin = node->inEdges.iterator();
194 while (iterin->hasNext()) {
195 OrderEdge *inEdge = iterin->next();
196 OrderNode *srcNode = inEdge->source;
197 srcNode->outEdges.remove(inEdge);
198 dor->mustOrderEdge(srcNode->getID(), node->getID());
199 BooleanEdge be = solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID());
200 solver->replaceBooleanWithTrue(be);
202 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
203 while (iterout->hasNext()) {
204 OrderEdge *outEdge = iterout->next();
205 OrderNode *sinkNode = outEdge->sink;
206 //Adding new edge to new sink and src nodes ...
207 if (srcNode == sinkNode) {
213 //Add new order constraint
214 BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
215 solver->addConstraint(orderconstraint);
218 OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
219 newEdge->mustPos = true;
220 newEdge->polPos = true;
221 if (newEdge->mustNeg)
223 srcNode->outEdges.add(newEdge);
224 sinkNode->inEdges.add(newEdge);
230 //Clean up old edges... Keep this later in case we don't have any in edges
231 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
232 while (iterout->hasNext()) {
233 OrderEdge *outEdge = iterout->next();
234 OrderNode *sinkNode = outEdge->sink;
235 dor->mustOrderEdge(node->getID(), sinkNode->getID());
236 sinkNode->inEdges.remove(outEdge);
237 BooleanEdge be2 = solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
238 solver->replaceBooleanWithTrue(be2);
243 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
244 SetIteratorOrderNode *iterator = graph->getNodes();
245 while (iterator->hasNext()) {
246 OrderNode *node = (OrderNode *)iterator->next();
249 if (isMustBeTrueNode(node)) {
250 bypassMustBeTrueNode(graph, node, dor);
256 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
257 SetIteratorOrderNode *iterator = graph->getNodes();
258 while (iterator->hasNext()) {
259 OrderNode *node = (OrderNode *)iterator->next();
262 attemptNodeMerge(graph, node, dor);
267 void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
268 SetIteratorOrderEdge *edgeit = node->outEdges.iterator();
269 while (edgeit->hasNext()) {
270 OrderEdge *outedge = edgeit->next();
271 //Only eliminate must edges
272 if (!outedge->mustPos)
274 OrderNode *dstnode = outedge->sink;
275 uint numOutEdges = node->outEdges.getSize();
276 uint numInEdges = dstnode->inEdges.getSize();
278 Need to avoid a situation where we create new reachability by
279 the merge. This can only happen if there is an extra in edge to
280 the dstnode and an extra out edge to our node.
283 if (numOutEdges == 1 || numInEdges == 1) {
284 /* Safe to do the Merge */
285 mergeNodes(graph, node, outedge, dstnode, dor);
287 //Throw away the iterator and start over
289 edgeit = node->outEdges.iterator();
295 void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
296 /* Fix up must edge between the two nodes */
297 node->outEdges.remove(edge);
298 dstnode->inEdges.remove(edge);
299 dor->mustOrderEdge(node->getID(), dstnode->getID());
301 BooleanEdge be = solver->orderConstraint(graph->getOrder(), node->getID(), dstnode->getID());
302 solver->replaceBooleanWithTrue(be);
304 /* Go through the incoming edges to the new node */
305 SetIteratorOrderEdge *inedgeit = dstnode->inEdges.iterator();
306 while (inedgeit->hasNext()) {
307 OrderEdge *inedge = inedgeit->next();
308 OrderNode *source = inedge->source;
309 //remove it from the source node
310 source->outEdges.remove(inedge);
311 //save the remapping that we did
312 dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
313 //create the new edge
314 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(source, node);
316 newedge->polPos |= inedge->polPos;
317 newedge->polNeg |= inedge->polNeg;
318 newedge->mustPos |= inedge->mustPos;
319 newedge->mustNeg |= inedge->mustNeg;
320 newedge->pseudoPos |= inedge->pseudoPos;
321 //add new edge to both
322 source->outEdges.add(newedge);
323 node->inEdges.add(newedge);
325 BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
326 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
327 solver->replaceBooleanWithBoolean(be, benew);
329 dstnode->inEdges.reset();
332 /* Go through the outgoing edges from the new node */
333 SetIteratorOrderEdge *outedgeit = dstnode->outEdges.iterator();
334 while (outedgeit->hasNext()) {
335 OrderEdge *outedge = outedgeit->next();
336 OrderNode *sink = outedge->sink;
337 //remove it from the sink node
338 sink->inEdges.remove(outedge);
339 //save the remapping that we did
340 dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
342 //create the new edge
343 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
345 newedge->polPos |= outedge->polPos;
346 newedge->polNeg |= outedge->polNeg;
347 newedge->mustPos |= outedge->mustPos;
348 newedge->mustNeg |= outedge->mustNeg;
349 newedge->pseudoPos |= outedge->pseudoPos;
350 //add new edge to both
351 sink->inEdges.add(newedge);
352 node->outEdges.add(newedge);
354 BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
355 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
356 solver->replaceBooleanWithBoolean(be, benew);
358 dstnode->outEdges.reset();
362 /* Mark destination as removed */
363 dstnode->removed = true;