--- /dev/null
+#include "orderedge.h"
+#include "ordergraph.h"
+
+OrderEdge *allocOrderEdge(OrderNode *source, OrderNode *sink) {
+ OrderEdge *This = (OrderEdge *) ourmalloc(sizeof(OrderEdge));
+ This->source = source;
+ This->sink = sink;
+ This->polPos = false;
+ This->polNeg = false;
+ This->mustPos = false;
+ This->mustNeg = false;
+ This->pseudoPos = false;
+ return This;
+}
+
+void deleteOrderEdge(OrderEdge *This) {
+ ourfree(This);
+}
+
--- /dev/null
+/*
+ * File: orderedge.h
+ * Author: hamed
+ *
+ * Created on August 7, 2017, 3:44 PM
+ */
+
+#ifndef ORDEREDGE_H
+#define ORDEREDGE_H
+#include "classlist.h"
+#include "mymemory.h"
+
+struct OrderEdge {
+ OrderNode *source;
+ OrderNode *sink;
+ unsigned int polPos : 1;
+ 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 */
+
--- /dev/null
+#include "ordergraph.h"
+#include "ordernode.h"
+#include "boolean.h"
+#include "orderedge.h"
+#include "ordergraph.h"
+#include "order.h"
+
+OrderGraph *allocOrderGraph(Order *order) {
+ OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
+ This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+ This->edges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+ This->order = order;
+ return This;
+}
+
+OrderGraph *buildOrderGraph(Order *order) {
+ OrderGraph *orderGraph = allocOrderGraph(order);
+ uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
+ for (uint j = 0; j < constrSize; j++) {
+ addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
+ }
+ return orderGraph;
+}
+
+//Builds only the subgraph for the must order graph.
+OrderGraph *buildMustOrderGraph(Order *order) {
+ OrderGraph *orderGraph = allocOrderGraph(order);
+ uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
+ for (uint j = 0; j < constrSize; j++) {
+ addMustOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
+ }
+ return orderGraph;
+}
+
+void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+ Polarity polarity = constr->polarity;
+ BooleanValue mustval = constr->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->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);
+ } 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);
+ }
+ break;
+ }
+ case P_UNDEFINED:
+ //There is an unreachable order constraint if this assert fires
+ ASSERT(0);
+ }
+}
+
+void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+ BooleanValue mustval = constr->boolVal;
+ Order *order = graph->order;
+ switch (mustval) {
+ case BV_UNSAT:
+ case BV_MUSTBETRUE: {
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ _1to2->mustPos = true;
+ _1to2->polPos = true;
+ addNewOutgoingEdge(node1, _1to2);
+ addNewIncomingEdge(node2, _1to2);
+ if (constr->boolVal == BV_MUSTBETRUE)
+ break;
+ }
+ case BV_MUSTBEFALSE: {
+ if (order->type == TOTAL) {
+ OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
+ _2to1->mustPos = true;
+ _2to1->polPos = true;
+ addNewOutgoingEdge(node2, _2to1);
+ addNewIncomingEdge(node1, _2to1);
+ } else {
+ OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
+ _1to2->mustNeg = true;
+ _1to2->polNeg = true;
+ addNewOutgoingEdge(node1, _1to2);
+ addNewIncomingEdge(node2, _1to2);
+ }
+ break;
+ }
+ case BV_UNDEFINED:
+ //Do Nothing
+ break;
+ }
+}
+
+OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
+ OrderNode *node = allocOrderNode(id);
+ OrderNode *tmp = getHashSetOrderNode(graph->nodes, node);
+ if ( tmp != NULL) {
+ deleteOrderNode(node);
+ node = tmp;
+ } else {
+ addHashSetOrderNode(graph->nodes, node);
+ }
+ return node;
+}
+
+OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
+ OrderNode node = {id, NULL, NULL, NOTVISITED, 0};
+ OrderNode *tmp = getHashSetOrderNode(graph->nodes, &node);
+ return tmp;
+}
+
+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 {
+ addHashSetOrderEdge(graph->edges, edge);
+ }
+ return edge;
+}
+
+OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
+ OrderEdge edge = {begin, end, 0, 0, 0, 0, 0};
+ OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &edge);
+ return tmp;
+}
+
+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, BooleanOrder *bOrder) {
+ OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
+ OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
+ addOrderEdge(graph, from, to, bOrder);
+}
+
+void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
+ OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
+ OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
+ addMustOrderEdge(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);
+ deleteOrderEdge(edge);
+ }
+ deleteIterOrderEdge(eiterator);
+ deleteHashSetOrderNode(graph->nodes);
+ deleteHashSetOrderEdge(graph->edges);
+ ourfree(graph);
+}
--- /dev/null
+/*
+ * File: ordergraph.h
+ * Author: hamed
+ *
+ * Created on August 7, 2017, 3:42 PM
+ */
+
+#ifndef ORDERGRAPH_H
+#define ORDERGRAPH_H
+#include "classlist.h"
+#include "structs.h"
+#include "mymemory.h"
+
+struct OrderGraph {
+ HashSetOrderNode *nodes;
+ HashSetOrderEdge *edges;
+ Order *order;
+};
+
+OrderGraph *allocOrderGraph(Order *order);
+OrderGraph *buildOrderGraph(Order *order);
+OrderGraph *buildMustOrderGraph(Order *order);
+void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
+void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
+OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
+OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
+OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
+OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
+void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
+void deleteOrderGraph(OrderGraph *graph);
+OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge);
+#endif/* ORDERGRAPH_H */
+
--- /dev/null
+#include "ordernode.h"
+#include "orderedge.h"
+
+OrderNode *allocOrderNode(uint64_t id) {
+ OrderNode *This = (OrderNode *) ourmalloc(sizeof(OrderNode));
+ This->id = id;
+ This->inEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+ This->outEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+ This->status = NOTVISITED;
+ This->sccNum = 0;
+ 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) {
+ deleteHashSetOrderEdge(node->inEdges);
+ deleteHashSetOrderEdge(node->outEdges);
+ ourfree(node);
+}
--- /dev/null
+
+/*
+ * File: ordernode.h
+ * Author: hamed
+ *
+ * Created on August 7, 2017, 3:43 PM
+ */
+
+#ifndef ORDERNODE_H
+#define ORDERNODE_H
+
+#include "classlist.h"
+#include "mymemory.h"
+#include "structs.h"
+#include "orderedge.h"
+
+enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET};
+typedef enum NodeStatus NodeStatus;
+
+struct OrderNode {
+ uint64_t id;
+ HashSetOrderEdge *inEdges;
+ HashSetOrderEdge *outEdges;
+ NodeStatus status;
+ uint sccNum;
+};
+
+OrderNode *allocOrderNode(uint64_t id);
+void addNewIncomingEdge(OrderNode *node, OrderEdge *edge);
+void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge);
+void deleteOrderNode(OrderNode *node);
+
+#endif/* ORDERNODE_H */
+
--- /dev/null
+#include "polarityassignment.h"
+#include "csolver.h"
+
+void computePolarities(CSolver *This) {
+ HSIteratorBoolean *iterator=iteratorBoolean(This->constraints);
+ while(hasNextBoolean(iterator)) {
+ Boolean *boolean = nextBoolean(iterator);
+ updatePolarity(boolean, P_TRUE);
+ updateMustValue(boolean, BV_MUSTBETRUE);
+ computePolarityAndBooleanValue(boolean);
+ }
+ deleteIterBoolean(iterator);
+}
+
+void updatePolarity(Boolean *This, Polarity polarity) {
+ This->polarity = (Polarity) (This->polarity | polarity);
+}
+
+void updateMustValue(Boolean *This, BooleanValue value) {
+ This->boolVal = (BooleanValue) (This->boolVal | value);
+}
+
+void computePolarityAndBooleanValue(Boolean *This) {
+ switch (GETBOOLEANTYPE(This)) {
+ case BOOLEANVAR:
+ case ORDERCONST:
+ return;
+ case PREDICATEOP:
+ return computePredicatePolarityAndBooleanValue((BooleanPredicate *)This);
+ case LOGICOP:
+ return computeLogicOpPolarityAndBooleanValue((BooleanLogic *)This);
+ default:
+ ASSERT(0);
+ }
+}
+
+void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
+ if (This->undefStatus != NULL) {
+ updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
+ computePolarityAndBooleanValue(This->undefStatus);
+ }
+}
+
+void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
+ computeLogicOpBooleanValue(This);
+ computeLogicOpPolarity(This);
+ uint size = getSizeArrayBoolean(&This->inputs);
+ for (uint i = 0; i < size; i++) {
+ computePolarityAndBooleanValue(getArrayBoolean(&This->inputs, i));
+ }
+}
+
+Polarity negatePolarity(Polarity This) {
+ switch (This) {
+ case P_UNDEFINED:
+ case P_BOTHTRUEFALSE:
+ return This;
+ case P_TRUE:
+ return P_FALSE;
+ case P_FALSE:
+ return P_TRUE;
+ default:
+ ASSERT(0);
+ }
+}
+
+BooleanValue negateBooleanValue(BooleanValue This) {
+ switch (This) {
+ case BV_UNDEFINED:
+ case BV_UNSAT:
+ return This;
+ case BV_MUSTBETRUE:
+ return BV_MUSTBEFALSE;
+ case BV_MUSTBEFALSE:
+ return BV_MUSTBETRUE;
+ default:
+ ASSERT(0);
+ }
+}
+
+void computeLogicOpPolarity(BooleanLogic *This) {
+ Polarity parentpolarity = GETBOOLEANPOLARITY(This);
+ switch (This->op) {
+ case L_AND:
+ case L_OR: {
+ uint size = getSizeArrayBoolean(&This->inputs);
+ for (uint i = 0; i < size; i++) {
+ Boolean *tmp = getArrayBoolean(&This->inputs, i);
+ updatePolarity(tmp, parentpolarity);
+ }
+ break;
+ }
+ case L_NOT: {
+ Boolean *tmp = getArrayBoolean(&This->inputs, 0);
+ updatePolarity(tmp, negatePolarity(parentpolarity));
+ break;
+ }
+ case L_XOR: {
+ updatePolarity(getArrayBoolean(&This->inputs, 0), P_BOTHTRUEFALSE);
+ updatePolarity(getArrayBoolean(&This->inputs, 1), P_BOTHTRUEFALSE);
+ break;
+ }
+ case L_IMPLIES: {
+ Boolean *left = getArrayBoolean(&This->inputs, 0);
+ updatePolarity(left, negatePolarity( parentpolarity));
+ Boolean *right = getArrayBoolean(&This->inputs, 1);
+ updatePolarity(right, parentpolarity);
+ break;
+ }
+ default:
+ ASSERT(0);
+ }
+}
+
+void computeLogicOpBooleanValue(BooleanLogic *This) {
+ BooleanValue parentbv = GETBOOLEANVALUE(This);
+ switch (This->op) {
+ case L_AND: {
+ if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
+ uint size = getSizeArrayBoolean(&This->inputs);
+ for (uint i = 0; i < size; i++) {
+ updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
+ }
+ }
+ return;
+ }
+ case L_OR: {
+ if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
+ uint size = getSizeArrayBoolean(&This->inputs);
+ for (uint i = 0; i < size; i++) {
+ updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
+ }
+ }
+ return;
+ }
+ case L_NOT:
+ updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
+ return;
+ case L_IMPLIES:
+ //implies is really an or with the first term negated
+ if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
+ uint size = getSizeArrayBoolean(&This->inputs);
+ updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
+ updateMustValue(getArrayBoolean(&This->inputs, 1), parentbv);
+ }
+ return;
+ case L_XOR:
+ return;
+ default:
+ ASSERT(0);
+ }
+}
--- /dev/null
+/*
+ * File: polarityassignment.h
+ * Author: hamed
+ *
+ * Created on August 6, 2017, 12:18 PM
+ */
+
+#ifndef POLARITYASSIGNMENT_H
+#define POLARITYASSIGNMENT_H
+#include "classlist.h"
+#include "mymemory.h"
+#include "common.h"
+#include "ops.h"
+#include "boolean.h"
+
+void computePolarities(CSolver *This);
+void updatePolarity(Boolean *This, Polarity polarity);
+void updateMustValue(Boolean *This, BooleanValue value);
+void computePolarityAndBooleanValue(Boolean *boolean);
+void computePredicatePolarityAndBooleanValue(BooleanPredicate *This);
+void computeLogicOpPolarityAndBooleanValue(BooleanLogic *boolean);
+Polarity negatePolarity(Polarity This);
+BooleanValue negateBooleanValue(BooleanValue This);
+void computeLogicOpPolarity(BooleanLogic *boolean);
+void computeLogicOpBooleanValue(BooleanLogic *boolean);
+
+#endif/* POLARITYASSIGNMENT_H */
+++ /dev/null
-#include "orderedge.h"
-#include "ordergraph.h"
-
-OrderEdge *allocOrderEdge(OrderNode *source, OrderNode *sink) {
- OrderEdge *This = (OrderEdge *) ourmalloc(sizeof(OrderEdge));
- This->source = source;
- This->sink = sink;
- This->polPos = false;
- This->polNeg = false;
- This->mustPos = false;
- This->mustNeg = false;
- This->pseudoPos = false;
- return This;
-}
-
-void deleteOrderEdge(OrderEdge *This) {
- ourfree(This);
-}
-
+++ /dev/null
-/*
- * File: orderedge.h
- * Author: hamed
- *
- * Created on August 7, 2017, 3:44 PM
- */
-
-#ifndef ORDEREDGE_H
-#define ORDEREDGE_H
-#include "classlist.h"
-#include "mymemory.h"
-
-struct OrderEdge {
- OrderNode *source;
- OrderNode *sink;
- unsigned int polPos : 1;
- 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 */
-
+++ /dev/null
-#include "ordergraph.h"
-#include "ordernode.h"
-#include "boolean.h"
-#include "orderedge.h"
-#include "ordergraph.h"
-#include "order.h"
-
-OrderGraph *allocOrderGraph(Order *order) {
- OrderGraph *This = (OrderGraph *) ourmalloc(sizeof(OrderGraph));
- This->nodes = allocHashSetOrderNode(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
- This->edges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
- This->order = order;
- return This;
-}
-
-OrderGraph *buildOrderGraph(Order *order) {
- OrderGraph *orderGraph = allocOrderGraph(order);
- uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
- for (uint j = 0; j < constrSize; j++) {
- addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
- }
- return orderGraph;
-}
-
-//Builds only the subgraph for the must order graph.
-OrderGraph *buildMustOrderGraph(Order *order) {
- OrderGraph *orderGraph = allocOrderGraph(order);
- uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
- for (uint j = 0; j < constrSize; j++) {
- addMustOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
- }
- return orderGraph;
-}
-
-void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
- Polarity polarity = constr->polarity;
- BooleanValue mustval = constr->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->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);
- } 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);
- }
- break;
- }
- case P_UNDEFINED:
- //There is an unreachable order constraint if this assert fires
- ASSERT(0);
- }
-}
-
-void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
- BooleanValue mustval = constr->boolVal;
- Order *order = graph->order;
- switch (mustval) {
- case BV_UNSAT:
- case BV_MUSTBETRUE: {
- OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
- _1to2->mustPos = true;
- _1to2->polPos = true;
- addNewOutgoingEdge(node1, _1to2);
- addNewIncomingEdge(node2, _1to2);
- if (constr->boolVal == BV_MUSTBETRUE)
- break;
- }
- case BV_MUSTBEFALSE: {
- if (order->type == TOTAL) {
- OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(graph, node2, node1);
- _2to1->mustPos = true;
- _2to1->polPos = true;
- addNewOutgoingEdge(node2, _2to1);
- addNewIncomingEdge(node1, _2to1);
- } else {
- OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(graph, node1, node2);
- _1to2->mustNeg = true;
- _1to2->polNeg = true;
- addNewOutgoingEdge(node1, _1to2);
- addNewIncomingEdge(node2, _1to2);
- }
- break;
- }
- case BV_UNDEFINED:
- //Do Nothing
- break;
- }
-}
-
-OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
- OrderNode *node = allocOrderNode(id);
- OrderNode *tmp = getHashSetOrderNode(graph->nodes, node);
- if ( tmp != NULL) {
- deleteOrderNode(node);
- node = tmp;
- } else {
- addHashSetOrderNode(graph->nodes, node);
- }
- return node;
-}
-
-OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
- OrderNode node = {id, NULL, NULL, NOTVISITED, 0};
- OrderNode *tmp = getHashSetOrderNode(graph->nodes, &node);
- return tmp;
-}
-
-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 {
- addHashSetOrderEdge(graph->edges, edge);
- }
- return edge;
-}
-
-OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end) {
- OrderEdge edge = {begin, end, 0, 0, 0, 0, 0};
- OrderEdge *tmp = getHashSetOrderEdge(graph->edges, &edge);
- return tmp;
-}
-
-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, BooleanOrder *bOrder) {
- OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
- OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
- addOrderEdge(graph, from, to, bOrder);
-}
-
-void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
- OrderNode *from = getOrderNodeFromOrderGraph(graph, bOrder->first);
- OrderNode *to = getOrderNodeFromOrderGraph(graph, bOrder->second);
- addMustOrderEdge(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);
- deleteOrderEdge(edge);
- }
- deleteIterOrderEdge(eiterator);
- deleteHashSetOrderNode(graph->nodes);
- deleteHashSetOrderEdge(graph->edges);
- ourfree(graph);
-}
+++ /dev/null
-/*
- * File: ordergraph.h
- * Author: hamed
- *
- * Created on August 7, 2017, 3:42 PM
- */
-
-#ifndef ORDERGRAPH_H
-#define ORDERGRAPH_H
-#include "classlist.h"
-#include "structs.h"
-#include "mymemory.h"
-
-struct OrderGraph {
- HashSetOrderNode *nodes;
- HashSetOrderEdge *edges;
- Order *order;
-};
-
-OrderGraph *allocOrderGraph(Order *order);
-OrderGraph *buildOrderGraph(Order *order);
-OrderGraph *buildMustOrderGraph(Order *order);
-void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
-void addMustOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder);
-OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
-OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
-OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id);
-OrderEdge *lookupOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, OrderNode *end);
-void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
-void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
-void deleteOrderGraph(OrderGraph *graph);
-OrderEdge *getInverseOrderEdge(OrderGraph *graph, OrderEdge *edge);
-#endif/* ORDERGRAPH_H */
-
+++ /dev/null
-#include "ordernode.h"
-#include "orderedge.h"
-
-OrderNode *allocOrderNode(uint64_t id) {
- OrderNode *This = (OrderNode *) ourmalloc(sizeof(OrderNode));
- This->id = id;
- This->inEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
- This->outEdges = allocHashSetOrderEdge(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
- This->status = NOTVISITED;
- This->sccNum = 0;
- 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) {
- deleteHashSetOrderEdge(node->inEdges);
- deleteHashSetOrderEdge(node->outEdges);
- ourfree(node);
-}
+++ /dev/null
-
-/*
- * File: ordernode.h
- * Author: hamed
- *
- * Created on August 7, 2017, 3:43 PM
- */
-
-#ifndef ORDERNODE_H
-#define ORDERNODE_H
-
-#include "classlist.h"
-#include "mymemory.h"
-#include "structs.h"
-#include "orderedge.h"
-
-enum NodeStatus {NOTVISITED, VISITED, FINISHED, ADDEDTOSET};
-typedef enum NodeStatus NodeStatus;
-
-struct OrderNode {
- uint64_t id;
- HashSetOrderEdge *inEdges;
- HashSetOrderEdge *outEdges;
- NodeStatus status;
- uint sccNum;
-};
-
-OrderNode *allocOrderNode(uint64_t id);
-void addNewIncomingEdge(OrderNode *node, OrderEdge *edge);
-void addNewOutgoingEdge(OrderNode *node, OrderEdge *edge);
-void deleteOrderNode(OrderNode *node);
-
-#endif/* ORDERNODE_H */
-
+++ /dev/null
-#include "polarityassignment.h"
-#include "csolver.h"
-
-void computePolarities(CSolver *This) {
- HSIteratorBoolean *iterator=iteratorBoolean(This->constraints);
- while(hasNextBoolean(iterator)) {
- Boolean *boolean = nextBoolean(iterator);
- updatePolarity(boolean, P_TRUE);
- updateMustValue(boolean, BV_MUSTBETRUE);
- computePolarityAndBooleanValue(boolean);
- }
- deleteIterBoolean(iterator);
-}
-
-void updatePolarity(Boolean *This, Polarity polarity) {
- This->polarity = (Polarity) (This->polarity | polarity);
-}
-
-void updateMustValue(Boolean *This, BooleanValue value) {
- This->boolVal = (BooleanValue) (This->boolVal | value);
-}
-
-void computePolarityAndBooleanValue(Boolean *This) {
- switch (GETBOOLEANTYPE(This)) {
- case BOOLEANVAR:
- case ORDERCONST:
- return;
- case PREDICATEOP:
- return computePredicatePolarityAndBooleanValue((BooleanPredicate *)This);
- case LOGICOP:
- return computeLogicOpPolarityAndBooleanValue((BooleanLogic *)This);
- default:
- ASSERT(0);
- }
-}
-
-void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
- if (This->undefStatus != NULL) {
- updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
- computePolarityAndBooleanValue(This->undefStatus);
- }
-}
-
-void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {
- computeLogicOpBooleanValue(This);
- computeLogicOpPolarity(This);
- uint size = getSizeArrayBoolean(&This->inputs);
- for (uint i = 0; i < size; i++) {
- computePolarityAndBooleanValue(getArrayBoolean(&This->inputs, i));
- }
-}
-
-Polarity negatePolarity(Polarity This) {
- switch (This) {
- case P_UNDEFINED:
- case P_BOTHTRUEFALSE:
- return This;
- case P_TRUE:
- return P_FALSE;
- case P_FALSE:
- return P_TRUE;
- default:
- ASSERT(0);
- }
-}
-
-BooleanValue negateBooleanValue(BooleanValue This) {
- switch (This) {
- case BV_UNDEFINED:
- case BV_UNSAT:
- return This;
- case BV_MUSTBETRUE:
- return BV_MUSTBEFALSE;
- case BV_MUSTBEFALSE:
- return BV_MUSTBETRUE;
- default:
- ASSERT(0);
- }
-}
-
-void computeLogicOpPolarity(BooleanLogic *This) {
- Polarity parentpolarity = GETBOOLEANPOLARITY(This);
- switch (This->op) {
- case L_AND:
- case L_OR: {
- uint size = getSizeArrayBoolean(&This->inputs);
- for (uint i = 0; i < size; i++) {
- Boolean *tmp = getArrayBoolean(&This->inputs, i);
- updatePolarity(tmp, parentpolarity);
- }
- break;
- }
- case L_NOT: {
- Boolean *tmp = getArrayBoolean(&This->inputs, 0);
- updatePolarity(tmp, negatePolarity(parentpolarity));
- break;
- }
- case L_XOR: {
- updatePolarity(getArrayBoolean(&This->inputs, 0), P_BOTHTRUEFALSE);
- updatePolarity(getArrayBoolean(&This->inputs, 1), P_BOTHTRUEFALSE);
- break;
- }
- case L_IMPLIES: {
- Boolean *left = getArrayBoolean(&This->inputs, 0);
- updatePolarity(left, negatePolarity( parentpolarity));
- Boolean *right = getArrayBoolean(&This->inputs, 1);
- updatePolarity(right, parentpolarity);
- break;
- }
- default:
- ASSERT(0);
- }
-}
-
-void computeLogicOpBooleanValue(BooleanLogic *This) {
- BooleanValue parentbv = GETBOOLEANVALUE(This);
- switch (This->op) {
- case L_AND: {
- if (parentbv == BV_MUSTBETRUE || parentbv == BV_UNSAT) {
- uint size = getSizeArrayBoolean(&This->inputs);
- for (uint i = 0; i < size; i++) {
- updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
- }
- }
- return;
- }
- case L_OR: {
- if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
- uint size = getSizeArrayBoolean(&This->inputs);
- for (uint i = 0; i < size; i++) {
- updateMustValue(getArrayBoolean(&This->inputs, i), parentbv);
- }
- }
- return;
- }
- case L_NOT:
- updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
- return;
- case L_IMPLIES:
- //implies is really an or with the first term negated
- if (parentbv == BV_MUSTBEFALSE || parentbv == BV_UNSAT) {
- uint size = getSizeArrayBoolean(&This->inputs);
- updateMustValue(getArrayBoolean(&This->inputs, 0), negateBooleanValue(parentbv));
- updateMustValue(getArrayBoolean(&This->inputs, 1), parentbv);
- }
- return;
- case L_XOR:
- return;
- default:
- ASSERT(0);
- }
-}
+++ /dev/null
-/*
- * File: polarityassignment.h
- * Author: hamed
- *
- * Created on August 6, 2017, 12:18 PM
- */
-
-#ifndef POLARITYASSIGNMENT_H
-#define POLARITYASSIGNMENT_H
-#include "classlist.h"
-#include "mymemory.h"
-#include "common.h"
-#include "ops.h"
-#include "boolean.h"
-
-void computePolarities(CSolver *This);
-void updatePolarity(Boolean *This, Polarity polarity);
-void updateMustValue(Boolean *This, BooleanValue value);
-void computePolarityAndBooleanValue(Boolean *boolean);
-void computePredicatePolarityAndBooleanValue(BooleanPredicate *This);
-void computeLogicOpPolarityAndBooleanValue(BooleanLogic *boolean);
-Polarity negatePolarity(Polarity This);
-BooleanValue negateBooleanValue(BooleanValue This);
-void computeLogicOpPolarity(BooleanLogic *boolean);
-void computeLogicOpBooleanValue(BooleanLogic *boolean);
-
-#endif/* POLARITYASSIGNMENT_H */
MKDIR_P = mkdir -p
OBJ_DIR = bin
-CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc)
+CPP_SOURCES := $(wildcard *.cc) $(wildcard AST/*.cc) $(wildcard ASTTransform/*.cc) $(wildcard ASTAnalyses/*.cc) $(wildcard Tuner/*.cc) $(wildcard Collections/*.cc) $(wildcard Backend/*.cc) $(wildcard Encoders/*.cc)
-HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h)
+HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h)
OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o)
CFLAGS := -Wall -g -O0
-CFLAGS += -IAST -ICollections -IBackend -I. -IEncoders -ITuner
+CFLAGS += -IAST -IASTTransform -IASTAnalyses -ICollections -IBackend -I. -IEncoders -ITuner
LDFLAGS := -ldl -lrt -rdynamic
SHARED := -shared
${OBJ_DIR}:
${MKDIR_P} ${OBJ_DIR}
${MKDIR_P} ${OBJ_DIR}/AST
+ ${MKDIR_P} ${OBJ_DIR}/ASTAnalyses
+ ${MKDIR_P} ${OBJ_DIR}/ASTTransform
${MKDIR_P} ${OBJ_DIR}/Tuner
${MKDIR_P} ${OBJ_DIR}/Collections
${MKDIR_P} ${OBJ_DIR}/Backend
projects / satune.git / commitdiff