From 3caf4d5dafa9a0bb4c2382f1bcb23831943457e3 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 14 Aug 2017 22:36:52 -0700 Subject: [PATCH] base version --- src/Encoders/orderedge.c | 3 ++ src/Encoders/orderedge.h | 6 ++++ src/Encoders/orderencoder.c | 67 ++++++++++++++++++++++++++++++++----- src/Encoders/orderencoder.h | 1 + src/Encoders/ordergraph.c | 18 ++++++---- src/Encoders/ordergraph.h | 2 +- 6 files changed, 82 insertions(+), 15 deletions(-) diff --git a/src/Encoders/orderedge.c b/src/Encoders/orderedge.c index 02f09e9..bc22a83 100644 --- 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 8785a0c..a34e3d2 100644 --- 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 c53d205..fe72a61 100644 --- 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; iallOrders, 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 eb90897..2f91a53 100644 --- 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 5aa1c0d..2510fab 100644 --- 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 34aadfa..1848d2e 100644 --- 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 */ -- 2.34.1