}
void DecomposeOrderTransform::doTransform() {
+ if(solver->isUnSAT())
+ return;
HashsetOrder *orders = solver->getActiveOrders()->copy();
SetIteratorOrder *orderit = orders->iterator();
while (orderit->hasNext()) {
BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
updateEdgePolarity(benew, be);
- solver->replaceBooleanWithBoolean(be, benew);
+ 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());
updateEdgePolarity(benew, be);
- solver->replaceBooleanWithBoolean(be, benew);
+ 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;