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                 _1to2->polPos=true;
  25                 if (mustval==BV_MUSTBETRUE || mustval == BV_UNSAT)
  26                         _1to2->mustPos=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                         _2to1->polPos=true;
  36                         if (mustval==BV_MUSTBEFALSE || mustval == BV_UNSAT)
  37                                 _2to1->mustPos=true;
  38                         addNewOutgoingEdge(node2, _2to1);
  39                         addNewIncomingEdge(node1, _2to1);
  40                 } else {
  41                         OrderEdge* _1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
  42                         _1to2->polNeg=true;
  43                         if (mustval==BV_MUSTBEFALSE || mustval == BV_UNSAT)
  44                                 _1to2->mustNeg=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 void addOrderConstraintToOrderGraph(OrderGraph* graph, Boolean* constr) {
  81         BooleanOrder* bOrder = (BooleanOrder*) constr;
  82         OrderNode* from = getOrderNodeFromOrderGraph(graph, bOrder->first);
  83         OrderNode* to = getOrderNodeFromOrderGraph(graph, bOrder->second);
  84         addOrderEdge(graph, from, to, constr);
  85 }
  86
  87 void deleteOrderGraph(OrderGraph* graph){
  88         HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
  89         while(hasNextOrderNode(iterator)){
  90                 OrderNode* node = nextOrderNode(iterator);
  91                 deleteOrderNode(node);
  92         }
  93         deleteIterOrderNode(iterator);
  94
  95         HSIteratorOrderEdge* eiterator = iteratorOrderEdge(graph->edges);
  96         while(hasNextOrderEdge(eiterator)){
  97                 OrderEdge* edge = nextOrderEdge(eiterator);
  98                 deleteOrderEdge(edge);
  99         }
 100         deleteIterOrderEdge(eiterator);
 101         ourfree(graph);
 102 }