Build graph

diff --git a/src/Encoders/orderedge.c b/src/Encoders/orderedge.c
index d8466afabc7b000367cd312b31f2ae48210f26c9..02f09e9d56492828dcb51b90bcc3f04c9dd1c5ee 100644 (file)
--- a/src/Encoders/orderedge.c
+++ b/src/Encoders/orderedge.c
@@ -4,6 +4,10 @@ OrderEdge* allocOrderEdge(OrderNode* source, OrderNode* sink) {
        OrderEdge* This = (OrderEdge*) ourmalloc(sizeof(OrderEdge));
        This->source = source;
        This->sink = sink;
+       This->polPos = false;
+       This->polNeg = false;
+       This->mustPos = false;
+       This->mustNeg = false;
        return This;
 }
 

diff --git a/src/Encoders/orderedge.h b/src/Encoders/orderedge.h
index 52501af51a07ddbda54cb2ffb73dd5718c2be62e..8785a0c7869fe509ca966a038c0b46653548dad5 100644 (file)
--- a/src/Encoders/orderedge.h
+++ b/src/Encoders/orderedge.h
@@ -9,11 +9,14 @@
 #define ORDEREDGE_H
 #include "classlist.h"
 #include "mymemory.h"
-#include "ordernode.h"
 
 struct OrderEdge {
        OrderNode* source;
        OrderNode* sink;
+       unsigned int polPos:1;
+       unsigned int polNeg:1;
+       unsigned int mustPos:1;
+       unsigned int mustNeg:1;
 };
 
 OrderEdge* allocOrderEdge(OrderNode* begin, OrderNode* end);

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index 8ac2649f801dcfb39f6d955d6d65d2eee1be7a0f..1fc80d192e8fe53a9f9bcf7ab86a8f492eef6588 100644 (file)
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -44,7 +44,7 @@ OrderEncoder* buildOrderGraphs(CSolver* This) {
 }
 
 OrderGraph* buildOrderGraph(Order *order) {
-       OrderGraph* orderGraph = allocOrderGraph();
+       OrderGraph* orderGraph = allocOrderGraph(order);
        uint constrSize = getSizeVectorBoolean(&order->constraints);
        for(uint j=0; j<constrSize; j++){
                addOrderConstraintToOrderGraph(orderGraph, getVectorBoolean(&order->constraints, j));

diff --git a/src/Encoders/ordergraph.c b/src/Encoders/ordergraph.c
index f2f8bd01afb7a30c9928714f21e8cef0d489cb36..5aa1c0d6a4c9f83cce0d7aa6659f5658ca7e4eed 100644 (file)
--- a/src/Encoders/ordergraph.c
+++ b/src/Encoders/ordergraph.c
@@ -2,33 +2,54 @@
 #include "ordernode.h"
 #include "boolean.h"
 #include "orderedge.h"
+#include "ordergraph.h"
+#include "order.h"
 
-OrderGraph* allocOrderGraph() {
+OrderGraph* allocOrderGraph(Order *order) {
        OrderGraph* This = (OrderGraph*) ourmalloc(sizeof(OrderGraph));
        This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+       This->order = order;
        initDefVectorOrderNode(&This->scc);
        return This;
 }
 
 void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean* constr) {
-       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) {
                        OrderEdge* _2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+                       _2to1->polPos=true;
+                       if (mustval==BV_MUSTBEFALSE || mustval == BV_UNSAT)
+                               _2to1->mustPos=true;
                        addNewOutgoingEdge(node2, _2to1);
                        addNewIncomingEdge(node1, _2to1);
-                       break;
+               } else {
+                       OrderEdge* _1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+                       _1to2->polNeg=true;
+                       if (mustval==BV_MUSTBEFALSE || mustval == BV_UNSAT)
+                               _1to2->mustNeg=true;
+                       addNewOutgoingEdge(node1, _1to2);
+                       addNewIncomingEdge(node2, _1to2);
                }
-               default:
-                       ASSERT(0);
-                               
+               break;
+       }
+       case P_UNDEFINED:
+               //There is an unreachable order constraint if this assert fires
+               ASSERT(0);
        }
 }
 

diff --git a/src/Encoders/ordergraph.h b/src/Encoders/ordergraph.h
index 3f944425116dc37d3994b70474325db68b791ab0..34aadfa8859cd5ad4adea757b39fccd2686e1521 100644 (file)
--- a/src/Encoders/ordergraph.h
+++ b/src/Encoders/ordergraph.h
@@ -14,10 +14,11 @@
 struct OrderGraph {
        HashSetOrderNode* nodes;
        HashSetOrderEdge* edges;
+       Order* order;
        VectorOrderNode scc;
 };
 
-OrderGraph* allocOrderGraph();
+OrderGraph* allocOrderGraph(Order *order);
 void addOrderConstraintToOrderGraph(OrderGraph* graph, Boolean* constr);
 OrderNode* getOrderNodeFromOrderGraph(OrderGraph* graph, uint64_t id);
 OrderEdge* getOrderEdgeFromOrderGraph(OrderGraph* graph, OrderNode* begin, OrderNode* end);