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