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 if (solver->isTrue(benew))
332 solver->replaceBooleanWithTrue(be);
333 else if (solver->isFalse(benew))
334 solver->replaceBooleanWithFalse(be);
336 solver->replaceBooleanWithBoolean(be, benew);
338 dstnode->inEdges.reset();
341 /* Go through the outgoing edges from the new node */
342 SetIteratorOrderEdge *outedgeit = dstnode->outEdges.iterator();
343 while (outedgeit->hasNext()) {
344 OrderEdge *outedge = outedgeit->next();
345 OrderNode *sink = outedge->sink;
346 //remove it from the sink node
347 sink->inEdges.remove(outedge);
348 //save the remapping that we did
349 dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
351 //create the new edge
352 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
354 newedge->polPos |= outedge->polPos;
355 newedge->polNeg |= outedge->polNeg;
356 newedge->mustPos |= outedge->mustPos;
357 newedge->mustNeg |= outedge->mustNeg;
358 newedge->pseudoPos |= outedge->pseudoPos;
359 //add new edge to both
360 sink->inEdges.add(newedge);
361 node->outEdges.add(newedge);
363 BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
364 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
365 updateEdgePolarity(benew, be);
366 if (solver->isTrue(benew))
367 solver->replaceBooleanWithTrue(be);
368 else if (solver->isFalse(benew))
369 solver->replaceBooleanWithFalse(be);
371 solver->replaceBooleanWithBoolean(be, benew);
373 dstnode->outEdges.reset();
377 /* Mark destination as removed */
378 dstnode->removed = true;