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                 //Clients can easily do this, so don't do anything.
  69                 ;
  70         }
  71 }
  72
  73 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  74         BooleanValue mustval = constr->boolVal;
  75         switch (mustval) {
  76         case BV_UNSAT:
  77         case BV_MUSTBETRUE: {
  78                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  79                 _1to2->mustPos = true;
  80                 _1to2->polPos = true;
  81                 node1->addNewOutgoingEdge(_1to2);
  82                 node2->addNewIncomingEdge(_1to2);
  83                 if (constr->boolVal == BV_MUSTBETRUE)
  84                         break;
  85         }
  86         case BV_MUSTBEFALSE: {
  87                 if (order->type == SATC_TOTAL) {
  88                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
  89                         _2to1->mustPos = true;
  90                         _2to1->polPos = true;
  91                         node2->addNewOutgoingEdge(_2to1);
  92                         node1->addNewIncomingEdge(_2to1);
  93                 } else {
  94                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
  95                         _1to2->mustNeg = true;
  96                         _1to2->polNeg = true;
  97                         node1->addNewOutgoingEdge(_1to2);
  98                         node2->addNewIncomingEdge(_1to2);
  99                 }
 100                 break;
 101         }
 102         case BV_UNDEFINED:
 103                 //Do Nothing
 104                 break;
 105         }
 106 }
 107
 108 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
 109         OrderNode *node = new OrderNode(id);
 110         OrderNode *tmp = nodes->get(node);
 111         if ( tmp != NULL) {
 112                 delete node;
 113                 node = tmp;
 114         } else {
 115                 nodes->add(node);
 116         }
 117         return node;
 118 }
 119
 120 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
 121         OrderNode node(id);
 122         OrderNode *tmp = nodes->get(&node);
 123         return tmp;
 124 }
 125
 126 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
 127         OrderEdge *edge = new OrderEdge(begin, end);
 128         OrderEdge *tmp = edges->get(edge);
 129         if ( tmp != NULL ) {
 130                 delete edge;
 131                 edge = tmp;
 132         } else {
 133                 edges->add(edge);
 134         }
 135         return edge;
 136 }
 137
 138 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
 139         OrderEdge edge(begin, end);
 140         OrderEdge *tmp = edges->get(&edge);
 141         return tmp;
 142 }
 143
 144 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
 145         OrderEdge inverseedge(edge->sink, edge->source);
 146         OrderEdge *tmp = edges->get(&inverseedge);
 147         return tmp;
 148 }
 149
 150 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 151         OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 152         OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 153         addOrderEdge(from, to, bOrder);
 154 }
 155
 156 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 157         OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 158         OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 159         addMustOrderEdge(from, to, bOrder);
 160 }
 161
 162 OrderGraph::~OrderGraph() {
 163         SetIteratorOrderNode *iterator = nodes->iterator();
 164         while (iterator->hasNext()) {
 165                 OrderNode *node = iterator->next();
 166                 delete node;
 167         }
 168         delete iterator;
 169
 170         SetIteratorOrderEdge *eiterator = edges->iterator();
 171         while (eiterator->hasNext()) {
 172                 OrderEdge *edge = eiterator->next();
 173                 delete edge;
 174         }
 175         delete eiterator;
 176         delete nodes;
 177         delete edges;
 178 }