src/ASTTransform/orderdecompose.cc

   1 #include "orderdecompose.h"
   2 #include "common.h"
   3 #include "order.h"
   4 #include "boolean.h"
   5 #include "ordergraph.h"
   6 #include "ordernode.h"
   7 #include "rewriter.h"
   8 #include "orderedge.h"
   9 #include "mutableset.h"
  10 #include "ops.h"
  11 #include "csolver.h"
  12
  13 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
  14         Vector<Order *> ordervec;
  15         Vector<Order *> partialcandidatevec;
  16         uint size = order->constraints.getSize();
  17         for (uint i = 0; i < size; i++) {
  18                 BooleanOrder *orderconstraint = order->constraints.get(i);
  19                 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
  20                 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
  21                 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
  22                 if (from->sccNum != to->sccNum) {
  23                         OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
  24                         if (edge->polPos) {
  25                                 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
  26                         } else if (edge->polNeg) {
  27                                 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
  28                         } else {
  29                                 //This case should only be possible if constraint isn't in AST
  30                                 ASSERT(0);
  31                         }
  32                 } else {
  33                         //Build new order and change constraint's order
  34                         Order *neworder = NULL;
  35                         if (ordervec.getSize() > from->sccNum)
  36                                 neworder = ordervec.get(from->sccNum);
  37                         if (neworder == NULL) {
  38                                 MutableSet *set = new MutableSet(order->set->type);
  39                                 neworder = new Order(order->type, set);
  40                                 This->allOrders.push(neworder);
  41                                 ordervec.setExpand(from->sccNum, neworder);
  42                                 if (order->type == PARTIAL)
  43                                         partialcandidatevec.setExpand(from->sccNum, neworder);
  44                                 else
  45                                         partialcandidatevec.setExpand(from->sccNum, NULL);
  46                         }
  47                         if (from->status != ADDEDTOSET) {
  48                                 from->status = ADDEDTOSET;
  49                                 ((MutableSet *)neworder->set)->addElementMSet(from->id);
  50                         }
  51                         if (to->status != ADDEDTOSET) {
  52                                 to->status = ADDEDTOSET;
  53                                 ((MutableSet *)neworder->set)->addElementMSet(to->id);
  54                         }
  55                         if (order->type == PARTIAL) {
  56                                 OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
  57                                 if (edge->polNeg)
  58                                         partialcandidatevec.setExpand(from->sccNum, NULL);
  59                         }
  60                         orderconstraint->order = neworder;
  61                         neworder->addOrderConstraint(orderconstraint);
  62                 }
  63         }
  64
  65         uint pcvsize=partialcandidatevec.getSize();
  66         for(uint i=0;i<pcvsize;i++) {
  67                 Order * neworder=partialcandidatevec.get(i);
  68                 if (neworder != NULL){
  69                         neworder->type = TOTAL;
  70                         model_print("i=%u\t", i);
  71                 }
  72         }
  73 }
  74