- switch(constr->polarity){
- case P_BOTHTRUEFALSE:
- case P_TRUE:{
- OrderEdge* _1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
- addNewOutgoingEdge(node1, _1to2);
- addNewIncomingEdge(node2, _1to2);
- if(constr->polarity == P_TRUE)
- break;
- }
- case P_FALSE:{
+ Polarity polarity=constr->polarity;
+ BooleanValue mustval=constr->boolVal;
+ Order* order=graph->order;
+ switch(polarity) {
+ case P_BOTHTRUEFALSE:
+ case P_TRUE:{
+ OrderEdge* _1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ _1to2->polPos=true;
+ if (mustval==BV_MUSTBETRUE || mustval == BV_UNSAT)
+ _1to2->mustPos=true;
+ addNewOutgoingEdge(node1, _1to2);
+ addNewIncomingEdge(node2, _1to2);
+ if(constr->polarity == P_TRUE)
+ break;
+ }
+ case P_FALSE:{
+ if (order->type==TOTAL) {