X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FEncoders%2Forderencoder.c;h=3c840e72db264e87772a6187869c003644ac595a;hp=084995b1126b4823c93eae99da7e0fc8432cbfa8;hb=31a3e00533833ee1c9131a2d0748ca90e3c0d880;hpb=a1b9094e1083a67672b11a51928015f4616d24d0 diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c index 084995b..3c840e7 100644 --- a/src/Encoders/orderencoder.c +++ b/src/Encoders/orderencoder.c @@ -357,6 +357,7 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i); OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first); OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second); + model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum); if (from->sccNum != to->sccNum) { OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to); if (edge->polPos) { @@ -390,6 +391,11 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) { addOrderConstraint(neworder, orderconstraint); } } + for(uint i=0; i