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 OrderGraph *graph = buildOrderGraph(order);
40 if (order->type == SATC_PARTIAL) {
41 //Required to do SCC analysis for partial order graphs. It
42 //makes sure we don't incorrectly optimize graphs with negative
44 completePartialOrderGraph(graph);
47 bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
50 reachMustAnalysis(solver, graph, false);
52 bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
55 //This pair of analysis is also optional
56 if (order->type == SATC_PARTIAL) {
57 localMustAnalysisPartial(solver, graph);
59 localMustAnalysisTotal(solver, graph);
64 bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
65 HashsetOrderEdge *edgesRemoved = NULL;
68 edgesRemoved = new HashsetOrderEdge();
69 removeMustBeTrueNodes(graph, edgesRemoved);
72 //This is needed for splitorder
73 computeStronglyConnectedComponentGraph(graph);
74 decomposeOrder(order, graph, edgesRemoved);
75 if (edgesRemoved != NULL)
83 void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved) {
84 Vector<Order *> ordervec;
85 Vector<Order *> partialcandidatevec;
86 uint size = currOrder->constraints.getSize();
87 for (uint i = 0; i < size; i++) {
88 BooleanOrder *orderconstraint = currOrder->constraints.get(i);
89 OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
90 OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
91 OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
92 OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
93 if (edgesRemoved != NULL) {
94 if (edgesRemoved->contains(edge)) {
95 solver->replaceBooleanWithTrue(orderconstraint);
97 } else if (edgesRemoved->contains(invedge)) {
98 solver->replaceBooleanWithFalse(orderconstraint);
103 if (from->sccNum != to->sccNum) {
106 solver->replaceBooleanWithTrue(orderconstraint);
107 } else if (edge->polNeg) {
108 solver->replaceBooleanWithFalse(orderconstraint);
110 //This case should only be possible if constraint isn't in AST
111 //This can happen, so don't do anything
115 if (invedge != NULL) {
116 if (invedge->polPos) {
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 if (ordervec.getSize() > from->sccNum)
134 neworder = ordervec.get(from->sccNum);
135 if (neworder == NULL) {
136 MutableSet *set = solver->createMutableSet(currOrder->set->getType());
137 neworder = solver->createOrder(currOrder->type, set);
138 ordervec.setExpand(from->sccNum, neworder);
139 if (currOrder->type == SATC_PARTIAL)
140 partialcandidatevec.setExpand(from->sccNum, neworder);
142 partialcandidatevec.setExpand(from->sccNum, NULL);
144 if (from->status != ADDEDTOSET) {
145 from->status = ADDEDTOSET;
146 ((MutableSet *)neworder->set)->addElementMSet(from->id);
148 if (to->status != ADDEDTOSET) {
149 to->status = ADDEDTOSET;
150 ((MutableSet *)neworder->set)->addElementMSet(to->id);
152 if (currOrder->type == SATC_PARTIAL) {
154 partialcandidatevec.setExpand(from->sccNum, NULL);
156 orderconstraint->order = neworder;
157 neworder->addOrderConstraint(orderconstraint);
160 currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
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, HashsetOrderEdge *edgesRemoved) {
194 SetIteratorOrderEdge *iterin = node->inEdges.iterator();
195 while (iterin->hasNext()) {
196 OrderEdge *inEdge = iterin->next();
197 OrderNode *srcNode = inEdge->source;
198 srcNode->outEdges.remove(inEdge);
199 edgesRemoved->add(inEdge);
200 SetIteratorOrderEdge *iterout = node->outEdges.iterator();
201 while (iterout->hasNext()) {
202 OrderEdge *outEdge = iterout->next();
203 OrderNode *sinkNode = outEdge->sink;
204 sinkNode->inEdges.remove(outEdge);
205 edgesRemoved->add(outEdge);
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);
231 void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {
232 SetIteratorOrderNode *iterator = graph->getNodes();
233 while (iterator->hasNext()) {
234 OrderNode *node = iterator->next();
235 if (isMustBeTrueNode(node)) {
236 bypassMustBeTrueNode(graph, node, edgesRemoved);