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)
23 DecomposeOrderTransform::~DecomposeOrderTransform() {
26 bool DecomposeOrderTransform::canExecuteTransform(){
27 return canExecutePass(solver, currOrder->type, DECOMPOSEORDER, &onoff);
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);
42 solver->replaceBooleanWithTrue(orderconstraint);
43 } else if (edge->polNeg) {
44 solver->replaceBooleanWithFalse(orderconstraint);
46 //This case should only be possible if constraint isn't in AST
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);
61 partialcandidatevec.setExpand(from->sccNum, NULL);
63 if (from->status != ADDEDTOSET) {
64 from->status = ADDEDTOSET;
65 ((MutableSet *)neworder->set)->addElementMSet(from->id);
67 if (to->status != ADDEDTOSET) {
68 to->status = ADDEDTOSET;
69 ((MutableSet *)neworder->set)->addElementMSet(to->id);
71 if (currOrder->type == SATC_PARTIAL) {
72 OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
74 partialcandidatevec.setExpand(from->sccNum, NULL);
76 orderconstraint->order = neworder;
77 neworder->addOrderConstraint(orderconstraint);
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);