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