src/Encoders/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 *allocOrderGraph(Order *order) {
   9         OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
  10         This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
  11         This->edges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
  12         This->order = order;
  13         return This;
  14 }
  15
  16 OrderGraph *buildOrderGraph(Order *order) {
  17         OrderGraph *orderGraph = allocOrderGraph(order);
  18         uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
  19         for (uint j = 0; j < constrSize; j++) {
  20                 addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
  21         }
  22         return orderGraph;
  23 }
  24
  25 //Builds only the subgraph for the must order graph.
  26 OrderGraph *buildMustOrderGraph(Order *order) {
  27         OrderGraph *orderGraph = allocOrderGraph(order);
  28         uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
  29         for (uint j = 0; j < constrSize; j++) {
  30                 addMustOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
  31         }
  32         return orderGraph;
  33 }
  34
  35 void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  36         Polarity polarity = constr->base.polarity;
  37         BooleanValue mustval = constr->base.boolVal;
  38         Order *order = graph->order;
  39         switch (polarity) {
  40         case P_BOTHTRUEFALSE:
  41         case P_TRUE: {
  42                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
  43                 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
  44                         _1to2->mustPos = true;
  45                 _1to2->polPos = true;
  46                 addNewOutgoingEdge(node1, _1to2);
  47                 addNewIncomingEdge(node2, _1to2);
  48                 if (constr->base.polarity == P_TRUE)
  49                         break;
  50         }
  51         case P_FALSE: {
  52                 if (order->type == TOTAL) {
  53                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
  54                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  55                                 _2to1->mustPos = true;
  56                         _2to1->polPos = true;
  57                         addNewOutgoingEdge(node2, _2to1);
  58                         addNewIncomingEdge(node1, _2to1);
  59                 } else {
  60                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
  61                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  62                                 _1to2->mustNeg = true;
  63                         _1to2->polNeg = true;
  64                         addNewOutgoingEdge(node1, _1to2);
  65                         addNewIncomingEdge(node2, _1to2);
  66                 }
  67                 break;
  68         }
  69         case P_UNDEFINED:
  70                 //There is an unreachable order constraint if this assert fires
  71                 ASSERT(0);
  72         }
  73 }
  74
  75 void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  76         BooleanValue mustval = constr->base.boolVal;
  77         Order *order = graph->order;
  78         switch (mustval) {
  79         case BV_UNSAT:
  80         case BV_MUSTBETRUE: {
  81                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
  82                 _1to2->mustPos = true;
  83                 _1to2->polPos = true;
  84                 addNewOutgoingEdge(node1, _1to2);
  85                 addNewIncomingEdge(node2, _1to2);
  86                 if (constr->base.boolVal == BV_MUSTBETRUE)
  87                         break;
  88         }
  89         case BV_MUSTBEFALSE: {
  90                 if (order->type == TOTAL) {
  91                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
  92                         _2to1->mustPos = true;
  93                         _2to1->polPos = true;
  94                         addNewOutgoingEdge(node2, _2to1);
  95                         addNewIncomingEdge(node1, _2to1);
  96                 } else {
  97                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
  98                         _1to2->mustNeg = true;
  99                         _1to2->polNeg = true;
 100                         addNewOutgoingEdge(node1, _1to2);
 101                         addNewIncomingEdge(node2, _1to2);
 102                 }
 103                 break;
 104         }
 105         case BV_UNDEFINED:
 106                 //Do Nothing
 107                 break;
 108         }
 109 }
 110
 111 OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
 112         OrderNode *node = allocOrderNode(id);
 113         OrderNode *tmp = getHashSetOrderNode(graph->nodes, node);
 114         if ( tmp != NULL) {
 115                 deleteOrderNode(node);
 116                 node = tmp;
 117         } else {
 118                 addHashSetOrderNode(graph->nodes, node);
 119         }
 120         return node;
 121 }
 122
 123 OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
 124         OrderNode node = {id, NULL, NULL, NOTVISITED, 0};
 125         OrderNode *tmp = getHashSetOrderNode(graph->nodes, &node);
 126         return tmp;
 127 }
 128
 129 OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
 130         OrderEdge *edge = allocOrderEdge(begin, end);
 131         OrderEdge *tmp = getHashSetOrderEdge(graph->edges, edge);
 132         if ( tmp != NULL ) {
 133                 deleteOrderEdge(edge);
 134                 edge = tmp;
 135         } else {
 136                 addHashSetOrderEdge(graph->edges, edge);
 137         }
 138         return edge;
 139 }
 140
 141 OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
 142         OrderEdge edge = {begin, end, 0, 0, 0, 0, 0};
 143         OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &edge);
 144         return tmp;
 145 }
 146
 147 OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
 148         OrderEdge inverseedge = {edge->sink, edge->source, false, false, false, false, false};
 149         OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &inverseedge);
 150         return tmp;
 151 }
 152
 153 void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
 154         OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
 155         OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
 156         addOrderEdge(graph, from, to, bOrder);
 157 }
 158
 159 void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
 160         OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
 161         OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
 162         addMustOrderEdge(graph, from, to, bOrder);
 163 }
 164
 165 void deleteOrderGraph(OrderGraph *graph) {
 166         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
 167         while (hasNextOrderNode(iterator)) {
 168                 OrderNode *node = nextOrderNode(iterator);
 169                 deleteOrderNode(node);
 170         }
 171         deleteIterOrderNode(iterator);
 172
 173         HSIteratorOrderEdge *eiterator = iteratorOrderEdge(graph->edges);
 174         while (hasNextOrderEdge(eiterator)) {
 175                 OrderEdge *edge = nextOrderEdge(eiterator);
 176                 deleteOrderEdge(edge);
 177         }
 178         deleteIterOrderEdge(eiterator);
 179         deleteHashSetOrderNode(graph->nodes);
 180         deleteHashSetOrderEdge(graph->edges);
 181         ourfree(graph);
 182 }