base version

diff --git a/src/Encoders/orderedge.c b/src/Encoders/orderedge.c
index 02f09e9d56492828dcb51b90bcc3f04c9dd1c5ee..bc22a83bb14557f8603a75d24bdfdd146ad734f2 100644 (file)
--- a/src/Encoders/orderedge.c
+++ b/src/Encoders/orderedge.c
@@ -1,4 +1,5 @@
 #include "orderedge.h"
+#include "ordergraph.h"
 
 OrderEdge* allocOrderEdge(OrderNode* source, OrderNode* sink) {
        OrderEdge* This = (OrderEdge*) ourmalloc(sizeof(OrderEdge));
@@ -8,9 +9,11 @@ OrderEdge* allocOrderEdge(OrderNode* source, OrderNode* sink) {
        This->polNeg = false;
        This->mustPos = false;
        This->mustNeg = false;
+       This->pseudoPos = false;
        return This;
 }
 
 void deleteOrderEdge(OrderEdge* This) {
        ourfree(This);
 }
+

diff --git a/src/Encoders/orderedge.h b/src/Encoders/orderedge.h
index 8785a0c7869fe509ca966a038c0b46653548dad5..a34e3d26604dcf2c2e8292c4c0fb90935566d756 100644 (file)
--- a/src/Encoders/orderedge.h
+++ b/src/Encoders/orderedge.h
@@ -17,10 +17,16 @@ struct OrderEdge {
        unsigned int polNeg:1;
        unsigned int mustPos:1;
        unsigned int mustNeg:1;
+       unsigned int pseudoPos:1;
 };
 
 OrderEdge* allocOrderEdge(OrderNode* begin, OrderNode* end);
 void deleteOrderEdge(OrderEdge* This);
+void setPseudoPos(OrderGraph *graph, OrderEdge* edge);
+void setMustPos(OrderGraph *graph, OrderEdge *edge);
+void setMustNeg(OrderGraph *graph, OrderEdge *edge);
+void setPolPos(OrderGraph *graph, OrderEdge *edge);
+void setPolNeg(OrderGraph *graph, OrderEdge *edge);
 
 #endif /* ORDEREDGE_H */
 

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index c53d2057bcfd5e9434a8bc25d53b1edbbe8efea8..fe72a61418dd7493a20c91625f33096696dd57ab 100644 (file)
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -14,7 +14,7 @@ NodeInfo* allocNodeInfo() {
        return This;
 }
 
-void deleteNodeInfo(NodeInfo* info){
+void deleteNodeInfo(NodeInfo* info) {
        ourfree(info);
 }
 
@@ -27,7 +27,7 @@ OrderGraph* buildOrderGraph(Order *order) {
        return orderGraph;
 }
 
-void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo){
+void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
        uint timer=0;
        HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
        while(hasNextOrderNode(iterator)){
@@ -44,7 +44,7 @@ void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nod
        deleteIterOrderNode(iterator);
 }
 
-void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo){
+void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo) {
        uint timer=0;
        uint size = getSizeVectorOrderNode(finishNodes);
        for(int i=size-1; i>=0; i--){
@@ -61,7 +61,7 @@ void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeIn
 }
 
 void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes,
-       HashTableNodeInfo* nodeToInfo, uint* timer, bool isReverse){
+       HashTableNodeInfo* nodeToInfo, uint* timer, bool isReverse) {
        (*timer)++;
        model_print("Timer in DFSNodeVisit:%u\n", *timer);
        HSIteratorOrderEdge* iterator = isReverse?iteratorOrderEdge(node->inEdges):iteratorOrderEdge(node->outEdges);
@@ -81,7 +81,7 @@ void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes,
        deleteIterOrderEdge(iterator);
 }
 
-void initializeNodeInfoSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo){
+void initializeNodeInfoSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo) {
        HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
        while(hasNextOrderNode(iterator)){
                putNodeInfo(nodeToInfo, nextOrderNode(iterator), allocNodeInfo());
@@ -89,7 +89,7 @@ void initializeNodeInfoSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo){
        deleteIterOrderNode(iterator);
 }
 
-void resetNodeInfoStatusSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo){
+void resetNodeInfoStatusSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo) {
        HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
        while(hasNextOrderNode(iterator)){
                NodeInfo* info= getNodeInfo(nodeToInfo, nextOrderNode(iterator));
@@ -98,7 +98,7 @@ void resetNodeInfoStatusSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo){
        deleteIterOrderNode(iterator);
 }
 
-void computeStronglyConnectedComponentGraph(OrderGraph* graph){
+void computeStronglyConnectedComponentGraph(OrderGraph* graph) {
        VectorOrderNode finishNodes;
        initDefVectorOrderNode(& finishNodes);
        HashTableNodeInfo* nodeToInfo = allocHashTableNodeInfo(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
@@ -107,17 +107,68 @@ void computeStronglyConnectedComponentGraph(OrderGraph* graph){
        resetNodeInfoStatusSCC(graph, nodeToInfo);
        DFSReverse(graph, &finishNodes, nodeToInfo);
        deleteHashTableNodeInfo(nodeToInfo);
+       deleteVectorArrayOrderNode(&finishNodes);
 }
 
-void removeMustBeTrueNodes(OrderGraph* graph){
+void removeMustBeTrueNodes(OrderGraph* graph) {
        //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
 }
 
+bool searchForNode(OrderNode *src, OrderNode *dst) {
+       bool found=false;
+       VectorOrderNode stack;
+       initDefVectorOrderNode(&stack);
+       pushVectorOrderNode(&stack, src);
+       HashSetOrderNode* discovered = allocHashSetOrderNode(16, 0.3);
+       while(getSizeVectorOrderNode(&stack) != 0) {
+               OrderNode* node = lastVectorOrderNode(&stack); popVectorOrderNode(&stack);
+               HSIteratorOrderEdge *edgeit = iteratorOrderEdge(node->outEdges);
+               while(hasNextOrderEdge(edgeit)) {
+                       OrderEdge* edge = nextOrderEdge(edgeit);
+                       if (edge->polPos) {
+                               OrderNode *edge_dst = edge->sink;
+                               if (edge_dst == dst)
+                                       goto exitloop;
+                               if (addHashSetOrderNode(discovered, edge_dst)) {
+                                       pushVectorOrderNode(&stack, edge_dst);
+                               }
+                       }
+               }
+               deleteIterOrderEdge(edgeit);
+       }
+ exitloop:
+       deleteHashSetOrderNode(discovered);
+       deleteVectorArrayOrderNode(&stack);
+       return found;
+}
+
+void completePartialOrderGraph(OrderGraph* graph) {
+       HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
+       while(hasNextOrderNode(iterator)) {
+               OrderNode* node = nextOrderNode(iterator);
+               HSIteratorOrderEdge *edgeit = iteratorOrderEdge(node->outEdges);
+               while(hasNextOrderEdge(edgeit)) {
+                       OrderEdge* edge = nextOrderEdge(edgeit);
+                       if(edge->polNeg) {
+                               if (edge->polPos || searchForNode(node, edge->sink)) {
+                                       OrderEdge * newedge = getOrderEdgeFromOrderGraph(graph, edge->sink, edge->source);
+                                       newedge->pseudoPos = true;
+                               }
+                       }
+               }
+               deleteIterOrderEdge(edgeit);
+       }
+       deleteIterOrderNode(iterator);
+}
+
 void orderAnalysis(CSolver* This){
        uint size = getSizeVectorOrder(This->allOrders);
        for(uint i=0; i<size; i++){
                Order* order = getVectorOrder(This->allOrders, i);
                OrderGraph* graph = buildOrderGraph(order);
+               if (order->type==PARTIAL) {
+                       completePartialOrderGraph(graph);
+               }
                removeMustBeTrueNodes(graph);
                computeStronglyConnectedComponentGraph(graph);
                deleteOrderGraph(graph);

diff --git a/src/Encoders/orderencoder.h b/src/Encoders/orderencoder.h
index eb908976424266a270550e60d0fa755cdbdf9c0e..2f91a530eb600dd1193d185b40fcd68529a62cf7 100644 (file)
--- a/src/Encoders/orderencoder.h
+++ b/src/Encoders/orderencoder.h
@@ -29,6 +29,7 @@ void initializeNodeInfoSCC(OrderGraph* graph, HashTableNodeInfo* nodeToInfo);
 void DFSNodeVisit(OrderNode* node, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo, uint* timer, bool isReverse);
 void DFS(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo);
 void DFSReverse(OrderGraph* graph, VectorOrderNode* finishNodes, HashTableNodeInfo* nodeToInfo);
+void completePartialOrderGraph(OrderGraph* graph);
 
 #endif /* ORDERGRAPHBUILDER_H */
 

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);

diff --git a/src/Encoders/ordergraph.h b/src/Encoders/ordergraph.h
index 34aadfa8859cd5ad4adea757b39fccd2686e1521..1848d2e7c197c6fc941b31c56d745b75ec6cbdf8 100644 (file)
--- a/src/Encoders/ordergraph.h
+++ b/src/Encoders/ordergraph.h
@@ -24,6 +24,6 @@ OrderNode* getOrderNodeFromOrderGraph(OrderGraph* graph, uint64_t id);
 OrderEdge* getOrderEdgeFromOrderGraph(OrderGraph* graph, OrderNode* begin, OrderNode* end);
 void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean* constr);
 void deleteOrderGraph(OrderGraph* graph);
-
+OrderEdge* getInverseOrderEdge(OrderGraph* graph, OrderEdge *edge);
 #endif /* ORDERGRAPH_H */