SetIteratorOrderNode *srciterator = sources->iterator();
while (srciterator->hasNext()) {
OrderNode *srcnode = srciterator->next();
+ if (srcnode->removed)
+ continue;
OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
newedge->mustPos = true;
newedge->polPos = true;
OrderGraph *buildOrderGraph(Order *order) {
ASSERT(order->graph == NULL);
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));
node = tmp;
} else {
nodes.add(node);
- allNodes.push(node);
}
return node;
}
}
OrderGraph::~OrderGraph() {
- uint size=allNodes.getSize();
- for(uint i=0;i<size;i++)
- delete allNodes.get(i);
-
- SetIteratorOrderEdge *eiterator = edges.iterator();
- while (eiterator->hasNext()) {
- OrderEdge *edge = eiterator->next();
- delete edge;
- }
- delete eiterator;
+ nodes.resetAndDelete();
+ edges.resetAndDelete();
}
bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
SetIteratorOrderNode *iterator = getNodes();
while (iterator->hasNext()) {
OrderNode *node = iterator->next();
- if (node->status == NOTVISITED) {
+ if (node->status == NOTVISITED && !node->removed) {
node->status = VISITED;
DFSNodeVisit(node, finishNodes, false, false, 0);
node->status = FINISHED;
SetIteratorOrderNode *iterator = getNodes();
while (iterator->hasNext()) {
OrderNode *node = iterator->next();
- if (node->status == NOTVISITED) {
+ if (node->status == NOTVISITED && !node->removed) {
node->status = VISITED;
DFSNodeVisit(node, finishNodes, false, true, 0);
node->status = FINISHED;
void computeStronglyConnectedComponentGraph();
void resetNodeInfoStatusSCC();
void completePartialOrderGraph();
- void removeNode(OrderNode *node) {nodes.remove(node);}
CMEMALLOC;
private:
HashsetOrderNode nodes;
- Vector<OrderNode *> allNodes;
HashsetOrderEdge edges;
Order *order;
void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *finishNodes, bool isReverse, bool mustvisit, uint sccNum);
}
-void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) {
+void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) {
Vector<Order *> partialcandidatevec;
uint size = currOrder->constraints.getSize();
for (uint i = 0; i < size; i++) {
OrderNode *srcNode = inEdge->source;
srcNode->outEdges.remove(inEdge);
edgesRemoved->add(inEdge);
+ bool removeOutgoingEdges = !iterin->hasNext();
+
SetIteratorOrderEdge *iterout = node->outEdges.iterator();
while (iterout->hasNext()) {
OrderEdge *outEdge = iterout->next();
OrderNode *sinkNode = outEdge->sink;
- sinkNode->inEdges.remove(outEdge);
- edgesRemoved->add(outEdge);
+ if (removeOutgoingEdges) {
+ sinkNode->inEdges.remove(outEdge);
+ edgesRemoved->add(outEdge);
+ }
//Adding new edge to new sink and src nodes ...
if (srcNode == sinkNode) {
solver->setUnSAT();
delete iterout;
delete iterin;
- graph->removeNode(node);
return;
}
//Add new order constraint
delete iterout;
}
delete iterin;
- graph->removeNode(node);
}
void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {
solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b1, solver->applyLogicalOperation(SATC_NOT, b2)));
solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b2, solver->applyLogicalOperation(SATC_NOT, b1)));
- solver->serialize();
if (solver->solve() == 1) {
printf("SAT\n");
printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
bool isEdge = suborder->encoding.resolver->resolveOrder(doredge->newfirst, doredge->newsecond);
if (isEdge)
graph->addEdge(doredge->origfirst, doredge->origsecond);
+ else if (order->type == SATC_TOTAL)
+ graph->addEdge(doredge->origsecond, doredge->origfirst);
}
}
delete iterator;
buildGraph();
OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
- ASSERT(from != NULL);
+ if (from == NULL) {
+ ASSERT(order->type != SATC_TOTAL);
+ return false;
+ }
OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
- ASSERT(to != NULL);
+ if (to == NULL) {
+ ASSERT(order->type != SATC_TOTAL);
+ return false;
+ }
switch (order->type) {
case SATC_TOTAL:
return from->sccNum < to->sccNum;