From 3caf4d5dafa9a0bb4c2382f1bcb23831943457e3 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
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; 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 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