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"
19 #include "polarityassignment.h"
22 DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
27 DecomposeOrderTransform::~DecomposeOrderTransform() {
30 void DecomposeOrderTransform::doTransform() {
31 HashsetOrder *orders = solver->getActiveOrders()->copy();
32 SetIteratorOrder *orderit = orders->iterator();
33 while (orderit->hasNext()) {
34 Order *order = orderit->next();
36 if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
40 DecomposeOrderResolver *dor = new DecomposeOrderResolver(order);
41 order->setOrderResolver(dor);
43 OrderGraph *graph = buildOrderGraph(order);
44 if (order->type == SATC_PARTIAL) {
45 //Required to do SCC analysis for partial order graphs. It
46 //makes sure we don't incorrectly optimize graphs with negative
48 graph->completePartialOrderGraph();
51 bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
53 reachMustAnalysis(solver, graph, false);
55 bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
57 //This pair of analysis is also optional
58 if (order->type == SATC_PARTIAL) {
59 localMustAnalysisPartial(solver, graph);
61 localMustAnalysisTotal(solver, graph);
65 bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
68 removeMustBeTrueNodes(graph, dor);
71 bool pruneEdges = GETVARTUNABLE(solver->getTuner(), order->type, MUSTEDGEPRUNE, &onoff);
74 mustEdgePrune(graph, dor);
77 //This is needed for splitorder
78 graph->computeStronglyConnectedComponentGraph();
79 decomposeOrder(order, graph, dor);
87 void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) {
88 Vector<Order *> partialcandidatevec;
89 uint size = currOrder->constraints.getSize();
90 for (uint i = 0; i < size; i++) {
91 BooleanOrder *orderconstraint = currOrder->constraints.get(i);
92 OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
93 OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
94 OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
95 OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
96 if (from->removed || to->removed)
99 if (from->sccNum != to->sccNum) {
102 dor->mustOrderEdge(from->getID(), to->getID());
103 solver->replaceBooleanWithTrue(orderconstraint);
104 } else if (edge->polNeg) {
105 if (currOrder->type == SATC_TOTAL)
106 dor->mustOrderEdge(to->getID(), from->getID());
107 solver->replaceBooleanWithFalse(orderconstraint);
109 //This case should only be possible if constraint isn't in AST
110 //This can happen, so don't do anything
114 if (invedge != NULL) {
115 if (invedge->polPos) {
116 dor->mustOrderEdge(to->getID(), from->getID());
117 solver->replaceBooleanWithFalse(orderconstraint);
118 } else if (edge->polNeg) {
119 //This case shouldn't happen... If we have a partial order,
120 //then we should have our own edge...If we have a total
121 //order, then this edge should be positive...
124 //This case should only be possible if constraint isn't in AST
125 //This can happen, so don't do anything
131 //Build new order and change constraint's order
132 Order *neworder = NULL;
133 neworder = dor->getOrder(from->sccNum);
134 if (neworder == NULL) {
135 MutableSet *set = solver->createMutableSet(currOrder->set->getType());
136 neworder = solver->createOrder(currOrder->type, set);
137 dor->setOrder(from->sccNum, neworder);
138 if (currOrder->type == SATC_PARTIAL)
139 partialcandidatevec.setExpand(from->sccNum, neworder);
141 partialcandidatevec.setExpand(from->sccNum, NULL);
143 if (from->status != ADDEDTOSET) {
144 from->status = ADDEDTOSET;
145 ((MutableSet *)neworder->set)->addElementMSet(from->id);
147 if (to->status != ADDEDTOSET) {
148 to->status = ADDEDTOSET;
149 ((MutableSet *)neworder->set)->addElementMSet(to->id);
151 if (currOrder->type == SATC_PARTIAL) {
153 partialcandidatevec.setExpand(from->sccNum, NULL);
155 BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
156 solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
157 updateEdgePolarity(neworderconstraint, orderconstraint);
158 dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
161 solver->getActiveOrders()->remove(currOrder);
162 uint pcvsize = partialcandidatevec.getSize();
163 for (uint i = 0; i < pcvsize; i++) {
164 Order *neworder = partialcandidatevec.get(i);
165 if (neworder != NULL) {
166 neworder->type = SATC_TOTAL;
171 bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
172 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
173 while (iterator->hasNext()) {
174 OrderEdge *edge = iterator->next();
175 if (!edge->mustPos) {
181 iterator = node->outEdges.iterator();
182 while (iterator->hasNext()) {
183 OrderEdge *edge = iterator->next();
184 if (!edge->mustPos) {
193 void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
194 node->removed = true;
195 SetIteratorOrderEdge *iterin = node->inEdges.iterator();
196 while (iterin->hasNext()) {
197 OrderEdge *inEdge = iterin->next();
198 OrderNode *srcNode = inEdge->source;
199 srcNode->outEdges.remove(inEdge);
200 dor->mustOrderEdge(srcNode->getID(), node->getID());
201 BooleanEdge be = solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID());
202 solver->replaceBooleanWithTrue(be);
204 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
205 while (iterout->hasNext()) {
206 OrderEdge *outEdge = iterout->next();
207 OrderNode *sinkNode = outEdge->sink;
208 //Adding new edge to new sink and src nodes ...
209 if (srcNode == sinkNode) {
215 //Add new order constraint
216 BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
217 updateEdgePolarity(orderconstraint, P_TRUE);
218 solver->addConstraint(orderconstraint);
221 OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
222 newEdge->mustPos = true;
223 newEdge->polPos = true;
224 if (newEdge->mustNeg)
226 srcNode->outEdges.add(newEdge);
227 sinkNode->inEdges.add(newEdge);
233 //Clean up old edges... Keep this later in case we don't have any in edges
234 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
235 while (iterout->hasNext()) {
236 OrderEdge *outEdge = iterout->next();
237 OrderNode *sinkNode = outEdge->sink;
238 dor->mustOrderEdge(node->getID(), sinkNode->getID());
239 sinkNode->inEdges.remove(outEdge);
240 BooleanEdge be2 = solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
241 solver->replaceBooleanWithTrue(be2);
246 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
247 SetIteratorOrderNode *iterator = graph->getNodes();
248 while (iterator->hasNext()) {
249 OrderNode *node = (OrderNode *)iterator->next();
252 if (isMustBeTrueNode(node)) {
253 bypassMustBeTrueNode(graph, node, dor);
259 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
260 SetIteratorOrderNode *iterator = graph->getNodes();
261 while (iterator->hasNext()) {
262 OrderNode *node = (OrderNode *)iterator->next();
265 attemptNodeMerge(graph, node, dor);
270 void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
271 SetIteratorOrderEdge *edgeit = node->outEdges.iterator();
272 while (edgeit->hasNext()) {
273 OrderEdge *outedge = edgeit->next();
274 //Only eliminate must edges
275 if (!outedge->mustPos)
277 OrderNode *dstnode = outedge->sink;
278 uint numOutEdges = node->outEdges.getSize();
279 uint numInEdges = dstnode->inEdges.getSize();
281 Need to avoid a situation where we create new reachability by
282 the merge. This can only happen if there is an extra in edge to
283 the dstnode and an extra out edge to our node.
286 if (numOutEdges == 1 || numInEdges == 1) {
287 /* Safe to do the Merge */
288 mergeNodes(graph, node, outedge, dstnode, dor);
290 //Throw away the iterator and start over
292 edgeit = node->outEdges.iterator();
298 void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
299 /* Fix up must edge between the two nodes */
300 node->outEdges.remove(edge);
301 dstnode->inEdges.remove(edge);
302 dor->mustOrderEdge(node->getID(), dstnode->getID());
304 BooleanEdge be = solver->orderConstraint(graph->getOrder(), node->getID(), dstnode->getID());
305 solver->replaceBooleanWithTrue(be);
307 /* Go through the incoming edges to the new node */
308 SetIteratorOrderEdge *inedgeit = dstnode->inEdges.iterator();
309 while (inedgeit->hasNext()) {
310 OrderEdge *inedge = inedgeit->next();
311 OrderNode *source = inedge->source;
312 //remove it from the source node
313 source->outEdges.remove(inedge);
314 //save the remapping that we did
315 dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
316 //create the new edge
317 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(source, node);
319 newedge->polPos |= inedge->polPos;
320 newedge->polNeg |= inedge->polNeg;
321 newedge->mustPos |= inedge->mustPos;
322 newedge->mustNeg |= inedge->mustNeg;
323 newedge->pseudoPos |= inedge->pseudoPos;
324 //add new edge to both
325 source->outEdges.add(newedge);
326 node->inEdges.add(newedge);
328 BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
329 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
330 updateEdgePolarity(benew, be);
331 solver->replaceBooleanWithBoolean(be, benew);
333 dstnode->inEdges.reset();
336 /* Go through the outgoing edges from the new node */
337 SetIteratorOrderEdge *outedgeit = dstnode->outEdges.iterator();
338 while (outedgeit->hasNext()) {
339 OrderEdge *outedge = outedgeit->next();
340 OrderNode *sink = outedge->sink;
341 //remove it from the sink node
342 sink->inEdges.remove(outedge);
343 //save the remapping that we did
344 dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
346 //create the new edge
347 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
349 newedge->polPos |= outedge->polPos;
350 newedge->polNeg |= outedge->polNeg;
351 newedge->mustPos |= outedge->mustPos;
352 newedge->mustNeg |= outedge->mustNeg;
353 newedge->pseudoPos |= outedge->pseudoPos;
354 //add new edge to both
355 sink->inEdges.add(newedge);
356 node->outEdges.add(newedge);
358 BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
359 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
360 updateEdgePolarity(benew, be);
361 solver->replaceBooleanWithBoolean(be, benew);
363 dstnode->outEdges.reset();
367 /* Mark destination as removed */
368 dstnode->removed = true;