}
bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
- HashsetOrderEdge *edgesRemoved = NULL;
if (mustReachPrune) {
- edgesRemoved = new HashsetOrderEdge();
- removeMustBeTrueNodes(graph, edgesRemoved);
+ removeMustBeTrueNodes(graph, dor);
+ }
+
+ bool pruneEdges = GETVARTUNABLE(solver->getTuner(), order->type, MUSTEDGEPRUNE, &onoff);
+
+ if (pruneEdges) {
+ mustEdgePrune(graph, dor);
}
//This is needed for splitorder
graph->computeStronglyConnectedComponentGraph();
- decomposeOrder(order, graph, edgesRemoved, dor);
- if (edgesRemoved != NULL)
- delete edgesRemoved;
+ decomposeOrder(order, graph, dor);
delete graph;
}
delete orderit;
}
-void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) {
+void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) {
Vector<Order *> partialcandidatevec;
uint size = currOrder->constraints.getSize();
for (uint i = 0; i < size; i++) {
OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
- if (edgesRemoved != NULL) {
- if (edgesRemoved->contains(edge)) {
- dor->mustOrderEdge(from->getID(), to->getID());
- solver->replaceBooleanWithTrue(orderconstraint);
- continue;
- } else if (edgesRemoved->contains(invedge)) {
- dor->mustOrderEdge(to->getID(), from->getID());
- solver->replaceBooleanWithFalse(orderconstraint);
- continue;
- }
- }
+ if (from->removed || to->removed)
+ continue;
if (from->sccNum != to->sccNum) {
if (edge != NULL) {
if (edge->polNeg)
partialcandidatevec.setExpand(from->sccNum, NULL);
}
- orderconstraint->order = neworder;
+ BooleanEdge neworderconstraint=solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
+ solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
+
dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
- neworder->addOrderConstraint(orderconstraint);
}
}
solver->getActiveOrders()->remove(currOrder);
return true;
}
-void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved) {
+void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
node->removed = true;
+ model_print("Removing %llu\n", node->getID());
SetIteratorOrderEdge *iterin = node->inEdges.iterator();
while (iterin->hasNext()) {
OrderEdge *inEdge = iterin->next();
OrderNode *srcNode = inEdge->source;
srcNode->outEdges.remove(inEdge);
- edgesRemoved->add(inEdge);
+ dor->mustOrderEdge(srcNode->getID(), node->getID());
+ BooleanEdge be=solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID());
+ solver->replaceBooleanWithTrue(be);
bool removeOutgoingEdges = !iterin->hasNext();
SetIteratorOrderEdge *iterout = node->outEdges.iterator();
OrderEdge *outEdge = iterout->next();
OrderNode *sinkNode = outEdge->sink;
if (removeOutgoingEdges) {
+ dor->mustOrderEdge(node->getID(), sinkNode->getID());
sinkNode->inEdges.remove(outEdge);
- edgesRemoved->add(outEdge);
+ BooleanEdge be2=solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID());
+ solver->replaceBooleanWithTrue(be2);
}
//Adding new edge to new sink and src nodes ...
if (srcNode == sinkNode) {
delete iterin;
}
-void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) {
+void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
SetIteratorOrderNode *iterator = graph->getNodes();
while (iterator->hasNext()) {
OrderNode *node = iterator->next();
+ if (node->removed)
+ continue;
if (isMustBeTrueNode(node)) {
- bypassMustBeTrueNode(graph, node, edgesRemoved);
+ bypassMustBeTrueNode(graph, node, dor);
}
}
delete iterator;
}
+
+void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
+ SetIteratorOrderNode *iterator = graph->getNodes();
+ while (iterator->hasNext()) {
+ OrderNode *node = iterator->next();
+ if (node->removed)
+ continue;
+ attemptNodeMerge(graph, node, dor);
+ }
+ delete iterator;
+}
+
+void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) {
+ SetIteratorOrderEdge * edgeit = node->outEdges.iterator();
+ while(edgeit->hasNext()) {
+ OrderEdge *outedge=edgeit->next();
+ OrderNode *dstnode=outedge->sink;
+ uint numOutEdges=node->outEdges.getSize();
+ uint numInEdges=dstnode->inEdges.getSize();
+ /*
+ Need to avoid a situation where we create new reachability by
+ the merge. This can only happen if there is an extra in edge to
+ the dstnode and an extra out edge to our node.
+ */
+
+ if (numOutEdges == 1 || numInEdges == 1) {
+ /* Safe to do the Merge */
+ mergeNodes(graph, node, outedge, dstnode, dor);
+
+ //Throw away the iterator and start over
+ delete edgeit;
+ edgeit=node->outEdges.iterator();
+ }
+ }
+ delete edgeit;
+}
+
+void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) {
+ /* Fix up must edge between the two nodes */
+ node->outEdges.remove(edge);
+ dstnode->inEdges.remove(edge);
+ dor->mustOrderEdge(node->getID(), dstnode->getID());
+
+ /* Go through the incoming edges to the new node */
+ SetIteratorOrderEdge *inedgeit=dstnode->inEdges.iterator();
+ while(inedgeit->hasNext()) {
+ OrderEdge *inedge=inedgeit->next();
+ OrderNode *source=inedge->source;
+ //remove it from the source node
+ source->outEdges.remove(inedge);
+ //save the remapping that we did
+ dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID());
+ //create the new edge
+ OrderEdge *newedge=graph->getOrderEdgeFromOrderGraph(source, node);
+ //update the flags
+ newedge->polPos |= inedge->polPos;
+ newedge->polNeg |= inedge->polNeg;
+ newedge->mustPos |= inedge->mustPos;
+ newedge->mustNeg |= inedge->mustNeg;
+ newedge->pseudoPos |= inedge->pseudoPos;
+ //add new edge to both
+ source->outEdges.add(newedge);
+ node->inEdges.add(newedge);
+
+ BooleanEdge be=solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
+ BooleanEdge benew=solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
+ solver->replaceBooleanWithBoolean(be, benew);
+
+ }
+ dstnode->inEdges.reset();
+ delete inedgeit;
+
+ /* Go through the outgoing edges from the new node */
+ SetIteratorOrderEdge *outedgeit=dstnode->outEdges.iterator();
+ while(outedgeit->hasNext()) {
+ OrderEdge *outedge=outedgeit->next();
+ OrderNode *sink=outedge->sink;
+ //remove it from the sink node
+ sink->inEdges.remove(outedge);
+ //save the remapping that we did
+ dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID());
+ //create the new edge
+ OrderEdge *newedge=graph->getOrderEdgeFromOrderGraph(node, sink);
+ //update the flags
+ newedge->polPos |= outedge->polPos;
+ newedge->polNeg |= outedge->polNeg;
+ newedge->mustPos |= outedge->mustPos;
+ newedge->mustNeg |= outedge->mustNeg;
+ newedge->pseudoPos |= outedge->pseudoPos;
+ //add new edge to both
+ sink->inEdges.add(newedge);
+ node->outEdges.add(newedge);
+ //add it to the remove set
+ }
+ dstnode->outEdges.reset();
+ delete outedgeit;
+
+ /* Mark destination as removed */
+ dstnode->removed = true;
+}