src/Encoders/ordergraph.c

   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 void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
  17         Polarity polarity = constr->base.polarity;
  18         BooleanValue mustval = constr->base.boolVal;
  19         Order *order = graph->order;
  20         switch (polarity) {
  21         case P_BOTHTRUEFALSE:
  22         case P_TRUE: {
  23                 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
  24                 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
  25                         _1to2->mustPos = true;
  26                 _1to2->polPos = true;
  27                 addNewOutgoingEdge(node1, _1to2);
  28                 addNewIncomingEdge(node2, _1to2);
  29                 if (constr->base.polarity == P_TRUE)
  30                         break;
  31         }
  32         case P_FALSE: {
  33                 if (order->type == TOTAL) {
  34                         OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
  35                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  36                                 _2to1->mustPos = true;
  37                         _2to1->polPos = true;
  38                         addNewOutgoingEdge(node2, _2to1);
  39                         addNewIncomingEdge(node1, _2to1);
  40                 } else {
  41                         OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
  42                         if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
  43                                 _1to2->mustNeg = true;
  44                         _1to2->polNeg = true;
  45                         addNewOutgoingEdge(node1, _1to2);
  46                         addNewIncomingEdge(node2, _1to2);
  47                 }
  48                 break;
  49         }
  50         case P_UNDEFINED:
  51                 //There is an unreachable order constraint if this assert fires
  52                 ASSERT(0);
  53         }
  54 }
  55
  56 OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
  57         OrderNode *node = allocOrderNode(id);
  58         OrderNode *tmp = getHashSetOrderNode(graph->nodes, node);
  59         if ( tmp != NULL) {
  60                 deleteOrderNode(node);
  61                 node = tmp;
  62         } else {
  63                 addHashSetOrderNode(graph->nodes, node);
  64         }
  65         return node;
  66 }
  67
  68 OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
  69         OrderEdge *edge = allocOrderEdge(begin, end);
  70         OrderEdge *tmp = getHashSetOrderEdge(graph->edges, edge);
  71         if ( tmp != NULL ) {
  72                 deleteOrderEdge(edge);
  73                 edge = tmp;
  74         } else {
  75                 addHashSetOrderEdge(graph->edges, edge);
  76         }
  77         return edge;
  78 }
  79
  80 OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
  81         OrderEdge inverseedge = {edge->sink, edge->source, false, false, false, false, false};
  82         OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &inverseedge);
  83         return tmp;
  84 }
  85
  86 void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
  87         OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
  88         OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
  89         addOrderEdge(graph, from, to, bOrder);
  90 }
  91
  92 void deleteOrderGraph(OrderGraph *graph) {
  93         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
  94         while (hasNextOrderNode(iterator)) {
  95                 OrderNode *node = nextOrderNode(iterator);
  96                 deleteOrderNode(node);
  97         }
  98         deleteIterOrderNode(iterator);
  99
 100         HSIteratorOrderEdge *eiterator = iteratorOrderEdge(graph->edges);
 101         while (hasNextOrderEdge(eiterator)) {
 102                 OrderEdge *edge = nextOrderEdge(eiterator);
 103                 deleteOrderEdge(edge);
 104         }
 105         deleteIterOrderEdge(eiterator);
 106         ourfree(graph);
 107 }