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         initDefVectorOrderNode(&This->scc);
  13         return This;
  14 }
  15
  16 void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean* constr) {
  17         Polarity polarity=constr->polarity;
  18         BooleanValue mustval=constr->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->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, Boolean* constr) {
  87         BooleanOrder* bOrder = (BooleanOrder*) constr;
  88         OrderNode* from = getOrderNodeFromOrderGraph(graph, bOrder->first);
  89         OrderNode* to = getOrderNodeFromOrderGraph(graph, bOrder->second);
  90         addOrderEdge(graph, from, to, constr);
  91 }
  92
  93 void deleteOrderGraph(OrderGraph* graph){
  94         HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
  95         while(hasNextOrderNode(iterator)){
  96                 OrderNode* node = nextOrderNode(iterator);
  97                 deleteOrderNode(node);
  98         }
  99         deleteIterOrderNode(iterator);
 100
 101         HSIteratorOrderEdge* eiterator = iteratorOrderEdge(graph->edges);
 102         while(hasNextOrderEdge(eiterator)){
 103                 OrderEdge* edge = nextOrderEdge(eiterator);
 104                 deleteOrderEdge(edge);
 105         }
 106         deleteIterOrderEdge(eiterator);
 107         ourfree(graph);
 108 }