From a19e8f63c0f85f81be4d5413d03374830a1ee571 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Thu, 17 Aug 2017 15:26:53 -0700 Subject: [PATCH] Fix bug and add support for computing transitive closure of must edge graph --- src/Collections/hashset.h | 8 +++ src/Collections/structs.c | 1 + src/Collections/structs.h | 2 + src/Collections/vector.h | 10 ++-- src/Encoders/orderencoder.c | 97 +++++++++++++++++++++++++------------ src/Encoders/orderencoder.h | 6 +-- 6 files changed, 86 insertions(+), 38 deletions(-) diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h index c9656a6..9282de9 100644 --- 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 b41a0b5..7be60b0 100644 --- 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 36ba052..183a123 100644 --- 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 97a3fff..ac32d85 100644 --- 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 0988abc..e330a7a 100644 --- 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 ae63cd6..19252c3 100644 --- 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); -- 2.34.1