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 ASSERT(order->graph == NULL);
16 OrderGraph *orderGraph = new OrderGraph(order);
17 order->graph = orderGraph;
18 uint constrSize = order->constraints.getSize();
19 for (uint j = 0; j < constrSize; j++) {
20 orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
25 //Builds only the subgraph for the must order graph.
26 OrderGraph *buildMustOrderGraph(Order *order) {
27 ASSERT(order->graph == NULL);
28 OrderGraph *orderGraph = new OrderGraph(order);
29 uint constrSize = order->constraints.getSize();
30 for (uint j = 0; j < constrSize; j++) {
31 orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
36 void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
37 Polarity polarity = constr->polarity;
38 BooleanValue mustval = constr->boolVal;
42 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(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 == SATC_TOTAL) {
53 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( 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(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
71 //Clients can easily do this, so don't do anything.
76 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
77 BooleanValue mustval = constr->boolVal;
81 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(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 == SATC_TOTAL) {
91 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
92 _2to1->mustPos = true;
94 node2->addNewOutgoingEdge(_2to1);
95 node1->addNewIncomingEdge(_2to1);
97 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
98 _1to2->mustNeg = true;
100 node1->addNewOutgoingEdge(_1to2);
101 node2->addNewIncomingEdge(_1to2);
111 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
112 OrderNode *node = new OrderNode(id);
113 OrderNode *tmp = nodes->get(node);
123 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
125 OrderNode *tmp = nodes->get(&node);
129 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
130 OrderEdge *edge = new OrderEdge(begin, end);
131 OrderEdge *tmp = edges->get(edge);
141 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
142 OrderEdge edge(begin, end);
143 OrderEdge *tmp = edges->get(&edge);
147 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
148 OrderEdge inverseedge(edge->sink, edge->source);
149 OrderEdge *tmp = edges->get(&inverseedge);
153 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
154 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
155 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
156 addOrderEdge(from, to, bOrder);
159 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
160 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
161 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
162 addMustOrderEdge(from, to, bOrder);
165 OrderGraph::~OrderGraph() {
166 SetIteratorOrderNode *iterator = nodes->iterator();
167 while (iterator->hasNext()) {
168 OrderNode *node = iterator->next();
173 SetIteratorOrderEdge *eiterator = edges->iterator();
174 while (eiterator->hasNext()) {
175 OrderEdge *edge = eiterator->next();
183 bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
184 HashsetOrderNode visited;
186 SetIteratorOrderEdge *iterator = source->outEdges.iterator();
188 while (iterator->hasNext()) {
189 OrderEdge *edge = iterator->next();
191 OrderNode *node = edge->sink;
192 if (!visited.contains(node)) {
193 if ( node == destination ) {
198 found = isTherePathVisit(visited, node, destination);
209 bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination) {
210 SetIteratorOrderEdge *iterator = current->outEdges.iterator();
212 while (iterator->hasNext()) {
213 OrderEdge *edge = iterator->next();
215 OrderNode *node = edge->sink;
216 if (node == destination) {
221 if (isTherePathVisit(visited, node, destination)) {