1 #include "orderdecompose.h"
5 #include "ordergraph.h"
9 #include "mutableset.h"
12 #include "orderencoder.h"
14 #include "integerencoding.h"
16 void orderAnalysis(CSolver *This) {
17 uint size = This->allOrders.getSize();
18 for (uint i = 0; i < size; i++) {
19 Order *order = This->allOrders.get(i);
20 bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
24 OrderGraph *graph = buildOrderGraph(order);
25 if (order->type == PARTIAL) {
26 //Required to do SCC analysis for partial order graphs. It
27 //makes sure we don't incorrectly optimize graphs with negative
29 completePartialOrderGraph(graph);
33 bool mustReachGlobal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHGLOBAL, &onoff);
36 reachMustAnalysis(This, graph, false);
38 bool mustReachLocal=GETVARTUNABLE(This->tuner, order->type, MUSTREACHLOCAL, &onoff);
41 //This pair of analysis is also optional
42 if (order->type == PARTIAL) {
43 localMustAnalysisPartial(This, graph);
45 localMustAnalysisTotal(This, graph);
49 bool mustReachPrune=GETVARTUNABLE(This->tuner, order->type, MUSTREACHPRUNE, &onoff);
52 removeMustBeTrueNodes(This, graph);
54 //This is needed for splitorder
55 computeStronglyConnectedComponentGraph(graph);
56 decomposeOrder(This, order, graph);
57 deleteOrderGraph(graph);
59 bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &onoff );
60 if(!doIntegerEncoding)
62 uint size = order->constraints.getSize();
63 for(uint i=0; i<size; i++){
64 orderIntegerEncodingSATEncoder(This->satEncoder, order->constraints.get(i));
70 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
71 Vector<Order *> ordervec;
72 Vector<Order *> partialcandidatevec;
73 uint size = order->constraints.getSize();
74 for (uint i = 0; i < size; i++) {
75 BooleanOrder *orderconstraint = order->constraints.get(i);
76 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
77 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
78 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
79 if (from->sccNum != to->sccNum) {
80 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
82 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
83 } else if (edge->polNeg) {
84 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
86 //This case should only be possible if constraint isn't in AST
90 //Build new order and change constraint's order
91 Order *neworder = NULL;
92 if (ordervec.getSize() > from->sccNum)
93 neworder = ordervec.get(from->sccNum);
94 if (neworder == NULL) {
95 MutableSet *set = new MutableSet(order->set->type);
96 This->allSets.push(set);
97 neworder = new Order(order->type, set);
98 This->allOrders.push(neworder);
99 ordervec.setExpand(from->sccNum, neworder);
100 if (order->type == PARTIAL)
101 partialcandidatevec.setExpand(from->sccNum, neworder);
103 partialcandidatevec.setExpand(from->sccNum, NULL);
105 if (from->status != ADDEDTOSET) {
106 from->status = ADDEDTOSET;
107 ((MutableSet *)neworder->set)->addElementMSet(from->id);
109 if (to->status != ADDEDTOSET) {
110 to->status = ADDEDTOSET;
111 ((MutableSet *)neworder->set)->addElementMSet(to->id);
113 if (order->type == PARTIAL) {
114 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
116 partialcandidatevec.setExpand(from->sccNum, NULL);
118 orderconstraint->order = neworder;
119 neworder->addOrderConstraint(orderconstraint);
123 uint pcvsize=partialcandidatevec.getSize();
124 for(uint i=0;i<pcvsize;i++) {
125 Order * neworder=partialcandidatevec.get(i);
126 if (neworder != NULL){
127 neworder->type = TOTAL;
128 model_print("i=%u\t", i);