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, Order* _order)
  19         :Transform(_solver),
  20         order(_order)
  21 {
  22 }
  23
  24 DecomposeOrderTransform::~DecomposeOrderTransform() {
  25 }
  26
  27 bool DecomposeOrderTransform::canExecuteTransform(){
  28         return canExecutePass(solver, order->type, DECOMPOSEORDER, &onoff);
  29 }
  30
  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);
  42                         if (edge->polPos) {
  43                                 solver->replaceBooleanWithTrue(orderconstraint);
  44                         } else if (edge->polNeg) {
  45                                 solver->replaceBooleanWithFalse(orderconstraint);
  46                         } else {
  47                                 //This case should only be possible if constraint isn't in AST
  48                                 ASSERT(0);
  49                         }
  50                 } else {
  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->getType());
  57                                 neworder = solver->createOrder(order->type, set);
  58                                 ordervec.setExpand(from->sccNum, neworder);
  59                                 if (order->type == PARTIAL)
  60                                         partialcandidatevec.setExpand(from->sccNum, neworder);
  61                                 else
  62                                         partialcandidatevec.setExpand(from->sccNum, NULL);
  63                         }
  64                         if (from->status != ADDEDTOSET) {
  65                                 from->status = ADDEDTOSET;
  66                                 ((MutableSet *)neworder->set)->addElementMSet(from->id);
  67                         }
  68                         if (to->status != ADDEDTOSET) {
  69                                 to->status = ADDEDTOSET;
  70                                 ((MutableSet *)neworder->set)->addElementMSet(to->id);
  71                         }
  72                         if (order->type == PARTIAL) {
  73                                 OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
  74                                 if (edge->polNeg)
  75                                         partialcandidatevec.setExpand(from->sccNum, NULL);
  76                         }
  77                         orderconstraint->order = neworder;
  78                         neworder->addOrderConstraint(orderconstraint);
  79                 }
  80         }
  81
  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);
  88                 }
  89         }
  90 }