Add option to optimize edges in final encoding

diff --git a/src/AST/order.c b/src/AST/order.c
index fde8c1f05f7256d35527d6cf074bc7a79211f1f5..3e0f73e285bcab0d0c88a95de824c5b21d4430ab 100644 (file)
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -10,6 +10,7 @@ Order *allocOrder(OrderType type, Set *set) {
        This->type = type;
        initOrderEncoding(&This->order, This);
        This->orderPairTable = NULL;
+       This->graph = NULL;
        return This;
 }
 

diff --git a/src/AST/order.h b/src/AST/order.h
index 53bf878f063a71a4c8ec11c626dcb673d6857f6f..c5a03a84f455b31e923867e23e1f8c4b70631cc5 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -11,6 +11,7 @@ struct Order {
        OrderType type;
        Set *set;
        HashTableOrderPair *orderPairTable;
+       OrderGraph *graph;
        VectorBooleanOrder constraints;
        OrderEncoding order;
 };

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index f380fdd3858a692ee0ae3cc27328e73709aa78a8..f5362b882160095f38babade394286bc6b79709d 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -15,8 +15,9 @@
 
 //TODO: Should handle sharing of AST Nodes without recoding them a second time
 
-SATEncoder *allocSATEncoder() {
+SATEncoder *allocSATEncoder(CSolver *solver) {
        SATEncoder *This = ourmalloc(sizeof (SATEncoder));
+       This->solver = solver;
        This->varcount = 1;
        This->cnf = createCNF();
        return This;

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 8db6239bff6ae5e9033a3fabd8030dc14bafd223..dee131dc5b4dd584962e0e20d000d76fcad8f3c9 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -9,13 +9,14 @@
 struct SATEncoder {
        uint varcount;
        CNF *cnf;
+       CSolver *solver;
 };
 
 #include "satelemencoder.h"
 #include "satorderencoder.h"
 #include "satfunctableencoder.h"
 
-SATEncoder *allocSATEncoder();
+SATEncoder *allocSATEncoder(CSolver *solver);
 void deleteSATEncoder(SATEncoder *This);
 void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This);
 Edge getNewVarSATEncoder(SATEncoder *This);

diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index 0b2622d0d96d66246bfbf9bc5e3709cd917d230a..c3ee2a2838db9b867132d3e88b55ad9d7f42e3ce 100644 (file)
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -2,8 +2,13 @@
 #include "structs.h"
 #include "common.h"
 #include "order.h"
+#include "csolver.h"
 #include "orderpair.h"
 #include "set.h"
+#include "tunable.h"
+#include "orderencoder.h"
+#include "ordergraph.h"
+#include "orderedge.h"
 
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
        switch ( constraint->order->type) {
@@ -17,7 +22,29 @@ Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
        return E_BOGUS;
 }
 
-Edge getPairConstraint(SATEncoder *This, HashTableOrderPair *table, OrderPair *pair) {
+Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
+       if (order->graph != NULL) {
+               OrderGraph *graph=order->graph;
+               OrderNode *first=lookupOrderNodeFromOrderGraph(graph, pair->first);
+               OrderNode *second=lookupOrderNodeFromOrderGraph(graph, pair->second);
+               if ((first != NULL) && (second != NULL)) {
+                       OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
+                       if (edge != NULL) {
+                               if (edge->mustPos)
+                                       return E_True;
+                               else if (edge->mustNeg)
+                                       return E_False;
+                       }
+                       OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, first, second);
+                       if (invedge != NULL) {
+                               if (invedge->mustPos)
+                                       return E_False;
+                               else if (invedge->mustNeg)
+                                       return E_True;
+                       }
+               }
+       }
+       HashTableOrderPair *table = order->orderPairTable;
        bool negate = false;
        OrderPair flipped;
        if (pair->first < pair->second) {
@@ -41,11 +68,15 @@ Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
        ASSERT(boolOrder->order->type == TOTAL);
        if (boolOrder->order->orderPairTable == NULL) {
                initializeOrderHashTable(boolOrder->order);
+               bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+               if (doOptOrderStructure) {
+                       boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
+                       reachMustAnalysis(This->solver, boolOrder->order->graph, true);
+               }
                createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
        }
-       HashTableOrderPair *orderPairTable = boolOrder->order->orderPairTable;
        OrderPair pair = {boolOrder->first, boolOrder->second, E_NULL};
-       Edge constraint = getPairConstraint(This, orderPairTable, &pair);
+       Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
        return constraint;
 }
 
@@ -56,20 +87,19 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
 #endif
        ASSERT(order->type == TOTAL);
        VectorInt *mems = order->set->members;
-       HashTableOrderPair *table = order->orderPairTable;
        uint size = getSizeVectorInt(mems);
        for (uint i = 0; i < size; i++) {
                uint64_t valueI = getVectorInt(mems, i);
                for (uint j = i + 1; j < size; j++) {
                        uint64_t valueJ = getVectorInt(mems, j);
                        OrderPair pairIJ = {valueI, valueJ};
-                       Edge constIJ = getPairConstraint(This, table, &pairIJ);
+                       Edge constIJ = getPairConstraint(This, order, &pairIJ);
                        for (uint k = j + 1; k < size; k++) {
                                uint64_t valueK = getVectorInt(mems, k);
                                OrderPair pairJK = {valueJ, valueK};
                                OrderPair pairIK = {valueI, valueK};
-                               Edge constIK = getPairConstraint(This, table, &pairIK);
-                               Edge constJK = getPairConstraint(This, table, &pairJK);
+                               Edge constIK = getPairConstraint(This, order, &pairIK);
+                               Edge constJK = getPairConstraint(This, order, &pairJK);
                                addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
                        }
                }

diff --git a/src/Backend/satorderencoder.h b/src/Backend/satorderencoder.h
index 53d741563b164a1fcc269a2c024e41c6266b7870..e3342bfcc3532b4fb0bf8e65aff3687e9c6dddf7 100644 (file)
--- a/src/Backend/satorderencoder.h
+++ b/src/Backend/satorderencoder.h
@@ -2,7 +2,7 @@
 #define SATORDERENCODER_H
 
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
-Edge getPairConstraint(SATEncoder *This, HashTableOrderPair *table, OrderPair *pair);
+Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair);
 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint);
 void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order);

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index e97a17b2dcf1d064f1ebceb4c70a5dd61877e1f2..e172d18503636169b2ef899e7aaa69e0e0f744f9 100644 (file)
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -9,15 +9,6 @@
 #include "mutableset.h"
 #include "tunable.h"
 
