Fix bug and add support for computing transitive closure of must edge graph

diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h
index c9656a69444a676e2f9f22843a3467b30766b638..9282de97c359dd5f7cc2b9b1e38e27a25497e939 100644 (file)
--- a/src/Collections/hashset.h
+++ b/src/Collections/hashset.h
@@ -45,6 +45,7 @@
        HashSet ## Name * copyHashSet ## Name(HashSet ## Name * set);                \
        void resetHashSet ## Name(HashSet ## Name * set);                         \
        bool addHashSet ## Name(HashSet ## Name * set,_Key key);                     \
+       void addAllHashSet ## Name(HashSet ## Name * set,HashSet ## Name * other);  \
        _Key getHashSet ## Name(HashSet ## Name * set,_Key key);                  \
        _Key getHashSetFirstKey ## Name(HashSet ## Name * set);                      \
        bool containsHashSet ## Name(HashSet ## Name * set,_Key key);             \
@@ -126,6 +127,13 @@
                reset ## Name ## Set(set->table);                                   \
        }                                                                     \
                                                                         \
+       void addAllHashSet ## Name(HashSet ## Name * set, HashSet ## Name * other) { \
+               HSIterator ## Name * it = iterator ## Name(other);                  \
+               while (hasNext ## Name(it))                                         \
+                       addHashSet ## Name(set, next ## Name(it));                        \
+               deleteIter ## Name(it);                                             \
+       }                                                                     \
+                                                                        \
        bool addHashSet ## Name(HashSet ## Name * set,_Key key) {                    \
                LinkNode ## Name * val = get ## Name ## Set(set->table, key);         \
                if (val == NULL) {                                                    \

diff --git a/src/Collections/structs.c b/src/Collections/structs.c
index b41a0b539510e94597fda745ee6f1b57be820cf8..7be60b0fa4dd1f69cd5eb5b46a370388ad0f65c3 100644 (file)
--- a/src/Collections/structs.c
+++ b/src/Collections/structs.c
@@ -77,3 +77,4 @@ HashSetImpl(TableEntry, TableEntry *, table_entry_hash_Function, table_entry_equ
 HashSetImpl(OrderNode, OrderNode *, order_node_hash_Function, order_node_equals);
 HashSetImpl(OrderEdge, OrderEdge *, order_edge_hash_Function, order_edge_equals);
 
+HashTableImpl(NodeToNodeSet, OrderNode *, HashSetOrderNode *, Ptr_hash_function, Ptr_equals, deleteHashSetOrderNode);

diff --git a/src/Collections/structs.h b/src/Collections/structs.h
index 36ba052319f625e5c69a5f3c19726084c936d48e..183a1230f90019e057146d58ba46d4879997a991 100644 (file)
--- a/src/Collections/structs.h
+++ b/src/Collections/structs.h
@@ -31,4 +31,6 @@ HashSetDef(Void, void *);
 HashSetDef(TableEntry, TableEntry *);
 HashSetDef(OrderNode, OrderNode *);
 HashSetDef(OrderEdge, OrderEdge *);
+
+HashTableDef(NodeToNodeSet, OrderNode *, HashSetOrderNode *);
 #endif

diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index 97a3fff18c9286642b7ae325467a7b4dbc4f9dbd..ac32d853d7945f5762e795b5df8292a215d4c569 100644 (file)
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -16,7 +16,7 @@
        type lastVector ## name(Vector ## name * vector);                      \
        void popVector ## name(Vector ## name * vector);                       \
        type getVector ## name(Vector ## name * vector, uint index);           \
-       void setExpandVector ## name(Vector ## name * vector, uint index, type item);   \
+       void setExpandVector ## name(Vector ## name * vector, uint index, type item); \
        void setVector ## name(Vector ## name * vector, uint index, type item); \
        uint getSizeVector ## name(Vector ## name * vector);                   \
        void setSizeVector ## name(Vector ## name * vector, uint size);        \
@@ -74,10 +74,10 @@
                return vector->array[index];                                        \
        }                                                                     \
        void setExpandVector ## name(Vector ## name * vector, uint index, type item) { \
-               if (index>=vector->size)                                                                                                                                                                                \
-                       setSizeVector ## name(vector, index + 1);                                                                                                       \
-               setVector ## name(vector, index, item);                                                                                                                 \
-       }                                                                                                                                                                                                                                                                                       \
+               if (index >= vector->size)                                            \
+                       setSizeVector ## name(vector, index + 1);                         \
+               setVector ## name(vector, index, item);                             \
+       }                                                                     \
        void setVector ## name(Vector ## name * vector, uint index, type item) { \
                vector->array[index] = item;                                          \
        }                                                                     \

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index 0988abcc7e4e559e3ef4c63998e0b93431ebae17..e330a7abe68ee57be6ab7db35385cbd28656ee81 100644 (file)
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -146,7 +146,7 @@ void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
                OrderNode *node = nextOrderNode(iterator);
                if (node->status == NOTVISITED) {
                        node->status = VISITED;
-                       DFSMustNodeVisit(node, finishNodes, false);
+                       DFSMustNodeVisit(node, finishNodes);
                        node->status = FINISHED;
                        pushVectorOrderNode(finishNodes, node);
                }
