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