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);
67 removeMustBeTrueNodes(solver, graph);
69 //This is needed for splitorder
70 computeStronglyConnectedComponentGraph(graph);
71 decomposeOrder(order, graph);
78 void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) {
79 Vector<Order *> ordervec;
80 Vector<Order *> partialcandidatevec;
81 uint size = currOrder->constraints.getSize();
82 for (uint i = 0; i < size; i++) {
83 BooleanOrder *orderconstraint = currOrder->constraints.get(i);
84 OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
85 OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
86 if (from->sccNum != to->sccNum) {
87 OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
90 solver->replaceBooleanWithTrue(orderconstraint);
91 } else if (edge->polNeg) {
92 solver->replaceBooleanWithFalse(orderconstraint);
94 //This case should only be possible if constraint isn't in AST
95 //This can happen, so don't do anything
99 OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
100 if (invedge != NULL) {
101 if (invedge->polPos) {
102 solver->replaceBooleanWithFalse(orderconstraint);
103 } else if (edge->polNeg) {
104 //This case shouldn't happen... If we have a partial order,
105 //then we should have our own edge...If we have a total
106 //order, then this edge should be positive...
109 //This case should only be possible if constraint isn't in AST
110 //This can happen, so don't do anything
116 //Build new order and change constraint's order
117 Order *neworder = NULL;
118 if (ordervec.getSize() > from->sccNum)
119 neworder = ordervec.get(from->sccNum);
120 if (neworder == NULL) {
121 MutableSet *set = solver->createMutableSet(currOrder->set->getType());
122 neworder = solver->createOrder(currOrder->type, set);
123 ordervec.setExpand(from->sccNum, neworder);
124 if (currOrder->type == SATC_PARTIAL)
125 partialcandidatevec.setExpand(from->sccNum, neworder);
127 partialcandidatevec.setExpand(from->sccNum, NULL);
129 if (from->status != ADDEDTOSET) {
130 from->status = ADDEDTOSET;
131 ((MutableSet *)neworder->set)->addElementMSet(from->id);
133 if (to->status != ADDEDTOSET) {
134 to->status = ADDEDTOSET;
135 ((MutableSet *)neworder->set)->addElementMSet(to->id);
137 if (currOrder->type == SATC_PARTIAL) {
138 OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
140 partialcandidatevec.setExpand(from->sccNum, NULL);
142 orderconstraint->order = neworder;
143 neworder->addOrderConstraint(orderconstraint);
146 currOrder->setOrderResolver( new DecomposeOrderResolver(currGraph, ordervec) );
147 solver->getActiveOrders()->remove(currOrder);
148 uint pcvsize = partialcandidatevec.getSize();
149 for (uint i = 0; i < pcvsize; i++) {
150 Order *neworder = partialcandidatevec.get(i);
151 if (neworder != NULL) {
152 neworder->type = SATC_TOTAL;