src/ASTAnalyses/ordergraph.cc

   1 #include "ordergraph.h"
   2 #include "ordernode.h"
   3 #include "boolean.h"
   4 #include "orderedge.h"
   5 #include "ordergraph.h"
   6 #include "order.h"
   7
   8 OrderGraph::OrderGraph(Order *_order) :
   9         nodes(new HashSetOrderNode()),
  10         edges(new HashSetOrderEdge()),
  11         order(_order) {
  12 }
  13
  14 OrderGraph *buildOrderGraph(Order *order) {
  15         OrderGraph *orderGraph = new OrderGraph(order);
  16         uint constrSize = order->constraints.getSize();
  17         for (uint j = 0; j < constrSize; j++) {
  18                 orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
  19         }
  20         return orderGraph;
  21 }
  22
  23 //Builds only the subgraph for the must order graph.
  24 OrderGraph *buildMustOrderGraph(Order *order) {
  25         OrderGraph *orderGraph = new OrderGraph(order);
  26         uint constrSize = order->constraints.getSize();
  27         for (uint j = 0; j < constrSize; j++) {
  28                 orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
  29         }
  30         return orderGraph;
  31 }
  32
  33 void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  34         Polarity polarity = constr->polarity;
  35         BooleanValue mustval = constr->boolVal;
  36         switch (polarity) {
  37         case P_BOTHTRUEFALSE:
  38         case P_TRUE: {
  39                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  40                 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
  41                         _1to2->mustPos = true;
  42                 _1to2->polPos = true;
  43                 node1->addNewOutgoingEdge(_1to2);
  44                 node2->addNewIncomingEdge(_1to2);
  45                 if (constr->polarity == P_TRUE)
  46                         break;
  47         }
  48         case P_FALSE: {
  49                 if (order->type == SATC_TOTAL) {
  50                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
  51                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  52                                 _2to1->mustPos = true;
  53                         _2to1->polPos = true;
  54                         node2->addNewOutgoingEdge(_2to1);
  55                         node1->addNewIncomingEdge(_2to1);
  56                 } else {
  57                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  58                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  59                                 _1to2->mustNeg = true;
  60                         _1to2->polNeg = true;
  61                         node1->addNewOutgoingEdge(_1to2);
  62                         node2->addNewIncomingEdge(_1to2);
  63                 }
  64                 break;
  65         }
  66         case P_UNDEFINED:
  67                 //There is an unreachable order constraint if this assert fires
  68                 ASSERT(0);
  69         }
  70 }
  71
  72 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  73         BooleanValue mustval = constr->boolVal;
  74         switch (mustval) {
  75         case BV_UNSAT:
  76         case BV_MUSTBETRUE: {
  77                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  78                 _1to2->mustPos = true;
  79                 _1to2->polPos = true;
  80                 node1->addNewOutgoingEdge(_1to2);
  81                 node2->addNewIncomingEdge(_1to2);
  82                 if (constr->boolVal == BV_MUSTBETRUE)
  83                         break;
  84         }
  85         case BV_MUSTBEFALSE: {
  86                 if (order->type == SATC_TOTAL) {
  87                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
  88                         _2to1->mustPos = true;
  89                         _2to1->polPos = true;
  90                         node2->addNewOutgoingEdge(_2to1);
  91                         node1->addNewIncomingEdge(_2to1);
  92                 } else {
  93                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  94                         _1to2->mustNeg = true;
  95                         _1to2->polNeg = true;
  96                         node1->addNewOutgoingEdge(_1to2);
  97                         node2->addNewIncomingEdge(_1to2);
  98                 }
  99                 break;
 100         }
 101         case BV_UNDEFINED:
 102                 //Do Nothing
 103                 break;
 104         }
 105 }
 106
 107 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
 108         OrderNode *node = new OrderNode(id);
 109         OrderNode *tmp = nodes->get(node);
 110         if ( tmp != NULL) {
 111                 delete node;
 112                 node = tmp;
 113         } else {
 114                 nodes->add(node);
 115         }
 116         return node;
 117 }
 118
 119 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
 120         OrderNode node(id);
 121         OrderNode *tmp = nodes->get(&node);
 122         return tmp;
 123 }
 124
 125 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
 126         OrderEdge *edge = new OrderEdge(begin, end);
 127         OrderEdge *tmp = edges->get(edge);
 128         if ( tmp != NULL ) {
 129                 delete edge;
 130                 edge = tmp;
 131         } else {
 132                 edges->add(edge);
 133         }
 134         return edge;
 135 }
 136
 137 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
 138         OrderEdge edge(begin, end);
 139         OrderEdge *tmp = edges->get(&edge);
 140         return tmp;
 141 }
 142
 143 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
 144         OrderEdge inverseedge(edge->sink, edge->source);
 145         OrderEdge *tmp = edges->get(&inverseedge);
 146         return tmp;
 147 }
 148
 149 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 150         OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 151         OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 152         addOrderEdge(from, to, bOrder);
 153 }
 154
 155 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 156         OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 157         OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 158         addMustOrderEdge(from, to, bOrder);
 159 }
 160
 161 OrderGraph::~OrderGraph() {
 162         SetIteratorOrderNode *iterator = nodes->iterator();
 163         while (iterator->hasNext()) {
 164                 OrderNode *node = iterator->next();
 165                 delete node;
 166         }
 167         delete iterator;
 168
 169         SetIteratorOrderEdge *eiterator = edges->iterator();
 170         while (eiterator->hasNext()) {
 171                 OrderEdge *edge = eiterator->next();
 172                 delete edge;
 173         }
 174         delete eiterator;
 175         delete nodes;
 176         delete edges;
 177 }