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, bool create) {
 109         OrderNode *node = new OrderNode(id);
 110         OrderNode *tmp = nodes->get(node);
 111         if ( tmp != NULL) {
 112                 delete node;
 113                 node = tmp;
 114         } else if (create) {
 115                 nodes->add(node);
 116         } else {
 117                 delete node;
 118                 return NULL;
 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, bool create) {
 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 if (create) {
 136                 edges->add(edge);
 137         } else {
 138                 delete edge;
 139                 return NULL;
 140         }
 141         return edge;
 142 }
 143
 144 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
 145         OrderEdge edge(begin, end);
 146         OrderEdge *tmp = edges->get(&edge);
 147         return tmp;
 148 }
 149
 150 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
 151         OrderEdge inverseedge(edge->sink, edge->source);
 152         OrderEdge *tmp = edges->get(&inverseedge);
 153         return tmp;
 154 }
 155
 156 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 157         OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 158         OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 159         addOrderEdge(from, to, bOrder);
 160 }
 161
 162 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 163         OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 164         OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 165         addMustOrderEdge(from, to, bOrder);
 166 }
 167
 168 OrderGraph::~OrderGraph() {
 169         SetIteratorOrderNode *iterator = nodes->iterator();
 170         while (iterator->hasNext()) {
 171                 OrderNode *node = iterator->next();
 172                 delete node;
 173         }
 174         delete iterator;
 175
 176         SetIteratorOrderEdge *eiterator = edges->iterator();
 177         while (eiterator->hasNext()) {
 178                 OrderEdge *edge = eiterator->next();
 179                 delete edge;
 180         }
 181         delete eiterator;
 182         delete nodes;
 183         delete edges;
 184 }