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"
18 DecomposeOrderTransform::DecomposeOrderTransform(CSolver* _solver, Order* _order)
24 DecomposeOrderTransform::~DecomposeOrderTransform() {
27 bool DecomposeOrderTransform::canExecuteTransform(){
28 return canExecutePass(solver, order->type, DECOMPOSEORDER, &onoff);
31 void DecomposeOrderTransform::doTransform(){
32 Vector<Order *> ordervec;
33 Vector<Order *> partialcandidatevec;
34 uint size = order->constraints.getSize();
35 for (uint i = 0; i < size; i++) {
36 BooleanOrder *orderconstraint = order->constraints.get(i);
37 OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
38 OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
39 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
40 if (from->sccNum != to->sccNum) {
41 OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
43 solver->replaceBooleanWithTrue(orderconstraint);
44 } else if (edge->polNeg) {
45 solver->replaceBooleanWithFalse(orderconstraint);
47 //This case should only be possible if constraint isn't in AST
51 //Build new order and change constraint's order
52 Order *neworder = NULL;
53 if (ordervec.getSize() > from->sccNum)
54 neworder = ordervec.get(from->sccNum);
55 if (neworder == NULL) {
56 MutableSet *set = solver->createMutableSet(order->set->type);
57 neworder = solver->createOrder(order->type, set);
58 ordervec.setExpand(from->sccNum, neworder);
59 if (order->type == PARTIAL)
60 partialcandidatevec.setExpand(from->sccNum, neworder);
62 partialcandidatevec.setExpand(from->sccNum, NULL);
64 if (from->status != ADDEDTOSET) {
65 from->status = ADDEDTOSET;
66 ((MutableSet *)neworder->set)->addElementMSet(from->id);
68 if (to->status != ADDEDTOSET) {
69 to->status = ADDEDTOSET;
70 ((MutableSet *)neworder->set)->addElementMSet(to->id);
72 if (order->type == PARTIAL) {
73 OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
75 partialcandidatevec.setExpand(from->sccNum, NULL);
77 orderconstraint->order = neworder;
78 neworder->addOrderConstraint(orderconstraint);
82 uint pcvsize = partialcandidatevec.getSize();
83 for (uint i = 0; i < pcvsize; i++) {
84 Order *neworder = partialcandidatevec.get(i);
85 if (neworder != NULL) {
86 neworder->type = TOTAL;
87 model_print("i=%u\t", i);