-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;
-}
-
 void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
        HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
        while (hasNextOrderNode(iterator)) {
@@ -398,7 +389,6 @@ void orderAnalysis(CSolver *This) {
        uint size = getSizeVectorOrder(This->allOrders);
        for (uint i = 0; i < size; i++) {
                Order *order = getVectorOrder(This->allOrders, i);
-               TunableDesc onoff={9, 1, 1};
                bool doDecompose=GETVARTUNABLE(This->tuner, order->type, DECOMPOSEORDER, &onoff);
                if (!doDecompose)
                        continue;

diff --git a/src/Encoders/orderencoder.h b/src/Encoders/orderencoder.h
index b0c13acd1fb4387805ee2db2771a0bac5b0520da..67a56b9813cb11eb26e097073927ba78e294b878 100644 (file)
--- a/src/Encoders/orderencoder.h
+++ b/src/Encoders/orderencoder.h
@@ -11,7 +11,6 @@
 #include "structs.h"
 #include "mymemory.h"
 
-OrderGraph *buildOrderGraph(Order *order);
 void computeStronglyConnectedComponentGraph(OrderGraph *graph);
 void orderAnalysis(CSolver *solver);
 void initializeNodeInfoSCC(OrderGraph *graph);

diff --git a/src/Encoders/ordergraph.c b/src/Encoders/ordergraph.c
index c47a16f7d5c74529c90d35e3d4b5a93b4cb4b2e7..f92007650c5b0e5ee179e7ad84c5acacfa8cd022 100644 (file)
--- a/src/Encoders/ordergraph.c
+++ b/src/Encoders/ordergraph.c
@@ -13,6 +13,25 @@ OrderGraph *allocOrderGraph(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->base.polarity;
        BooleanValue mustval = constr->base.boolVal;
@@ -53,6 +72,42 @@ void addOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, Boolean
        }
 }
 
+void addMustOrderEdge(OrderGraph *graph, OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
+       BooleanValue mustval = constr->base.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->base.polarity == 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);
@@ -65,6 +120,12 @@ OrderNode *getOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
        return node;
 }
 
+OrderNode *lookupOrderNodeFromOrderGraph(OrderGraph *graph, uint64_t id) {
+       OrderNode node = {id, NULL, NULL, 0, 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);
@@ -77,6 +138,12 @@ OrderEdge *getOrderEdgeFromOrderGraph(OrderGraph *graph, OrderNode *begin, Order
        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);
@@ -89,6 +156,12 @@ void addOrderConstraintToOrderGraph(OrderGraph *graph, BooleanOrder *bOrder) {
        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)) {

diff --git a/src/Encoders/ordergraph.h b/src/Encoders/ordergraph.h
index 5540d73ddc266eb79865011c19a8f666a8026ca9..33f2b69cab59121f7e0033c0a3d44e2b6ba12d4d 100644 (file)
--- a/src/Encoders/ordergraph.h
+++ b/src/Encoders/ordergraph.h
@@ -18,10 +18,16 @@ struct OrderGraph {
 };
 
 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 */

diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 66c46381f5f2aa63a80751e7176507e82bd962e3..cbd9f29898b3c4921b5a63fc859d8ed20828d2f2 100644 (file)
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -21,6 +21,8 @@ int getVarTunable(Tuner *This, VarType vartype, TunableParam param, TunableDesc
 #define GETTUNABLE(This, param, descriptor) getTunable(This, param, descriptor)
 #define GETVARTUNABLE(This, vartype, param, descriptor) getTunable(This, param, descriptor)
 
-enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE};
+static TunableDesc onoff={0, 1, 1};
+static TunableDesc offon={0, 1, 0};
+enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE};
 typedef enum Tunables Tunables;
 #endif

diff --git a/src/csolver.c b/src/csolver.c
index fbc86914af04d8f6439ced323c4e0769811da14e..e9c9526e14d9861273c9793fda12f2d3e26a5756 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -24,8 +24,8 @@ CSolver *allocCSolver() {
        This->allTables = allocDefVectorTable();
        This->allOrders = allocDefVectorOrder();
        This->allFunctions = allocDefVectorFunction();
-       This->satEncoder = allocSATEncoder();
        This->tuner = allocTuner();
+       This->satEncoder = allocSATEncoder(This);
        return This;
 }