+void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+ BooleanValue mustval = constr->base.boolVal;
+ Order *order = graph->order;
+ switch (mustval) {
+ case BV_UNSAT:
+ case BV_MUSTBETRUE: {
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ _1to2->mustPos = true;
+ _1to2->polPos = true;
+ addNewOutgoingEdge(node1, _1to2);
+ addNewIncomingEdge(node2, _1to2);
+ if (constr->base.polarity == BV_MUSTBETRUE)
+ break;
+ }
+ case BV_MUSTBEFALSE: {
+ if (order->type == TOTAL) {
+ OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+ _2to1->mustPos = true;
+ _2to1->polPos = true;
+ addNewOutgoingEdge(node2, _2to1);
+ addNewIncomingEdge(node1, _2to1);
+ } else {
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ _1to2->mustNeg = true;
+ _1to2->polNeg = true;
+ addNewOutgoingEdge(node1, _1to2);
+ addNewIncomingEdge(node2, _1to2);
+ }
+ break;
+ }
+ case BV_UNDEFINED:
+ //Do Nothing
+ break;
+ }
+}
+