src/Translator/decomposeorderresolver.cc

   1
   2 /*
   3  * File:   DecomposeOrderResolver.cc
   4  * Author: hamed
   5  *
   6  * Created on September 1, 2017, 10:36 AM
   7  */
   8
   9 #include "decomposeorderresolver.h"
  10 #include "order.h"
  11 #include "ordernode.h"
  12 #include "ordergraph.h"
  13
  14 DecomposeOrderResolver::DecomposeOrderResolver(Order *_order) :
  15         graph(NULL),
  16         order(_order)
  17 {
  18 }
  19
  20 DecomposeOrderResolver::~DecomposeOrderResolver() {
  21         if (graph != NULL)
  22                 delete graph;
  23         edges.resetAndDelete();
  24 }
  25
  26 void DecomposeOrderResolver::mustOrderEdge(uint64_t first, uint64_t second) {
  27         DOREdge edge(first, second, 0, first, second);
  28         if (!edges.contains(&edge)) {
  29                 DOREdge *newedge = new DOREdge(first, second, 0, first, second);
  30                 edges.add(newedge);
  31         }
  32 }
  33
  34 void DecomposeOrderResolver::remapEdge(uint64_t first, uint64_t second, uint64_t newfirst, uint64_t newsecond) {
  35         DOREdge edge(first, second, 0, first, second);
  36         DOREdge *oldedge = edges.get(&edge);
  37         if (oldedge != NULL) {
  38                 edges.remove(oldedge);
  39                 oldedge->newfirst = newfirst;
  40                 oldedge->newsecond = newsecond;
  41                 edges.add(oldedge);
  42         } else {
  43                 DOREdge *newedge = new DOREdge(first, second, 0, newfirst, newsecond);
  44                 edges.add(newedge);
  45         }
  46 }
  47
  48 void DecomposeOrderResolver::setEdgeOrder(uint64_t first, uint64_t second, uint sccNum) {
  49         DOREdge edge(first, second, 0, first, second);
  50         DOREdge *oldedge = edges.get(&edge);
  51         if (oldedge != NULL) {
  52                 oldedge->orderindex = sccNum;
  53         } else {
  54                 DOREdge *newedge = new DOREdge(first, second, sccNum, first, second);
  55                 edges.add(newedge);
  56         }
  57 }
  58
  59 void DecomposeOrderResolver::setOrder(uint sccNum, Order *neworder) {
  60         orders.setExpand(sccNum, neworder);
  61 }
  62
  63 Order *DecomposeOrderResolver::getOrder(uint sccNum) {
  64         Order *neworder = NULL;
  65         if (orders.getSize() > sccNum)
  66                 neworder = orders.get(sccNum);
  67         return neworder;
  68 }
  69
  70 void DecomposeOrderResolver::buildGraph() {
  71         graph = new OrderGraph(order);
  72         SetIteratorDOREdge *iterator = edges.iterator();
  73         while (iterator->hasNext()) {
  74                 DOREdge *doredge = iterator->next();
  75                 if (doredge->orderindex == 0) {
  76                         graph->addEdge(doredge->origfirst, doredge->origsecond);
  77                 } else {
  78                         Order *suborder = orders.get(doredge->orderindex);
  79                         bool isEdge = suborder->encoding.resolver->resolveOrder(doredge->newfirst, doredge->newsecond);
  80                         if (isEdge)
  81                                 graph->addEdge(doredge->origfirst, doredge->origsecond);
  82                         else if (order->type == SATC_TOTAL)
  83                                 graph->addEdge(doredge->origsecond, doredge->origfirst);
  84                 }
  85         }
  86         delete iterator;
  87         if (order->type == SATC_TOTAL) {
  88                 graph->computeStronglyConnectedComponentGraph();
  89         }
  90 }
  91
  92 bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
  93         if (graph == NULL)
  94                 buildGraph();
  95
  96         OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
  97         if (from == NULL) {
  98                 ASSERT(order->type != SATC_TOTAL);
  99                 return false;
 100         }
 101         OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
 102         if (to == NULL) {
 103                 ASSERT(order->type != SATC_TOTAL);
 104                 return false;
 105         }
 106         switch (order->type) {
 107         case SATC_TOTAL:
 108                 return from->sccNum < to->sccNum;
 109         case SATC_PARTIAL:
 110                 return resolvePartialOrder(from, to);
 111         default:
 112                 ASSERT(0);
 113         }
 114 }
 115
 116 bool DecomposeOrderResolver::resolvePartialOrder(OrderNode *first, OrderNode *second) {
 117         if (first->sccNum > second->sccNum) {
 118                 return false;
 119         } else {
 120                 return graph->isTherePath(first, second);
 121         }
 122 }
 123