@@ -154,35 +154,18 @@ void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
        deleteIterOrderNode(iterator);
 }
 
-void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool clearBackEdges) {
-       //First compute implication of transitive closure on must pos edges
+void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes) {
        HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
-       while (hasNextOrderEdge(iterator)) {
-               OrderEdge *edge = nextOrderEdge(iterator);
-               OrderNode *parent = edge->source;
-               if (parent->status == VISITED) {
-                       edge->mustPos = true;
-               }
-       }
-       deleteIterOrderEdge(iterator);
-
-       //Next compute implication of transitive closure on must neg edges
-       iterator = iteratorOrderEdge(node->outEdges);
        while (hasNextOrderEdge(iterator)) {
                OrderEdge *edge = nextOrderEdge(iterator);
                OrderNode *child = edge->sink;
 
-               if (clearBackEdges && child->status == VISITED) {
-                       //We have a backedge, so note that this edge must be negative
-                       edge->mustNeg = true;
-               }
-
                if (!edge->mustPos)     //Ignore edges that are not must Positive edges
                        continue;
 
                if (child->status == NOTVISITED) {
                        child->status = VISITED;
-                       DFSMustNodeVisit(child, finishNodes, clearBackEdges);
+                       DFSMustNodeVisit(child, finishNodes);
                        child->status = FINISHED;
                        pushVectorOrderNode(finishNodes, child);
                }
@@ -190,16 +173,70 @@ void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool clearB
        deleteIterOrderEdge(iterator);
 }
 
-void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes) {
+
+void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
        uint size = getSizeVectorOrderNode(finishNodes);
+       HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
+
        for (int i = size - 1; i >= 0; i--) {
                OrderNode *node = getVectorOrderNode(finishNodes, i);
-               if (node->status == NOTVISITED) {
-                       node->status = VISITED;
-                       DFSMustNodeVisit(node, NULL, true);
-                       node->status = FINISHED;
+               HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
+               putNodeToNodeSet(table, node, sources);
+
+               {
+                       //Compute source sets
+                       HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
+                       while (hasNextOrderEdge(iterator)) {
+                               OrderEdge *edge = nextOrderEdge(iterator);
+                               OrderNode *parent = edge->source;
+                               if (edge->mustPos) {
+                                       addHashSetOrderNode(sources, parent);
+                                       HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
+                                       addAllHashSetOrderNode(sources, parent_srcs);
+                               }
+                       }
+                       deleteIterOrderEdge(iterator);
+               }
+               if (computeTransitiveClosure) {
+                       //Compute full transitive closure for nodes
+                       HSIteratorOrderNode *srciterator = iteratorOrderNode(sources);
+                       while (hasNextOrderNode(srciterator)) {
+                               OrderNode *srcnode = nextOrderNode(srciterator);
+                               OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
+                               newedge->mustPos = true;
+                               newedge->polPos = true;
+                               addHashSetOrderEdge(srcnode->outEdges,newedge);
+                               addHashSetOrderEdge(node->inEdges,newedge);
+                       }
+                       deleteIterOrderNode(srciterator);
+               }
+               {
+                       //Use source sets to compute mustPos edges
+                       HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
+                       while (hasNextOrderEdge(iterator)) {
+                               OrderEdge *edge = nextOrderEdge(iterator);
+                               OrderNode *parent = edge->source;
+                               if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) {
+                                       edge->mustPos = true;
+                               }
+                       }
+                       deleteIterOrderEdge(iterator);
+               }
+               {
+                       //Use source sets to compute mustNeg edges that would introduce cycle if true
+                       HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
+                       while (hasNextOrderEdge(iterator)) {
+                               OrderEdge *edge = nextOrderEdge(iterator);
+                               OrderNode *child = edge->sink;
+                               if (!edge->mustPos && containsHashSetOrderNode(sources, child)) {
+                                       edge->mustNeg = true;
+                               }
+                       }
+                       deleteIterOrderEdge(iterator);
                }
        }
+
+       resetAndDeleteHashTableNodeToNodeSet(table);
 }
 
 /* This function finds edges that would form a cycle with must edges
@@ -207,7 +244,7 @@ void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes) {
    must be true because of transitivity from other must be true
    edges. */
 
