#include "decomposeorderresolver.h"
#include "tunable.h"
#include "orderanalysis.h"
+#include "polarityassignment.h"
DecomposeOrderTransform::DecomposeOrderTransform(CSolver *_solver)
}
BooleanEdge neworderconstraint = solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second);
solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint);
-
+ updateEdgePolarity(neworderconstraint, orderconstraint);
dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum);
}
}
}
//Add new order constraint
BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID());
+ updateEdgePolarity(orderconstraint, P_TRUE);
solver->addConstraint(orderconstraint);
//Add new edge
void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) {
SetIteratorOrderNode *iterator = graph->getNodes();
while (iterator->hasNext()) {
- OrderNode *node = iterator->next();
+ OrderNode *node = (OrderNode *)iterator->next();
if (node->removed)
continue;
if (isMustBeTrueNode(node)) {
void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) {
SetIteratorOrderNode *iterator = graph->getNodes();
while (iterator->hasNext()) {
- OrderNode *node = iterator->next();
+ OrderNode *node = (OrderNode *)iterator->next();
if (node->removed)
continue;
attemptNodeMerge(graph, node, dor);
BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
- solver->replaceBooleanWithBoolean(be, benew);
+ 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;
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
BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
- solver->replaceBooleanWithBoolean(be, benew);
+ 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;