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);
11 This->edges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
16 OrderGraph *buildOrderGraph(Order *order) {
17 OrderGraph *orderGraph = allocOrderGraph(order);
18 uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
19 for (uint j = 0; j < constrSize; j++) {
20 addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
25 //Builds only the subgraph for the must order graph.
26 OrderGraph *buildMustOrderGraph(Order *order) {
27 OrderGraph *orderGraph = allocOrderGraph(order);
28 uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
29 for (uint j = 0; j < constrSize; j++) {
30 addMustOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
35 void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
36 Polarity polarity = constr->polarity;
37 BooleanValue mustval = constr->boolVal;
38 Order *order = graph->order;
42 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
43 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
44 _1to2->mustPos = true;
46 addNewOutgoingEdge(node1, _1to2);
47 addNewIncomingEdge(node2, _1to2);
48 if (constr->polarity == P_TRUE)
52 if (order->type == TOTAL) {
53 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
54 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
55 _2to1->mustPos = true;
57 addNewOutgoingEdge(node2, _2to1);
58 addNewIncomingEdge(node1, _2to1);
60 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
61 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
62 _1to2->mustNeg = true;
64 addNewOutgoingEdge(node1, _1to2);
65 addNewIncomingEdge(node2, _1to2);
70 //There is an unreachable order constraint if this assert fires
75 void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
76 BooleanValue mustval = constr->boolVal;
77 Order *order = graph->order;
81 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
82 _1to2->mustPos = true;
84 addNewOutgoingEdge(node1, _1to2);
85 addNewIncomingEdge(node2, _1to2);
86 if (constr->boolVal == BV_MUSTBETRUE)
89 case BV_MUSTBEFALSE: {
90 if (order->type == TOTAL) {
91 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
92 _2to1->mustPos = true;
94 addNewOutgoingEdge(node2, _2to1);
95 addNewIncomingEdge(node1, _2to1);
97 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
98 _1to2->mustNeg = true;
100 addNewOutgoingEdge(node1, _1to2);
101 addNewIncomingEdge(node2, _1to2);
111 OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
112 OrderNode *node = allocOrderNode(id);
113 OrderNode *tmp = getHashSetOrderNode(graph->nodes, node);
115 deleteOrderNode(node);
118 addHashSetOrderNode(graph->nodes, node);
123 OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
124 OrderNode node = {id, NULL, NULL, NOTVISITED, 0};
125 OrderNode *tmp = getHashSetOrderNode(graph->nodes, &node);
129 OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
130 OrderEdge *edge = allocOrderEdge(begin, end);
131 OrderEdge *tmp = getHashSetOrderEdge(graph->edges, edge);
133 deleteOrderEdge(edge);
136 addHashSetOrderEdge(graph->edges, edge);
141 OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
142 OrderEdge edge = {begin, end, 0, 0, 0, 0, 0};
143 OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &edge);
147 OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
148 OrderEdge inverseedge = {edge->sink, edge->source, false, false, false, false, false};
149 OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &inverseedge);
153 void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
154 OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
155 OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
156 addOrderEdge(graph, from, to, bOrder);
159 void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
160 OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
161 OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
162 addMustOrderEdge(graph, from, to, bOrder);
165 void deleteOrderGraph(OrderGraph *graph) {
166 HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
167 while (hasNextOrderNode(iterator)) {
168 OrderNode *node = nextOrderNode(iterator);
169 deleteOrderNode(node);
171 deleteIterOrderNode(iterator);
173 HSIteratorOrderEdge *eiterator = iteratorOrderEdge(graph->edges);
174 while (hasNextOrderEdge(eiterator)) {
175 OrderEdge *edge = nextOrderEdge(eiterator);
176 deleteOrderEdge(edge);
178 deleteIterOrderEdge(eiterator);
179 deleteHashSetOrderNode(graph->nodes);
180 deleteHashSetOrderEdge(graph->edges);