From: Hamed Date: Wed, 9 Aug 2017 04:37:52 +0000 (-0700) Subject: Building the OrderGraph ... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=e610ad2233ef2764db7014513b8db069f07223b6 Building the OrderGraph ... --- diff --git a/src/Encoders/orderedge.c b/src/Encoders/orderedge.c index a1b8d57..6774cce 100644 --- a/src/Encoders/orderedge.c +++ b/src/Encoders/orderedge.c @@ -1,10 +1,10 @@ #include "orderedge.h" -OrderEdge* allocOrderEdge(Boolean* order, OrderNode* begin, OrderNode* end){ +OrderEdge* allocOrderEdge(Boolean* order, OrderNode* source, OrderNode* sink){ OrderEdge* This = (OrderEdge*) ourmalloc(sizeof(OrderEdge)); - This->source = begin; - This->sink = end; + This->source = source; + This->sink = sink; This->order = order; return This; } diff --git a/src/Encoders/ordergraph.c b/src/Encoders/ordergraph.c index 7b1d613..fbb73d3 100644 --- a/src/Encoders/ordergraph.c +++ b/src/Encoders/ordergraph.c @@ -1,5 +1,7 @@ #include "ordergraph.h" #include "ordernode.h" +#include "boolean.h" +#include "orderedge.h" OrderGraph* allocOrderGraph(){ OrderGraph* This = (OrderGraph*) ourmalloc(sizeof(OrderGraph)); @@ -7,6 +9,61 @@ OrderGraph* allocOrderGraph(){ return This; } +void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean* constr){ + switch(constr->polarity){ + case P_BOTHTRUEFALSE: + case P_TRUE:{ + OrderEdge* _1to2 = getOrderEdgeFromOrderGraph(graph, constr, node1, node2); + addNewOutgoingEdge(node1, _1to2); + addNewIncomingEdge(node2, _1to2); + if(constr->polarity == P_TRUE) + break; + } + case P_FALSE:{ + OrderEdge* _2to1 = getOrderEdgeFromOrderGraph(graph, constr, node2, node1); + addNewOutgoingEdge(node2, _2to1); + addNewIncomingEdge(node1, _2to1); + break; + } + default: + ASSERT(0); + + } +} + +OrderNode* getOrderNodeFromOrderGraph(OrderGraph* graph, uint64_t id, Order* order){ + OrderNode* node = allocOrderNode(id, order); + OrderNode* tmp = getHashSetOrderNode(graph->nodes, node); + if( tmp!= NULL){ + deleteOrderNode(node); + node= tmp; + } else { + addHashSetOrderNode(graph->nodes, node); + } + return node; +} + +OrderEdge* getOrderEdgeFromOrderGraph(OrderGraph* graph, Boolean* order, OrderNode* begin, OrderNode* end){ + OrderEdge* edge = allocOrderEdge(order, begin, end); + OrderEdge* tmp = getHashSetOrderEdge(graph->edges, edge); + if(tmp!= NULL){ + deleteOrderEdge(edge); + edge = tmp; + } else { + addHashSetOrderEdge(graph->edges, edge); + } + return edge; +} + +void addOrderConstraintToOrderGraph(OrderGraph* graph, Boolean* constr){ + BooleanOrder* bOrder = (BooleanOrder*) constr; + OrderNode* from = getOrderNodeFromOrderGraph(graph, bOrder->first, bOrder->order); + OrderNode* to = getOrderNodeFromOrderGraph(graph, bOrder->second, bOrder->order); + addOrderEdge(graph, from, to, constr); + +} + + void deleteOrderGraph(OrderGraph* graph){ HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes); while(hasNextOrderNode(iterator)){ @@ -14,5 +71,12 @@ void deleteOrderGraph(OrderGraph* graph){ deleteOrderNode(node); } deleteIterOrderNode(iterator); + + HSIteratorOrderEdge* eiterator = iteratorOrderEdge(graph->edges); + while(hasNextOrderEdge(eiterator)){ + OrderEdge* edge = nextOrderEdge(eiterator); + deleteOrderEdge(edge); + } + deleteIterOrderEdge(eiterator); ourfree(graph); } \ No newline at end of file diff --git a/src/Encoders/ordergraph.h b/src/Encoders/ordergraph.h index ceffe74..67b3fc2 100644 --- a/src/Encoders/ordergraph.h +++ b/src/Encoders/ordergraph.h @@ -13,10 +13,14 @@ struct OrderGraph{ HashSetOrderNode* nodes; + HashSetOrderEdge* edges; }; OrderGraph* allocOrderGraph(); - +void addOrderConstraintToOrderGraph(OrderGraph* graph, Boolean* constr); +OrderNode* getOrderNodeFromOrderGraph(OrderGraph* graph, uint64_t id, Order* order); +OrderEdge* getOrderEdgeFromOrderGraph(OrderGraph* graph, Boolean* order, OrderNode* begin, OrderNode* end); +void addOrderEdge(OrderGraph* graph, OrderNode* node1, OrderNode* node2, Boolean* constr); void deleteOrderGraph(OrderGraph* graph); #endif /* ORDERGRAPH_H */ diff --git a/src/Encoders/ordergraphbuilder.c b/src/Encoders/ordergraphbuilder.c new file mode 100644 index 0000000..285840a --- /dev/null +++ b/src/Encoders/ordergraphbuilder.c @@ -0,0 +1,21 @@ + +#include "ordergraphbuilder.h" +#include "structs.h" +#include "csolver.h" +#include "boolean.h" +#include "ordergraph.h" + + +void buildOrderGraph(CSolver* This){ + uint size = getSizeVectorBoolean(This->constraints); + OrderGraph* orderGraph = allocOrderGraph(); + for(uint i=0; iconstraints, i); + if(GETBOOLEANTYPE(constraint) == ORDERCONST){ + addOrderConstraintToOrderGraph(orderGraph, constraint); + } + } + //TODO: We should add the orderGraph to our encoder + deleteOrderGraph(orderGraph); +} + diff --git a/src/Encoders/ordergraphbuilder.h b/src/Encoders/ordergraphbuilder.h new file mode 100644 index 0000000..3a31a25 --- /dev/null +++ b/src/Encoders/ordergraphbuilder.h @@ -0,0 +1,15 @@ +/* + * File: ordergraphbuilder.h + * Author: hamed + * + * Created on August 8, 2017, 6:36 PM + */ + +#ifndef ORDERGRAPHBUILDER_H +#define ORDERGRAPHBUILDER_H +#include "classlist.h" + +void buildOrderGraph(CSolver* This); +void computeStronglyConnectedComponentGraph(OrderGraph* graph); +#endif /* ORDERGRAPHBUILDER_H */ + diff --git a/src/Encoders/ordernode.c b/src/Encoders/ordernode.c index 13c2c09..d441a07 100644 --- a/src/Encoders/ordernode.c +++ b/src/Encoders/ordernode.c @@ -10,17 +10,18 @@ OrderNode* allocOrderNode(uint64_t id, Order* order){ return This; } +void addNewIncomingEdge(OrderNode* node, OrderEdge* edge){ + ASSERT(!containsHashSetOrderEdge(node->inEdges, edge)); // Only for testing ... Should be removed after testing + addHashSetOrderEdge(node->inEdges, edge); +} + +void addNewOutgoingEdge(OrderNode* node, OrderEdge* edge){ + ASSERT(!containsHashSetOrderEdge(node->outEdges, edge)); + addHashSetOrderEdge(node->outEdges, edge); +} + void deleteOrderNode(OrderNode* node){ - //NOTE: each node only responsible to delete its outgoing edges and - // only delete the set for incoming edges (incoming edges are going - // to be deleted by other OrderNodes that they go out from them ... deleteHashSetOrderEdge(node->inEdges); - HSIteratorOrderEdge* iterator = iteratorOrderEdge(node->outEdges); - while(hasNextOrderEdge(iterator)){ - OrderEdge* edge = nextOrderEdge(iterator); - deleteOrderEdge(edge); - } - deleteIterOrderEdge(iterator); deleteHashSetOrderEdge(node->outEdges); ourfree(node); } \ No newline at end of file diff --git a/src/Encoders/ordernode.h b/src/Encoders/ordernode.h index 5480d54..9abecf3 100644 --- a/src/Encoders/ordernode.h +++ b/src/Encoders/ordernode.h @@ -12,6 +12,7 @@ #include "classlist.h" #include "mymemory.h" #include "structs.h" +#include "orderedge.h" struct OrderNode{ uint64_t id; Order* order; @@ -20,7 +21,8 @@ struct OrderNode{ }; OrderNode* allocOrderNode(uint64_t id, Order* order); - +void addNewIncomingEdge(OrderNode* node, OrderEdge* edge); +void addNewOutgoingEdge(OrderNode* node, OrderEdge* edge); void deleteOrderNode(OrderNode* node); #endif /* ORDERNODE_H */