1 #include "ordergraph.h"
5 #include "ordergraph.h"
8 OrderGraph::OrderGraph(Order *_order) :
9 nodes(new HashsetOrderNode()),
10 edges(new HashsetOrderEdge()),
14 OrderGraph *buildOrderGraph(Order *order) {
15 OrderGraph *orderGraph = new OrderGraph(order);
16 uint constrSize = order->constraints.getSize();
17 for (uint j = 0; j < constrSize; j++) {
18 orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
23 //Builds only the subgraph for the must order graph.
24 OrderGraph *buildMustOrderGraph(Order *order) {
25 OrderGraph *orderGraph = new OrderGraph(order);
26 uint constrSize = order->constraints.getSize();
27 for (uint j = 0; j < constrSize; j++) {
28 orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
33 void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
34 Polarity polarity = constr->polarity;
35 BooleanValue mustval = constr->boolVal;
39 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
40 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
41 _1to2->mustPos = true;
43 node1->addNewOutgoingEdge(_1to2);
44 node2->addNewIncomingEdge(_1to2);
45 if (constr->polarity == P_TRUE)
49 if (order->type == SATC_TOTAL) {
50 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
51 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
52 _2to1->mustPos = true;
54 node2->addNewOutgoingEdge(_2to1);
55 node1->addNewIncomingEdge(_2to1);
57 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
58 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
59 _1to2->mustNeg = true;
61 node1->addNewOutgoingEdge(_1to2);
62 node2->addNewIncomingEdge(_1to2);
67 //There is an unreachable order constraint if this assert fires
72 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
73 BooleanValue mustval = constr->boolVal;
77 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
78 _1to2->mustPos = true;
80 node1->addNewOutgoingEdge(_1to2);
81 node2->addNewIncomingEdge(_1to2);
82 if (constr->boolVal == BV_MUSTBETRUE)
85 case BV_MUSTBEFALSE: {
86 if (order->type == SATC_TOTAL) {
87 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
88 _2to1->mustPos = true;
90 node2->addNewOutgoingEdge(_2to1);
91 node1->addNewIncomingEdge(_2to1);
93 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
94 _1to2->mustNeg = true;
96 node1->addNewOutgoingEdge(_1to2);
97 node2->addNewIncomingEdge(_1to2);
107 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
108 OrderNode *node = new OrderNode(id);
109 OrderNode *tmp = nodes->get(node);
119 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
121 OrderNode *tmp = nodes->get(&node);
125 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
126 OrderEdge *edge = new OrderEdge(begin, end);
127 OrderEdge *tmp = edges->get(edge);
137 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
138 OrderEdge edge(begin, end);
139 OrderEdge *tmp = edges->get(&edge);
143 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
144 OrderEdge inverseedge(edge->sink, edge->source);
145 OrderEdge *tmp = edges->get(&inverseedge);
149 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
150 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
151 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
152 addOrderEdge(from, to, bOrder);
155 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
156 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
157 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
158 addMustOrderEdge(from, to, bOrder);
161 OrderGraph::~OrderGraph() {
162 SetIteratorOrderNode *iterator = nodes->iterator();
163 while (iterator->hasNext()) {
164 OrderNode *node = iterator->next();
169 SetIteratorOrderEdge *eiterator = edges->iterator();
170 while (eiterator->hasNext()) {
171 OrderEdge *edge = eiterator->next();