From ae9f38b4b72822a5a73909a795043bfcbb534e2f Mon Sep 17 00:00:00 2001 From: bdemsky Date: Tue, 22 Aug 2017 16:36:07 -0700 Subject: [PATCH] Add option to optimize edges in final encoding --- src/AST/order.c | 1 + src/AST/order.h | 1 + src/Backend/satencoder.c | 3 +- src/Backend/satencoder.h | 3 +- src/Backend/satorderencoder.c | 44 +++++++++++++++++---- src/Backend/satorderencoder.h | 2 +- src/Encoders/orderencoder.c | 10 ----- src/Encoders/orderencoder.h | 1 - src/Encoders/ordergraph.c | 73 +++++++++++++++++++++++++++++++++++ src/Encoders/ordergraph.h | 6 +++ src/Tuner/tunable.h | 4 +- src/csolver.c | 2 +- 12 files changed, 127 insertions(+), 23 deletions(-) diff --git a/src/AST/order.c b/src/AST/order.c index fde8c1f..3e0f73e 100644 --- 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 53bf878..c5a03a8 100644 --- 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 f380fdd..f5362b8 100644 --- 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 8db6239..dee131d 100644 --- 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 0b2622d..c3ee2a2 100644 --- 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 53d7415..e3342bf 100644 --- 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 e97a17b..e172d18 100644 --- 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 b0c13ac..67a56b9 100644 --- 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 c47a16f..f920076 100644 --- 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 5540d73..33f2b69 100644 --- 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 66c4638..cbd9f29 100644 --- 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 fbc8691..e9c9526 100644 --- 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; } -- 2.34.1