1 #include "ordergraph.h"
5 #include "ordergraph.h"
8 OrderGraph* allocOrderGraph(Order *order) {
9 OrderGraph* This = (OrderGraph*) ourmalloc(sizeof(OrderGraph));
10 This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
12 initDefVectorOrderNode(&This->scc);
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;
23 OrderEdge* _1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
24 if (mustval==BV_MUSTBETRUE || mustval == BV_UNSAT)
25 _1to2->mustPos = true;
27 addNewOutgoingEdge(node1, _1to2);
28 addNewIncomingEdge(node2, _1to2);
29 if(constr->polarity == P_TRUE)
33 if (order->type==TOTAL) {
34 OrderEdge* _2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
35 if (mustval==BV_MUSTBEFALSE || mustval == BV_UNSAT)
36 _2to1->mustPos = true;
38 addNewOutgoingEdge(node2, _2to1);
39 addNewIncomingEdge(node1, _2to1);
41 OrderEdge* _1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
42 if (mustval==BV_MUSTBEFALSE || mustval == BV_UNSAT)
43 _1to2->mustNeg = true;
45 addNewOutgoingEdge(node1, _1to2);
46 addNewIncomingEdge(node2, _1to2);
51 //There is an unreachable order constraint if this assert fires
56 OrderNode* getOrderNodeFromOrderGraph(OrderGraph* graph, uint64_t id) {
57 OrderNode* node = allocOrderNode(id);
58 OrderNode* tmp = getHashSetOrderNode(graph->nodes, node);
60 deleteOrderNode(node);
63 addHashSetOrderNode(graph->nodes, node);
68 OrderEdge* getOrderEdgeFromOrderGraph(OrderGraph* graph, OrderNode* begin, OrderNode* end) {
69 OrderEdge* edge = allocOrderEdge(begin, end);
70 OrderEdge* tmp = getHashSetOrderEdge(graph->edges, edge);
72 deleteOrderEdge(edge);
75 addHashSetOrderEdge(graph->edges, edge);
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);
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);
93 void deleteOrderGraph(OrderGraph* graph){
94 HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
95 while(hasNextOrderNode(iterator)){
96 OrderNode* node = nextOrderNode(iterator);
97 deleteOrderNode(node);
99 deleteIterOrderNode(iterator);
101 HSIteratorOrderEdge* eiterator = iteratorOrderEdge(graph->edges);
102 while(hasNextOrderEdge(eiterator)){
103 OrderEdge* edge = nextOrderEdge(eiterator);
104 deleteOrderEdge(edge);
106 deleteIterOrderEdge(eiterator);