#include "ordernode.h"
#include "boolean.h"
#include "orderedge.h"
+#include "ordergraph.h"
+#include "order.h"
-OrderGraph* allocOrderGraph(){
- OrderGraph* This = (OrderGraph*) ourmalloc(sizeof(OrderGraph));
+OrderGraph *allocOrderGraph(Order *order) {
+ OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
- initDefVectorOrderNode(&This->scc);
+ This->order = order;
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);
+void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+ Polarity polarity = constr->base.polarity;
+ BooleanValue mustval = constr->base.boolVal;
+ Order *order = graph->order;
+ switch (polarity) {
+ case P_BOTHTRUEFALSE:
+ case P_TRUE: {
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
+ _1to2->mustPos = true;
+ _1to2->polPos = true;
+ addNewOutgoingEdge(node1, _1to2);
+ addNewIncomingEdge(node2, _1to2);
+ if (constr->base.polarity == P_TRUE)
+ break;
+ }
+ case P_FALSE: {
+ if (order->type == TOTAL) {
+ OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+ if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
+ _2to1->mustPos = true;
+ _2to1->polPos = true;
addNewOutgoingEdge(node2, _2to1);
addNewIncomingEdge(node1, _2to1);
- break;
+ } else {
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
+ _1to2->mustNeg = true;
+ _1to2->polNeg = true;
+ addNewOutgoingEdge(node1, _1to2);
+ addNewIncomingEdge(node2, _1to2);
}
- default:
- ASSERT(0);
-
+ break;
+ }
+ case P_UNDEFINED:
+ //There is an unreachable order constraint if this assert fires
+ 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){
+OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
+ OrderNode *node = allocOrderNode(id);
+ OrderNode *tmp = getHashSetOrderNode(graph->nodes, node);
+ if ( tmp != NULL) {
deleteOrderNode(node);
- node= tmp;
+ 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){
+OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
+ OrderEdge *edge = allocOrderEdge(begin, end);
+ OrderEdge *tmp = getHashSetOrderEdge(graph->edges, edge);
+ if ( tmp != NULL ) {
deleteOrderEdge(edge);
edge = tmp;
} else {
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);
+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 deleteOrderGraph(OrderGraph* graph){
- HSIteratorOrderNode* iterator = iteratorOrderNode(graph->nodes);
- while(hasNextOrderNode(iterator)){
- OrderNode* node = nextOrderNode(iterator);
+void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
+ OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
+ OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
+ addOrderEdge(graph, from, to, bOrder);
+}
+
+void deleteOrderGraph(OrderGraph *graph) {
+ HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
+ while (hasNextOrderNode(iterator)) {
+ OrderNode *node = nextOrderNode(iterator);
deleteOrderNode(node);
}
deleteIterOrderNode(iterator);
-
- HSIteratorOrderEdge* eiterator = iteratorOrderEdge(graph->edges);
- while(hasNextOrderEdge(eiterator)){
- OrderEdge* edge = nextOrderEdge(eiterator);
+
+ HSIteratorOrderEdge *eiterator = iteratorOrderEdge(graph->edges);
+ while (hasNextOrderEdge(eiterator)) {
+ OrderEdge *edge = nextOrderEdge(eiterator);
deleteOrderEdge(edge);
}
deleteIterOrderEdge(eiterator);
ourfree(graph);
-}
\ No newline at end of file
+}