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);
15 void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
16 Polarity polarity = constr->base.polarity;
17 BooleanValue mustval = constr->base.boolVal;
18 Order *order = graph->order;
22 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
23 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
24 _1to2->mustPos = true;
26 addNewOutgoingEdge(node1, _1to2);
27 addNewIncomingEdge(node2, _1to2);
28 if (constr->base.polarity == P_TRUE)
32 if (order->type == TOTAL) {
33 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
34 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
35 _2to1->mustPos = true;
37 addNewOutgoingEdge(node2, _2to1);
38 addNewIncomingEdge(node1, _2to1);
40 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
41 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
42 _1to2->mustNeg = true;
44 addNewOutgoingEdge(node1, _1to2);
45 addNewIncomingEdge(node2, _1to2);
50 //There is an unreachable order constraint if this assert fires
55 OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
56 OrderNode *node = allocOrderNode(id);
57 OrderNode *tmp = getHashSetOrderNode(graph->nodes, node);
59 deleteOrderNode(node);
62 addHashSetOrderNode(graph->nodes, node);
67 OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
68 OrderEdge *edge = allocOrderEdge(begin, end);
69 OrderEdge *tmp = getHashSetOrderEdge(graph->edges, edge);
71 deleteOrderEdge(edge);
74 addHashSetOrderEdge(graph->edges, edge);
79 OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
80 OrderEdge inverseedge = {edge->sink, edge->source, false, false, false, false, false};
81 OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &inverseedge);
85 void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
86 OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
87 OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
88 addOrderEdge(graph, from, to, bOrder);
91 void deleteOrderGraph(OrderGraph *graph) {
92 HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
93 while (hasNextOrderNode(iterator)) {
94 OrderNode *node = nextOrderNode(iterator);
95 deleteOrderNode(node);
97 deleteIterOrderNode(iterator);
99 HSIteratorOrderEdge *eiterator = iteratorOrderEdge(graph->edges);
100 while (hasNextOrderEdge(eiterator)) {
101 OrderEdge *edge = nextOrderEdge(eiterator);
102 deleteOrderEdge(edge);
104 deleteIterOrderEdge(eiterator);