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();
16 OrderGraph *buildOrderGraph(Order *order) {
17 OrderGraph *orderGraph = allocOrderGraph(order);
18 uint constrSize = order->constraints.getSize();
19 for (uint j = 0; j < constrSize; j++) {
20 addOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
25 //Builds only the subgraph for the must order graph.
26 OrderGraph *buildMustOrderGraph(Order *order) {
27 OrderGraph *orderGraph = allocOrderGraph(order);
28 uint constrSize = order->constraints.getSize();
29 for (uint j = 0; j < constrSize; j++) {
30 addMustOrderConstraintToOrderGraph(orderGraph, order->constraints.get(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 node1->addNewOutgoingEdge(_1to2);
47 node2->addNewIncomingEdge(_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 node2->addNewOutgoingEdge(_2to1);
58 node1->addNewIncomingEdge(_2to1);
60 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
61 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
62 _1to2->mustNeg = true;
64 node1->addNewOutgoingEdge(_1to2);
65 node2->addNewIncomingEdge(_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 node1->addNewOutgoingEdge(_1to2);
85 node2->addNewIncomingEdge(_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 node2->addNewOutgoingEdge(_2to1);
95 node1->addNewIncomingEdge(_2to1);
97 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
98 _1to2->mustNeg = true;
100 node1->addNewOutgoingEdge(_1to2);
101 node2->addNewIncomingEdge(_1to2);
111 OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
112 OrderNode *node = new OrderNode(id);
113 OrderNode *tmp = graph->nodes->get(node);
118 graph->nodes->add(node);
123 OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
125 OrderNode *tmp = graph->nodes->get(&node);
129 OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
130 OrderEdge *edge = new OrderEdge(begin, end);
131 OrderEdge *tmp = graph->edges->get(edge);
136 graph->edges->add(edge);
141 OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
142 OrderEdge edge(begin, end);
143 OrderEdge *tmp = graph->edges->get(&edge);
147 OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
148 OrderEdge inverseedge(edge->sink, edge->source);
149 OrderEdge *tmp = graph->edges->get(&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 = graph->nodes->iterator();
167 while (iterator->hasNext()) {
168 OrderNode *node = iterator->next();
173 HSIteratorOrderEdge *eiterator = graph->edges->iterator();
174 while (eiterator->hasNext()) {
175 OrderEdge *edge = eiterator->next();