+
+void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
+ SetIteratorOrderNode *iterator = graph->getNodes();
+ while (iterator->hasNext()) {
+ OrderNode *node = (OrderNode *)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();
+ //Only eliminate must edges
+ if (!outedge->mustPos)
+ continue;
+ 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());
+
+ BooleanEdge be = solver->orderConstraint(graph->getOrder(), node->getID(), dstnode->getID());
+ solver->replaceBooleanWithTrue(be);
+
+ /* 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());
+ updateEdgePolarity(benew, be);
+ if (solver->isTrue(benew))
+ solver->replaceBooleanWithTrue(be);
+ else if (solver->isFalse(benew))
+ solver->replaceBooleanWithFalse(be);
+ else
+ 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);
+
+ BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
+ BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
+ updateEdgePolarity(benew, be);
+ if (solver->isTrue(benew))
+ solver->replaceBooleanWithTrue(be);
+ else if (solver->isFalse(benew))
+ solver->replaceBooleanWithFalse(be);
+ else
+ solver->replaceBooleanWithBoolean(be, benew);
+ }
+ dstnode->outEdges.reset();
+ delete outedgeit;
+
+
+ /* Mark destination as removed */
+ dstnode->removed = true;
+}