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 }