#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
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;
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;