OrderNode* sinkNode = outEdge->sink;
sinkNode->inEdges.remove(outEdge);
//Adding new edge to new sink and src nodes ...
- OrderEdge *newEdge =getOrderEdgeFromOrderGraph(graph, srcNode, sinkNode);
+ OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
newEdge->mustPos = true;
newEdge->polPos = true;
if (newEdge->mustNeg)
while(iterator->hasNext()) {
OrderNode* node = iterator->next();
if(isMustBeTrueNode(node)){
- bypassMustBeTrueNode(This,graph, node);
+ bypassMustBeTrueNode(This, graph, node);
}
}
delete iterator;
ASSERT(parent != rnode);
if (edge->polNeg && parent->sccNum != rnode->sccNum &&
sources->contains(parent)) {
- OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, rnode, parent);
+ OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent);
newedge->pseudoPos = true;
}
}
HSIteratorOrderNode *srciterator = sources->iterator();
while (srciterator->hasNext()) {
OrderNode *srcnode = srciterator->next();
- OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
+ OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
newedge->mustPos = true;
newedge->polPos = true;
if (newedge->mustNeg)
while (iterator->hasNext()) {
OrderEdge *edge = iterator->next();
if (edge->mustPos) {
- OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
+ OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
if (invEdge != NULL) {
if (!invEdge->mustPos) {
invEdge->polPos = false;
} else
solver->unsat = true;
- OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
+ OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
if (invEdge != NULL) {
if (!invEdge->mustPos)
invEdge->polPos = false;
#include "ordergraph.h"
#include "order.h"
-OrderGraph *allocOrderGraph(Order *order) {
- OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
- This->nodes = new HashSetOrderNode();
- This->edges = new HashSetOrderEdge();
- This->order = order;
- return This;
+OrderGraph::OrderGraph(Order *_order) :
+ nodes(new HashSetOrderNode()),
+ edges(new HashSetOrderEdge()),
+ order(_order) {
}
OrderGraph *buildOrderGraph(Order *order) {
- OrderGraph *orderGraph = allocOrderGraph(order);
+ OrderGraph *orderGraph = new OrderGraph(order);
uint constrSize = order->constraints.getSize();
for (uint j = 0; j < constrSize; j++) {
- addOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
+ orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
}
return orderGraph;
}
//Builds only the subgraph for the must order graph.
OrderGraph *buildMustOrderGraph(Order *order) {
- OrderGraph *orderGraph = allocOrderGraph(order);
+ OrderGraph *orderGraph = new OrderGraph(order);
uint constrSize = order->constraints.getSize();
for (uint j = 0; j < constrSize; j++) {
- addMustOrderConstraintToOrderGraph(orderGraph, order->constraints.get(j));
+ orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
}
return orderGraph;
}
-void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
Polarity polarity = constr->polarity;
BooleanValue mustval = constr->boolVal;
- Order *order = graph->order;
switch (polarity) {
case P_BOTHTRUEFALSE:
case P_TRUE: {
- OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
_1to2->mustPos = true;
_1to2->polPos = true;
}
case P_FALSE: {
if (order->type == TOTAL) {
- OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+ OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
_2to1->mustPos = true;
_2to1->polPos = true;
node2->addNewOutgoingEdge(_2to1);
node1->addNewIncomingEdge(_2to1);
} else {
- OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
_1to2->mustNeg = true;
_1to2->polNeg = true;
}
}
-void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
BooleanValue mustval = constr->boolVal;
- Order *order = graph->order;
switch (mustval) {
case BV_UNSAT:
case BV_MUSTBETRUE: {
- OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
_1to2->mustPos = true;
_1to2->polPos = true;
node1->addNewOutgoingEdge(_1to2);
}
case BV_MUSTBEFALSE: {
if (order->type == TOTAL) {
- OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+ OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
_2to1->mustPos = true;
_2to1->polPos = true;
node2->addNewOutgoingEdge(_2to1);
node1->addNewIncomingEdge(_2to1);
} else {
- OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
_1to2->mustNeg = true;
_1to2->polNeg = true;
node1->addNewOutgoingEdge(_1to2);
}
}
-OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
+OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
OrderNode *node = new OrderNode(id);
- OrderNode *tmp = graph->nodes->get(node);
+ OrderNode *tmp = nodes->get(node);
if ( tmp != NULL) {
delete node;
node = tmp;
} else {
- graph->nodes->add(node);
+ nodes->add(node);
}
return node;
}
-OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
+OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
OrderNode node(id);
- OrderNode *tmp = graph->nodes->get(&node);
+ OrderNode *tmp = nodes->get(&node);
return tmp;
}
-OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
+OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
OrderEdge *edge = new OrderEdge(begin, end);
- OrderEdge *tmp = graph->edges->get(edge);
+ OrderEdge *tmp = edges->get(edge);
if ( tmp != NULL ) {
delete edge;
edge = tmp;
} else {
- graph->edges->add(edge);
+ edges->add(edge);
}
return edge;
}
-OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
+OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
OrderEdge edge(begin, end);
- OrderEdge *tmp = graph->edges->get(&edge);
+ OrderEdge *tmp = edges->get(&edge);
return tmp;
}
-OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge) {
+OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
OrderEdge inverseedge(edge->sink, edge->source);
- OrderEdge *tmp = graph->edges->get(&inverseedge);
+ OrderEdge *tmp = edges->get(&inverseedge);
return tmp;
}
-void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
- OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
- OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
- addOrderEdge(graph, from, to, bOrder);
+void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
+ OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
+ OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
+ addOrderEdge(from, to, bOrder);
}
-void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
- OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
- OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
- addMustOrderEdge(graph, from, to, bOrder);
+void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
+ OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
+ OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
+ addMustOrderEdge(from, to, bOrder);
}
-void deleteOrderGraph(OrderGraph *graph) {
- HSIteratorOrderNode *iterator = graph->nodes->iterator();
+OrderGraph::~OrderGraph() {
+ HSIteratorOrderNode *iterator = nodes->iterator();
while (iterator->hasNext()) {
OrderNode *node = iterator->next();
delete node;
}
delete iterator;
- HSIteratorOrderEdge *eiterator = graph->edges->iterator();
+ HSIteratorOrderEdge *eiterator = edges->iterator();
while (eiterator->hasNext()) {
OrderEdge *edge = eiterator->next();
delete edge;
}
delete eiterator;
- delete graph->nodes;
- delete graph->edges;
- ourfree(graph);
+ delete nodes;
+ delete edges;
}
#include "structs.h"
#include "mymemory.h"
-struct OrderGraph {
+class OrderGraph {
+ public:
+ OrderGraph(Order *order);
+ ~OrderGraph();
+ void addOrderConstraintToOrderGraph(BooleanOrder *bOrder);
+ void addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder);
+ OrderNode *getOrderNodeFromOrderGraph(uint64_t id);
+ OrderEdge *getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
+ OrderNode *lookupOrderNodeFromOrderGraph(uint64_t id);
+ OrderEdge *lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end);
+ void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+ void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+ OrderEdge *getInverseOrderEdge(OrderEdge *edge);
HashSetOrderNode *nodes;
HashSetOrderEdge *edges;
Order *order;
};
-OrderGraph *allocOrderGraph(Order *order);
OrderGraph *buildOrderGraph(Order *order);
OrderGraph *buildMustOrderGraph(Order *order);
-void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
-void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
-OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
-OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
-OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
-OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
-void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
-void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
-void deleteOrderGraph(OrderGraph *graph);
-OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge);
#endif/* ORDERGRAPH_H */
//This is needed for splitorder
computeStronglyConnectedComponentGraph(graph);
decomposeOrder(This, order, graph);
- deleteOrderGraph(graph);
+ delete graph;
bool doIntegerEncoding = GETVARTUNABLE(This->tuner, order->order.type, ORDERINTEGERENCODING, &offon );
if(!doIntegerEncoding)
uint size = order->constraints.getSize();
for (uint i = 0; i < size; i++) {
BooleanOrder *orderconstraint = order->constraints.get(i);
- OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
- OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
+ OrderNode *from = graph->getOrderNodeFromOrderGraph(orderconstraint->first);
+ OrderNode *to = graph->getOrderNodeFromOrderGraph(orderconstraint->second);
model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
if (from->sccNum != to->sccNum) {
- OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
+ OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
if (edge->polPos) {
replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
} else if (edge->polNeg) {
((MutableSet *)neworder->set)->addElementMSet(to->id);
}
if (order->type == PARTIAL) {
- OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
+ OrderEdge *edge = graph->getOrderEdgeFromOrderGraph(from, to);
if (edge->polNeg)
partialcandidatevec.setExpand(from->sccNum, NULL);
}