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
68 //Clients can easily do this, so don't do anything.
73 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
74 BooleanValue mustval = constr->boolVal;
78 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
79 _1to2->mustPos = true;
81 node1->addNewOutgoingEdge(_1to2);
82 node2->addNewIncomingEdge(_1to2);
83 if (constr->boolVal == BV_MUSTBETRUE)
86 case BV_MUSTBEFALSE: {
87 if (order->type == SATC_TOTAL) {
88 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
89 _2to1->mustPos = true;
91 node2->addNewOutgoingEdge(_2to1);
92 node1->addNewIncomingEdge(_2to1);
94 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
95 _1to2->mustNeg = true;
97 node1->addNewOutgoingEdge(_1to2);
98 node2->addNewIncomingEdge(_1to2);
108 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
109 OrderNode *node = new OrderNode(id);
110 OrderNode *tmp = nodes->get(node);
120 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
122 OrderNode *tmp = nodes->get(&node);
126 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
127 OrderEdge *edge = new OrderEdge(begin, end);
128 OrderEdge *tmp = edges->get(edge);
138 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
139 OrderEdge edge(begin, end);
140 OrderEdge *tmp = edges->get(&edge);
144 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
145 OrderEdge inverseedge(edge->sink, edge->source);
146 OrderEdge *tmp = edges->get(&inverseedge);
150 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
151 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
152 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
153 addOrderEdge(from, to, bOrder);
156 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
157 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
158 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
159 addMustOrderEdge(from, to, bOrder);
162 OrderGraph::~OrderGraph() {
163 SetIteratorOrderNode *iterator = nodes->iterator();
164 while (iterator->hasNext()) {
165 OrderNode *node = iterator->next();
170 SetIteratorOrderEdge *eiterator = edges->iterator();
171 while (eiterator->hasNext()) {
172 OrderEdge *edge = eiterator->next();