Small edit
[satune.git] / src / ASTTransform / decomposeordertransform.cc
1 /* 
2  * File:   ordertransform.cc
3  * Author: hamed
4  * 
5  * Created on August 28, 2017, 10:35 AM
6  */
7
8 #include "decomposeordertransform.h"
9 #include "order.h"
10 #include "orderedge.h"
11 #include "ordernode.h"
12 #include "boolean.h"
13 #include "mutableset.h"
14 #include "ordergraph.h"
15 #include "csolver.h"
16
17
18 DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver)
19         :Transform(_solver)
20 {
21 }
22
23 DecomposeOrderTransform::~DecomposeOrderTransform() {
24 }
25
26 bool DecomposeOrderTransform::canExecuteTransform(){
27         return canExecutePass(solver, currOrder->type, DECOMPOSEORDER, &onoff);
28 }
29
30 void DecomposeOrderTransform::doTransform(){
31         Vector<Order *> ordervec;
32         Vector<Order *> partialcandidatevec;
33         uint size = currOrder->constraints.getSize();
34         for (uint i = 0; i < size; i++) {
35                 BooleanOrder *orderconstraint = currOrder->constraints.get(i);
36                 OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
37                 OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
38                 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
39                 if (from->sccNum != to->sccNum) {
40                         OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
41                         if (edge->polPos) {
42                                 solver->replaceBooleanWithTrue(orderconstraint);
43                         } else if (edge->polNeg) {
44                                 solver->replaceBooleanWithFalse(orderconstraint);
45                         } else {
46                                 //This case should only be possible if constraint isn't in AST
47                                 ASSERT(0);
48                         }
49                 } else {
50                         //Build new order and change constraint's order
51                         Order *neworder = NULL;
52                         if (ordervec.getSize() > from->sccNum)
53                                 neworder = ordervec.get(from->sccNum);
54                         if (neworder == NULL) {
55                                 MutableSet *set = solver->createMutableSet(currOrder->set->getType());
56                                 neworder = solver->createOrder(currOrder->type, set);
57                                 ordervec.setExpand(from->sccNum, neworder);
58                                 if (currOrder->type == SATC_PARTIAL)
59                                         partialcandidatevec.setExpand(from->sccNum, neworder);
60                                 else
61                                         partialcandidatevec.setExpand(from->sccNum, NULL);
62                         }
63                         if (from->status != SATC_ADDEDTOSET) {
64                                 from->status = SATC_ADDEDTOSET;
65                                 ((MutableSet *)neworder->set)->addElementMSet(from->id);
66                         }
67                         if (to->status != SATC_ADDEDTOSET) {
68                                 to->status = SATC_ADDEDTOSET;
69                                 ((MutableSet *)neworder->set)->addElementMSet(to->id);
70                         }
71                         if (currOrder->type == SATC_PARTIAL) {
72                                 OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
73                                 if (edge->polNeg)
74                                         partialcandidatevec.setExpand(from->sccNum, NULL);
75                         }
76                         orderconstraint->order = neworder;
77                         neworder->addOrderConstraint(orderconstraint);
78                 }
79         }
80
81         uint pcvsize = partialcandidatevec.getSize();
82         for (uint i = 0; i < pcvsize; i++) {
83                 Order *neworder = partialcandidatevec.get(i);
84                 if (neworder != NULL) {
85                         neworder->type = SATC_TOTAL;
86                         model_print("i=%u\t", i);
87                 }
88         }
89 }