+void DecomposeOrderTransform::doTransform() {
+ HashsetOrder *orders = solver->getActiveOrders()->copy();
+ SetIteratorOrder * orderit=orders->iterator();
+ while(orderit->hasNext()) {
+ Order *order = orderit->next();
+
+ if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
+ continue;
+ }
+
+ OrderGraph *graph = buildOrderGraph(order);
+ if (order->type == SATC_PARTIAL) {
+ //Required to do SCC analysis for partial order graphs. It
+ //makes sure we don't incorrectly optimize graphs with negative
+ //polarity edges
+ completePartialOrderGraph(graph);
+ }
+
+ bool mustReachGlobal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHGLOBAL, &onoff);
+
+ if (mustReachGlobal)
+ reachMustAnalysis(solver, graph, false);
+
+ bool mustReachLocal = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHLOCAL, &onoff);
+
+ if (mustReachLocal) {
+ //This pair of analysis is also optional
+ if (order->type == SATC_PARTIAL) {
+ localMustAnalysisPartial(solver, graph);
+ } else {
+ localMustAnalysisTotal(solver, graph);
+ }
+ }
+
+
+ bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
+
+ if (mustReachPrune)
+ removeMustBeTrueNodes(solver, graph);
+
+ //This is needed for splitorder
+ computeStronglyConnectedComponentGraph(graph);
+ decomposeOrder(order, graph);
+ }
+ delete orderit;
+ delete orders;