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 order->graph = orderGraph;
17 uint constrSize = order->constraints.getSize();
18 for (uint j = 0; j < constrSize; j++) {
19 orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
24 //Builds only the subgraph for the must order graph.
25 OrderGraph *buildMustOrderGraph(Order *order) {
26 OrderGraph *orderGraph = new OrderGraph(order);
27 uint constrSize = order->constraints.getSize();
28 for (uint j = 0; j < constrSize; j++) {
29 orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
34 void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
35 Polarity polarity = constr->polarity;
36 BooleanValue mustval = constr->boolVal;
40 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
41 if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
42 _1to2->mustPos = true;
44 node1->addNewOutgoingEdge(_1to2);
45 node2->addNewIncomingEdge(_1to2);
46 if (constr->polarity == P_TRUE)
50 if (order->type == SATC_TOTAL) {
51 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
52 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
53 _2to1->mustPos = true;
55 node2->addNewOutgoingEdge(_2to1);
56 node1->addNewIncomingEdge(_2to1);
58 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
59 if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
60 _1to2->mustNeg = true;
62 node1->addNewOutgoingEdge(_1to2);
63 node2->addNewIncomingEdge(_1to2);
68 //There is an unreachable order constraint if this assert fires
69 //Clients can easily do this, so don't do anything.
74 void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
75 BooleanValue mustval = constr->boolVal;
79 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
80 _1to2->mustPos = true;
82 node1->addNewOutgoingEdge(_1to2);
83 node2->addNewIncomingEdge(_1to2);
84 if (constr->boolVal == BV_MUSTBETRUE)
87 case BV_MUSTBEFALSE: {
88 if (order->type == SATC_TOTAL) {
89 OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
90 _2to1->mustPos = true;
92 node2->addNewOutgoingEdge(_2to1);
93 node1->addNewIncomingEdge(_2to1);
95 OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
96 _1to2->mustNeg = true;
98 node1->addNewOutgoingEdge(_1to2);
99 node2->addNewIncomingEdge(_1to2);
109 OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
110 OrderNode *node = new OrderNode(id);
111 OrderNode *tmp = nodes->get(node);
121 OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
123 OrderNode *tmp = nodes->get(&node);
127 OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
128 OrderEdge *edge = new OrderEdge(begin, end);
129 OrderEdge *tmp = edges->get(edge);
139 OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
140 OrderEdge edge(begin, end);
141 OrderEdge *tmp = edges->get(&edge);
145 OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
146 OrderEdge inverseedge(edge->sink, edge->source);
147 OrderEdge *tmp = edges->get(&inverseedge);
151 void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
152 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
153 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
154 addOrderEdge(from, to, bOrder);
157 void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
158 OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
159 OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
160 addMustOrderEdge(from, to, bOrder);
163 OrderGraph::~OrderGraph() {
164 SetIteratorOrderNode *iterator = nodes->iterator();
165 while (iterator->hasNext()) {
166 OrderNode *node = iterator->next();
171 SetIteratorOrderEdge *eiterator = edges->iterator();
172 while (eiterator->hasNext()) {
173 OrderEdge *edge = eiterator->next();
181 bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
182 HashsetOrderNode visited;
184 SetIteratorOrderEdge *iterator = source->outEdges.iterator();
186 while(iterator->hasNext()){
187 OrderNode* node = iterator->next()->sink;
188 if(!visited.contains(node)){
189 if( node == destination ){
194 found =isTherePathVisit(visited, node, destination);
204 bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination){
205 SetIteratorOrderEdge *iterator = current->outEdges.iterator();
207 while(iterator->hasNext()){
208 OrderNode* node = iterator->next()->sink;
209 if(node == destination){
214 if(isTherePathVisit(visited, node, destination)){