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() {
33 HashsetOrder *orders = solver->getActiveOrders()->copy();
34 SetIteratorOrder *orderit = orders->iterator();
35 while (orderit->hasNext()) {
36 Order *order = orderit->next();
38 if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
42 DecomposeOrderResolver *dor = new DecomposeOrderResolver(order);
43 order->setOrderResolver(dor);
45 OrderGraph *graph = buildOrderGraph(order);
46 if (order->type == SATC_PARTIAL) {
47 //Required to do SCC analysis for partial order graphs. It
48 //makes sure we don't incorrectly optimize graphs with negative
50 graph->completePartialOrderGraph();
53 bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
55 reachMustAnalysis(solver, graph, false);
57 bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
59 //This pair of analysis is also optional
60 if (order->type == SATC_PARTIAL) {
61 localMustAnalysisPartial(solver, graph);
63 localMustAnalysisTotal(solver, graph);
67 bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
70 removeMustBeTrueNodes(graph, dor);
73 bool pruneEdges = GETVARTUNABLE(solver->getTuner(), order->type, MUSTEDGEPRUNE, &onoff);
76 mustEdgePrune(graph, dor);
79 //This is needed for splitorder
80 graph->computeStronglyConnectedComponentGraph();
81 decomposeOrder(order, graph, dor);
89 void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) {
90 Vector<Order *> partialcandidatevec;
91 uint size = currOrder->constraints.getSize();
92 for (uint i = 0; i < size; i++) {
93 BooleanOrder *orderconstraint = currOrder->constraints.get(i);
94 OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
95 OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
96 OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
97 OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
98 if (from->removed || to->removed)
101 if (from->sccNum != to->sccNum) {
104 dor->mustOrderEdge(from->getID(), to->getID());
105 solver->replaceBooleanWithTrue(orderconstraint);
106 } else if (edge->polNeg) {
107 if (currOrder->type == SATC_TOTAL)
108 dor->mustOrderEdge(to->getID(), from->getID());
109 solver->replaceBooleanWithFalse(orderconstraint);
111 //This case should only be possible if constraint isn't in AST
112 //This can happen, so don't do anything
116 if (invedge != NULL) {
117 if (invedge->polPos) {
118 dor->mustOrderEdge(to->getID(), from->getID());
119 solver->replaceBooleanWithFalse(orderconstraint);
120 } else if (edge->polNeg) {
121 //This case shouldn't happen... If we have a partial order,
122 //then we should have our own edge...If we have a total
123 //order, then this edge should be positive...
126 //This case should only be possible if constraint isn't in AST
127 //This can happen, so don't do anything
133 //Build new order and change constraint's order
134 Order *neworder = NULL;
135 neworder = dor->getOrder(from->sccNum);
136 if (neworder == NULL) {
137 MutableSet *set = solver->createMutableSet(currOrder->set->getType());
138 neworder = solver->createOrder(currOrder->type, set);
139 dor->setOrder(from->sccNum, neworder);
140 if (currOrder->type == SATC_PARTIAL)
141 partialcandidatevec.setExpand(from->sccNum, neworder);
143 partialcandidatevec.setExpand(from->sccNum, NULL);
145 if (from->status != ADDEDTOSET) {
146 from->status = ADDEDTOSET;
147 ((MutableSet *)neworder->set)->addElementMSet(from->id);
149 if (to->status != ADDEDTOSET) {
150 to->status = ADDEDTOSET;
151 ((MutableSet *)neworder->set)->addElementMSet(to->id);
153 if (currOrder->type == SATC_PARTIAL) {
155 partialcandidatevec.setExpand(from->sccNum, NULL);
157 BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
158 solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
159 updateEdgePolarity(neworderconstraint, orderconstraint);
160 dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
163 solver->getActiveOrders()->remove(currOrder);
164 uint pcvsize = partialcandidatevec.getSize();
165 for (uint i = 0; i < pcvsize; i++) {
166 Order *neworder = partialcandidatevec.get(i);
167 if (neworder != NULL) {
168 neworder->type = SATC_TOTAL;
173 bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
174 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
175 while (iterator->hasNext()) {
176 OrderEdge *edge = iterator->next();
177 if (!edge->mustPos) {
183 iterator = node->outEdges.iterator();
184 while (iterator->hasNext()) {
185 OrderEdge *edge = iterator->next();
186 if (!edge->mustPos) {
195 void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
196 node->removed = true;
197 SetIteratorOrderEdge *iterin = node->inEdges.iterator();
198 while (iterin->hasNext()) {
199 OrderEdge *inEdge = iterin->next();
200 OrderNode *srcNode = inEdge->source;
201 srcNode->outEdges.remove(inEdge);
202 dor->mustOrderEdge(srcNode->getID(), node->getID());
203 BooleanEdge be = solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID());
204 solver->replaceBooleanWithTrue(be);
206 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
207 while (iterout->hasNext()) {
208 OrderEdge *outEdge = iterout->next();
209 OrderNode *sinkNode = outEdge->sink;
210 //Adding new edge to new sink and src nodes ...
211 if (srcNode == sinkNode) {
217 //Add new order constraint
218 BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
219 updateEdgePolarity(orderconstraint, P_TRUE);
220 solver->addConstraint(orderconstraint);
223 OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
224 newEdge->mustPos = true;
225 newEdge->polPos = true;
226 if (newEdge->mustNeg)
228 srcNode->outEdges.add(newEdge);
229 sinkNode->inEdges.add(newEdge);
235 //Clean up old edges... Keep this later in case we don't have any in edges
236 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
237 while (iterout->hasNext()) {
238 OrderEdge *outEdge = iterout->next();
239 OrderNode *sinkNode = outEdge->sink;
240 dor->mustOrderEdge(node->getID(), sinkNode->getID());
241 sinkNode->inEdges.remove(outEdge);
242 BooleanEdge be2 = solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
243 solver->replaceBooleanWithTrue(be2);
248 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
249 SetIteratorOrderNode *iterator = graph->getNodes();
250 while (iterator->hasNext()) {
251 OrderNode *node = (OrderNode *)iterator->next();
254 if (isMustBeTrueNode(node)) {
255 bypassMustBeTrueNode(graph, node, dor);
261 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
262 SetIteratorOrderNode *iterator = graph->getNodes();
263 while (iterator->hasNext()) {
264 OrderNode *node = (OrderNode *)iterator->next();
267 attemptNodeMerge(graph, node, dor);
272 void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
273 SetIteratorOrderEdge *edgeit = node->outEdges.iterator();
274 while (edgeit->hasNext()) {
275 OrderEdge *outedge = edgeit->next();
276 //Only eliminate must edges
277 if (!outedge->mustPos)
279 OrderNode *dstnode = outedge->sink;
280 uint numOutEdges = node->outEdges.getSize();
281 uint numInEdges = dstnode->inEdges.getSize();
283 Need to avoid a situation where we create new reachability by
284 the merge. This can only happen if there is an extra in edge to
285 the dstnode and an extra out edge to our node.
288 if (numOutEdges == 1 || numInEdges == 1) {
289 /* Safe to do the Merge */
290 mergeNodes(graph, node, outedge, dstnode, dor);
292 //Throw away the iterator and start over
294 edgeit = node->outEdges.iterator();
300 void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
301 /* Fix up must edge between the two nodes */
302 node->outEdges.remove(edge);
303 dstnode->inEdges.remove(edge);
304 dor->mustOrderEdge(node->getID(), dstnode->getID());
306 BooleanEdge be = solver->orderConstraint(graph->getOrder(), node->getID(), dstnode->getID());
307 solver->replaceBooleanWithTrue(be);
309 /* Go through the incoming edges to the new node */
310 SetIteratorOrderEdge *inedgeit = dstnode->inEdges.iterator();
311 while (inedgeit->hasNext()) {
312 OrderEdge *inedge = inedgeit->next();
313 OrderNode *source = inedge->source;
314 //remove it from the source node
315 source->outEdges.remove(inedge);
316 //save the remapping that we did
317 dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
318 //create the new edge
319 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(source, node);
321 newedge->polPos |= inedge->polPos;
322 newedge->polNeg |= inedge->polNeg;
323 newedge->mustPos |= inedge->mustPos;
324 newedge->mustNeg |= inedge->mustNeg;
325 newedge->pseudoPos |= inedge->pseudoPos;
326 //add new edge to both
327 source->outEdges.add(newedge);
328 node->inEdges.add(newedge);
330 BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
331 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
332 updateEdgePolarity(benew, be);
333 solver->replaceBooleanWithBoolean(be, benew);
335 dstnode->inEdges.reset();
338 /* Go through the outgoing edges from the new node */
339 SetIteratorOrderEdge *outedgeit = dstnode->outEdges.iterator();
340 while (outedgeit->hasNext()) {
341 OrderEdge *outedge = outedgeit->next();
342 OrderNode *sink = outedge->sink;
343 //remove it from the sink node
344 sink->inEdges.remove(outedge);
345 //save the remapping that we did
346 dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
348 //create the new edge
349 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
351 newedge->polPos |= outedge->polPos;
352 newedge->polNeg |= outedge->polNeg;
353 newedge->mustPos |= outedge->mustPos;
354 newedge->mustNeg |= outedge->mustNeg;
355 newedge->pseudoPos |= outedge->pseudoPos;
356 //add new edge to both
357 sink->inEdges.add(newedge);
358 node->outEdges.add(newedge);
360 BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
361 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
362 updateEdgePolarity(benew, be);
363 solver->replaceBooleanWithBoolean(be, benew);
365 dstnode->outEdges.reset();
369 /* Mark destination as removed */
370 dstnode->removed = true;