1 #include "ordergraph.h"
5 #include "ordergraph.h"
8 OrderGraph *allocOrderGraph(Order *order) {
9 OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
10 This->nodes = new HashSetOrderNode();
11 This->edges = new HashSetOrderEdge();
17 OrderGraph *buildOrderGraph(Order *order) {
18 OrderGraph *orderGraph = allocOrderGraph(order);
19 uint constrSize = order->constraints.getSize();
20 for (uint j = 0; j < constrSize; j++) {
21 addOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
26 //Builds only the subgraph for the must order graph.
27 OrderGraph *buildMustOrderGraph(Order *order) {
28 OrderGraph *orderGraph = allocOrderGraph(order);
29 uint constrSize = order->constraints.getSize();
30 for (uint j = 0; j < constrSize; j++) {
31 addMustOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
36 void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
37 Polarity polarity = constr->polarity;
38 BooleanValue mustval = constr->boolVal;
39 Order *order = graph->order;
43 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
44 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
45 _1to2->mustPos = true;
47 addNewOutgoingEdge(node1, _1to2);
48 addNewIncomingEdge(node2, _1to2);
49 if (constr->polarity == P_TRUE)
53 if (order->type == TOTAL) {
54 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
55 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
56 _2to1->mustPos = true;
58 addNewOutgoingEdge(node2, _2to1);
59 addNewIncomingEdge(node1, _2to1);
61 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
62 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
63 _1to2->mustNeg = true;
65 addNewOutgoingEdge(node1, _1to2);
66 addNewIncomingEdge(node2, _1to2);
71 //There is an unreachable order constraint if this assert fires
76 void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
77 BooleanValue mustval = constr->boolVal;
78 Order *order = graph->order;
82 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
83 _1to2->mustPos = true;
85 addNewOutgoingEdge(node1, _1to2);
86 addNewIncomingEdge(node2, _1to2);
87 if (constr->boolVal == BV_MUSTBETRUE)
90 case BV_MUSTBEFALSE: {
91 if (order->type == TOTAL) {
92 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
93 _2to1->mustPos = true;
95 addNewOutgoingEdge(node2, _2to1);
96 addNewIncomingEdge(node1, _2to1);
98 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
99 _1to2->mustNeg = true;
100 _1to2->polNeg = true;
101 addNewOutgoingEdge(node1, _1to2);
102 addNewIncomingEdge(node2, _1to2);
112 OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
113 OrderNode *node = allocOrderNode(id);
114 OrderNode *tmp = graph->nodes->get(node);
116 deleteOrderNode(node);
119 graph->nodes->add(node);
124 OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
125 OrderNode node = {id, NULL, NULL, NOTVISITED, 0};
126 OrderNode *tmp = graph->nodes->get(&node);
130 OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
131 OrderEdge *edge = allocOrderEdge(begin, end);
132 OrderEdge *tmp = graph->edges->get(edge);
134 deleteOrderEdge(edge);
137 graph->edges->add(edge);
142 OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
143 OrderEdge edge = {begin, end, 0, 0, 0, 0, 0};
144 OrderEdge *tmp = graph->edges->get(&edge);
148 OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
149 OrderEdge inverseedge = {edge->sink, edge->source, false, false, false, false, false};
150 OrderEdge *tmp = graph->edges->get(&inverseedge);
154 void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
155 OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
156 OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
157 addOrderEdge(graph, from, to, bOrder);
160 void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
161 OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
162 OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
163 addMustOrderEdge(graph, from, to, bOrder);
166 void deleteOrderGraph(OrderGraph *graph) {
167 HSIteratorOrderNode *iterator = graph->nodes->iterator();
168 while (iterator->hasNext()) {
169 OrderNode *node = iterator->next();
170 deleteOrderNode(node);
174 HSIteratorOrderEdge *eiterator = graph->edges->iterator();
175 while (eiterator->hasNext()) {
176 OrderEdge *edge = eiterator->next();
177 deleteOrderEdge(edge);