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 if (solver->isUnSAT())
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 Vector<BooleanOrder *> *constraints = currOrder->getConstraints();
92 uint size = constraints->getSize();
93 for (uint i = 0; i < size; i++) {
94 BooleanOrder *orderconstraint = constraints->get(i);
95 OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
96 OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
97 OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
98 OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
99 if (from->removed || to->removed)
102 if (from->sccNum != to->sccNum) {
105 dor->mustOrderEdge(from->getID(), to->getID());
106 solver->replaceBooleanWithTrue(orderconstraint);
107 } else if (edge->polNeg) {
108 if (currOrder->type == SATC_TOTAL)
109 dor->mustOrderEdge(to->getID(), from->getID());
110 solver->replaceBooleanWithFalse(orderconstraint);
112 //This case should only be possible if constraint isn't in AST
113 //This can happen, so don't do anything
117 if (invedge != NULL) {
118 if (invedge->polPos) {
119 dor->mustOrderEdge(to->getID(), from->getID());
120 solver->replaceBooleanWithFalse(orderconstraint);
121 } else if (edge->polNeg) {
122 //This case shouldn't happen... If we have a partial order,
123 //then we should have our own edge...If we have a total
124 //order, then this edge should be positive...
127 //This case should only be possible if constraint isn't in AST
128 //This can happen, so don't do anything
134 //Build new order and change constraint's order
135 Order *neworder = NULL;
136 neworder = dor->getOrder(from->sccNum);
137 if (neworder == NULL) {
138 MutableSet *set = solver->createMutableSet(currOrder->set->getType());
139 neworder = solver->createOrder(currOrder->type, set);
140 dor->setOrder(from->sccNum, neworder);
141 if (currOrder->type == SATC_PARTIAL)
142 partialcandidatevec.setExpand(from->sccNum, neworder);
144 partialcandidatevec.setExpand(from->sccNum, NULL);
146 if (from->status != ADDEDTOSET) {
147 from->status = ADDEDTOSET;
148 ((MutableSet *)neworder->set)->addElementMSet(from->id);
150 if (to->status != ADDEDTOSET) {
151 to->status = ADDEDTOSET;
152 ((MutableSet *)neworder->set)->addElementMSet(to->id);
154 if (currOrder->type == SATC_PARTIAL) {
156 partialcandidatevec.setExpand(from->sccNum, NULL);
158 BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
159 solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
160 updateEdgePolarity(neworderconstraint, orderconstraint);
161 dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
164 solver->getActiveOrders()->remove(currOrder);
165 uint pcvsize = partialcandidatevec.getSize();
166 for (uint i = 0; i < pcvsize; i++) {
167 Order *neworder = partialcandidatevec.get(i);
168 if (neworder != NULL) {
169 neworder->type = SATC_TOTAL;
174 bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) {
175 SetIteratorOrderEdge *iterator = node->inEdges.iterator();
176 while (iterator->hasNext()) {
177 OrderEdge *edge = iterator->next();
178 if (!edge->mustPos) {
184 iterator = node->outEdges.iterator();
185 while (iterator->hasNext()) {
186 OrderEdge *edge = iterator->next();
187 if (!edge->mustPos) {
196 void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
197 node->removed = true;
198 SetIteratorOrderEdge *iterin = node->inEdges.iterator();
199 while (iterin->hasNext()) {
200 OrderEdge *inEdge = iterin->next();
201 OrderNode *srcNode = inEdge->source;
202 srcNode->outEdges.remove(inEdge);
203 dor->mustOrderEdge(srcNode->getID(), node->getID());
204 BooleanEdge be = solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID());
205 solver->replaceBooleanWithTrue(be);
207 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
208 while (iterout->hasNext()) {
209 OrderEdge *outEdge = iterout->next();
210 OrderNode *sinkNode = outEdge->sink;
211 //Adding new edge to new sink and src nodes ...
212 if (srcNode == sinkNode) {
218 //Add new order constraint
219 BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
220 updateEdgePolarity(orderconstraint, P_TRUE);
221 solver->addConstraint(orderconstraint);
224 OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
225 newEdge->mustPos = true;
226 newEdge->polPos = true;
227 if (newEdge->mustNeg)
229 srcNode->outEdges.add(newEdge);
230 sinkNode->inEdges.add(newEdge);
236 //Clean up old edges... Keep this later in case we don't have any in edges
237 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
238 while (iterout->hasNext()) {
239 OrderEdge *outEdge = iterout->next();
240 OrderNode *sinkNode = outEdge->sink;
241 dor->mustOrderEdge(node->getID(), sinkNode->getID());
242 sinkNode->inEdges.remove(outEdge);
243 BooleanEdge be2 = solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
244 solver->replaceBooleanWithTrue(be2);
249 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
250 SetIteratorOrderNode *iterator = graph->getNodes();
251 while (iterator->hasNext()) {
252 OrderNode *node = (OrderNode *)iterator->next();
255 if (isMustBeTrueNode(node)) {
256 bypassMustBeTrueNode(graph, node, dor);
262 void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
263 SetIteratorOrderNode *iterator = graph->getNodes();
264 while (iterator->hasNext()) {
265 OrderNode *node = (OrderNode *)iterator->next();
268 attemptNodeMerge(graph, node, dor);
273 void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
274 SetIteratorOrderEdge *edgeit = node->outEdges.iterator();
275 while (edgeit->hasNext()) {
276 OrderEdge *outedge = edgeit->next();
277 //Only eliminate must edges
278 if (!outedge->mustPos)
280 OrderNode *dstnode = outedge->sink;
281 uint numOutEdges = node->outEdges.getSize();
282 uint numInEdges = dstnode->inEdges.getSize();
284 Need to avoid a situation where we create new reachability by
285 the merge. This can only happen if there is an extra in edge to
286 the dstnode and an extra out edge to our node.
289 if (numOutEdges == 1 || numInEdges == 1) {
290 /* Safe to do the Merge */
291 mergeNodes(graph, node, outedge, dstnode, dor);
293 //Throw away the iterator and start over
295 edgeit = node->outEdges.iterator();
301 void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
302 /* Fix up must edge between the two nodes */
303 node->outEdges.remove(edge);
304 dstnode->inEdges.remove(edge);
305 dor->mustOrderEdge(node->getID(), dstnode->getID());
307 BooleanEdge be = solver->orderConstraint(graph->getOrder(), node->getID(), dstnode->getID());
308 solver->replaceBooleanWithTrue(be);
310 /* Go through the incoming edges to the new node */
311 SetIteratorOrderEdge *inedgeit = dstnode->inEdges.iterator();
312 while (inedgeit->hasNext()) {
313 OrderEdge *inedge = inedgeit->next();
314 OrderNode *source = inedge->source;
315 //remove it from the source node
316 source->outEdges.remove(inedge);
317 //save the remapping that we did
318 dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
319 //create the new edge
320 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(source, node);
322 newedge->polPos |= inedge->polPos;
323 newedge->polNeg |= inedge->polNeg;
324 newedge->mustPos |= inedge->mustPos;
325 newedge->mustNeg |= inedge->mustNeg;
326 newedge->pseudoPos |= inedge->pseudoPos;
327 //add new edge to both
328 source->outEdges.add(newedge);
329 node->inEdges.add(newedge);
331 BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
332 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
333 updateEdgePolarity(benew, be);
334 if (solver->isTrue(benew))
335 solver->replaceBooleanWithTrue(be);
336 else if (solver->isFalse(benew))
337 solver->replaceBooleanWithFalse(be);
339 solver->replaceBooleanWithBoolean(be, benew);
341 dstnode->inEdges.reset();
344 /* Go through the outgoing edges from the new node */
345 SetIteratorOrderEdge *outedgeit = dstnode->outEdges.iterator();
346 while (outedgeit->hasNext()) {
347 OrderEdge *outedge = outedgeit->next();
348 OrderNode *sink = outedge->sink;
349 //remove it from the sink node
350 sink->inEdges.remove(outedge);
351 //save the remapping that we did
352 dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
354 //create the new edge
355 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(node, sink);
357 newedge->polPos |= outedge->polPos;
358 newedge->polNeg |= outedge->polNeg;
359 newedge->mustPos |= outedge->mustPos;
360 newedge->mustNeg |= outedge->mustNeg;
361 newedge->pseudoPos |= outedge->pseudoPos;
362 //add new edge to both
363 sink->inEdges.add(newedge);
364 node->outEdges.add(newedge);
366 BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
367 BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
368 updateEdgePolarity(benew, be);
369 if (solver->isTrue(benew))
370 solver->replaceBooleanWithTrue(be);
371 else if (solver->isFalse(benew))
372 solver->replaceBooleanWithFalse(be);
374 solver->replaceBooleanWithBoolean(be, benew);
376 dstnode->outEdges.reset();
380 /* Mark destination as removed */
381 dstnode->removed = true;