-void reachMustAnalysis(OrderGraph *graph) {
+void reachMustAnalysis(OrderGraph *graph, bool computeTransitiveClosure) {
        VectorOrderNode finishNodes;
        initDefVectorOrderNode(&finishNodes);
        //Topologically sort the mustPos edge graph
@@ -215,7 +252,7 @@ void reachMustAnalysis(OrderGraph *graph) {
        resetNodeInfoStatusSCC(graph);
 
        //Find any backwards edges that complete cycles and force them to be mustNeg
-       DFSClearContradictions(graph, &finishNodes);
+       DFSClearContradictions(graph, &finishNodes, computeTransitiveClosure);
        deleteVectorArrayOrderNode(&finishNodes);
        resetNodeInfoStatusSCC(graph);
 }
@@ -282,11 +319,11 @@ void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
                        replaceBooleanWithFalse((Boolean *)orderconstraint);
                } else {
                        //Build new order and change constraint's order
-                       Order * neworder = NULL;
+                       Order *neworder = NULL;
                        if (getSizeVectorOrder(&ordervec) > from->sccNum)
                                neworder = getVectorOrder(&ordervec, from->sccNum);
                        if (neworder == NULL) {
-                               Set * set = (Set *) allocMutableSet(order->set->type);
+                               Set *set = (Set *) allocMutableSet(order->set->type);
                                neworder = allocOrder(order->type, set);
                                pushVectorOrder(This->allOrders, neworder);
                                setExpandVectorOrder(&ordervec, from->sccNum, neworder);
@@ -319,7 +356,7 @@ void orderAnalysis(CSolver *This) {
                }
 
                //This analysis is completely optional
-               reachMustAnalysis(graph);
+               reachMustAnalysis(graph, false);
 
                //This pair of analysis is also optional
                if (order->type == PARTIAL) {

diff --git a/src/Encoders/orderencoder.h b/src/Encoders/orderencoder.h
index ae63cd682b7c9a4edd4d31059ff9fa272517254d..19252c32c3799d6d75bfdb1a1d7406e193be144d 100644 (file)
--- a/src/Encoders/orderencoder.h
+++ b/src/Encoders/orderencoder.h
@@ -24,9 +24,9 @@ void removeMustBeTrueNodes(OrderGraph *graph);
 void DFSPseudoNodeVisit(OrderGraph *graph, OrderNode *node);
 void completePartialOrderGraph(OrderGraph *graph);
 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes);
-void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool clearBackEdges);
-void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes);
-void reachMustAnalysis(OrderGraph *graph);
+void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes);
+void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure);
+void reachMustAnalysis(OrderGraph *graph, bool computeTransitiveClosure);
 void localMustAnalysisTotal(OrderGraph *graph);
 void localMustAnalysisPartial(OrderGraph *graph);
 void orderAnalysis(CSolver *This);