base version

[satune.git] / src / Encoders / ordergraph.c

diff --git a/src/Encoders/ordergraph.c b/src/Encoders/ordergraph.c
index 5aa1c0d6a4c9f83cce0d7aa6659f5658ca7e4eed..2510fab7a15c29744ff2d0f6ada155159387b77e 100644 (file)
--- a/src/Encoders/ordergraph.c
+++ b/src/Encoders/ordergraph.c
@@ -21,9 +21,9 @@ void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean
        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;
+                       _1to2->mustPos = true;
+               _1to2->polPos = true;
                addNewOutgoingEdge(node1, _1to2);
                addNewIncomingEdge(node2, _1to2);
                if(constr->polarity == P_TRUE)
@@ -32,16 +32,16 @@ void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean
        case P_FALSE:{
                if (order->type==TOTAL) {
                        OrderEdge* _2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
-                       _2to1->polPos=true;
                        if (mustval==BV_MUSTBEFALSE || mustval == BV_UNSAT)
-                               _2to1->mustPos=true;
+                               _2to1->mustPos = true;
+                       _2to1->polPos = true;
                        addNewOutgoingEdge(node2, _2to1);
                        addNewIncomingEdge(node1, _2to1);
                } else {
                        OrderEdge* _1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
-                       _1to2->polNeg=true;
                        if (mustval==BV_MUSTBEFALSE || mustval == BV_UNSAT)
-                               _1to2->mustNeg=true;
+                               _1to2->mustNeg = true;
+                       _1to2->polNeg = true;
                        addNewOutgoingEdge(node1, _1to2);
                        addNewIncomingEdge(node2, _1to2);
                }
@@ -77,6 +77,12 @@ OrderEdge* getOrderEdgeFromOrderGraph(OrderGraph* graph, OrderNode* begin, Order
        return edge;
 }
 
+OrderEdge* getInverseOrderEdge(OrderGraph* graph, OrderEdge *edge) {
+       OrderEdge inverseedge={edge->sink, edge->source, false, false, false, false, false};
+       OrderEdge * tmp=getHashSetOrderEdge(graph->edges, &inverseedge);
+       return tmp;
+}
+
 void addOrderConstraintToOrderGraph(OrderGraph* graph, Boolean* constr) {
        BooleanOrder* bOrder = (BooleanOrder*) constr;
        OrderNode* from = getOrderNodeFromOrderGraph(graph, bOrder->first);