#include "order.h"
OrderGraph::OrderGraph(Order *_order) :
- nodes(new HashSetOrderNode()),
- edges(new HashSetOrderEdge()),
+ nodes(new HashsetOrderNode()),
+ edges(new HashsetOrderEdge()),
order(_order) {
}
OrderGraph *buildOrderGraph(Order *order) {
OrderGraph *orderGraph = new OrderGraph(order);
+ order->graph = orderGraph;
uint constrSize = order->constraints.getSize();
for (uint j = 0; j < constrSize; j++) {
orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
break;
}
case P_FALSE: {
- if (order->type == TOTAL) {
+ if (order->type == SATC_TOTAL) {
OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
_2to1->mustPos = true;
}
case P_UNDEFINED:
//There is an unreachable order constraint if this assert fires
- ASSERT(0);
+ //Clients can easily do this, so don't do anything.
+ ;
}
}
break;
}
case BV_MUSTBEFALSE: {
- if (order->type == TOTAL) {
+ if (order->type == SATC_TOTAL) {
OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
_2to1->mustPos = true;
_2to1->polPos = true;
}
OrderGraph::~OrderGraph() {
- HSIteratorOrderNode *iterator = nodes->iterator();
+ SetIteratorOrderNode *iterator = nodes->iterator();
while (iterator->hasNext()) {
OrderNode *node = iterator->next();
delete node;
}
delete iterator;
- HSIteratorOrderEdge *eiterator = edges->iterator();
+ SetIteratorOrderEdge *eiterator = edges->iterator();
while (eiterator->hasNext()) {
OrderEdge *edge = eiterator->next();
delete edge;
delete nodes;
delete edges;
}
+
+bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
+ HashsetOrderNode visited;
+ visited.add(source);
+ SetIteratorOrderEdge *iterator = source->outEdges.iterator();
+ bool found = false;
+ while(iterator->hasNext()){
+ OrderNode* node = iterator->next()->sink;
+ if(!visited.contains(node)){
+ if( node == destination ){
+ found = true;
+ break;
+ }
+ visited.add(node);
+ found =isTherePathVisit(visited, node, destination);
+ if(found){
+ break;
+ }
+ }
+ }
+ delete iterator;
+ return found;
+}
+
+bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination){
+ SetIteratorOrderEdge *iterator = current->outEdges.iterator();
+ bool found = false;
+ while(iterator->hasNext()){
+ OrderNode* node = iterator->next()->sink;
+ if(node == destination){
+ found = true;
+ break;
+ }
+ visited.add(node);
+ if(isTherePathVisit(visited, node, destination)){
+ found = true;
+ break;
+ }
+ }
+ delete iterator;
+ return found;
+}