src/Backend/satorderencoder.c

   1 #include "satencoder.h"
   2 #include "structs.h"
   3 #include "common.h"
   4 #include "order.h"
   5 #include "csolver.h"
   6 #include "orderpair.h"
   7 #include "set.h"
   8 #include "tunable.h"
   9 #include "orderencoder.h"
  10 #include "ordergraph.h"
  11 #include "orderedge.h"
  12
  13 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
  14         switch ( constraint->order->type) {
  15         case PARTIAL:
  16                 return encodePartialOrderSATEncoder(This, constraint);
  17         case TOTAL:
  18                 return encodeTotalOrderSATEncoder(This, constraint);
  19         default:
  20                 ASSERT(0);
  21         }
  22         return E_BOGUS;
  23 }
  24
  25 Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
  26         if (order->graph != NULL) {
  27                 OrderGraph *graph=order->graph;
  28                 OrderNode *first=lookupOrderNodeFromOrderGraph(graph, pair->first);
  29                 OrderNode *second=lookupOrderNodeFromOrderGraph(graph, pair->second);
  30                 if ((first != NULL) && (second != NULL)) {
  31                         OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
  32                         if (edge != NULL) {
  33                                 if (edge->mustPos)
  34                                         return E_True;
  35                                 else if (edge->mustNeg)
  36                                         return E_False;
  37                         }
  38                         OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first);
  39                         if (invedge != NULL) {
  40                                 if (invedge->mustPos)
  41                                         return E_False;
  42                                 else if (invedge->mustNeg)
  43                                         return E_True;
  44                         }
  45                 }
  46         }
  47         HashTableOrderPair *table = order->orderPairTable;
  48         bool negate = false;
  49         OrderPair flipped;
  50         if (pair->first < pair->second) {
  51                 negate = true;
  52                 flipped.first = pair->second;
  53                 flipped.second = pair->first;
  54                 pair = &flipped;
  55         }
  56         Edge constraint;
  57         if (!containsOrderPair(table, pair)) {
  58                 constraint = getNewVarSATEncoder(This);
  59                 OrderPair *paircopy = allocOrderPair(pair->first, pair->second, constraint);
  60                 putOrderPair(table, paircopy, paircopy);
  61         } else
  62                 constraint = getOrderPair(table, pair)->constraint;
  63
  64         return negate ? constraintNegate(constraint) : constraint;
  65 }
  66
  67 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
  68         ASSERT(boolOrder->order->type == TOTAL);
  69         if (boolOrder->order->orderPairTable == NULL) {
  70                 initializeOrderHashTable(boolOrder->order);
  71                 bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
  72                 if (doOptOrderStructure) {
  73                         boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
  74                         reachMustAnalysis(This->solver, boolOrder->order->graph, true);
  75                 }
  76                 createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
  77         }
  78         OrderPair pair = {boolOrder->first, boolOrder->second, E_NULL};
  79         Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
  80         return constraint;
  81 }
  82
  83
  84 void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
  85 #ifdef TRACE_DEBUG
  86         model_print("in total order ...\n");
  87 #endif
  88         ASSERT(order->type == TOTAL);
  89         VectorInt *mems = order->set->members;
  90         uint size = getSizeVectorInt(mems);
  91         for (uint i = 0; i < size; i++) {
  92                 uint64_t valueI = getVectorInt(mems, i);
  93                 for (uint j = i + 1; j < size; j++) {
  94                         uint64_t valueJ = getVectorInt(mems, j);
  95                         OrderPair pairIJ = {valueI, valueJ};
  96                         Edge constIJ = getPairConstraint(This, order, &pairIJ);
  97                         for (uint k = j + 1; k < size; k++) {
  98                                 uint64_t valueK = getVectorInt(mems, k);
  99                                 OrderPair pairJK = {valueJ, valueK};
 100                                 OrderPair pairIK = {valueI, valueK};
 101                                 Edge constIK = getPairConstraint(This, order, &pairIK);
 102                                 Edge constJK = getPairConstraint(This, order, &pairJK);
 103                                 addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
 104                         }
 105                 }
 106         }
 107 }
 108
 109 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
 110         ASSERT(pair->first != pair->second);
 111         bool negate = false;
 112         OrderPair flipped;
 113         if (pair->first < pair->second) {
 114                 negate = true;
 115                 flipped.first = pair->second;
 116                 flipped.second = pair->first;
 117                 pair = &flipped;
 118         }
 119         if (!containsOrderPair(table, pair)) {
 120                 return E_NULL;
 121         }
 122         Edge constraint = getOrderPair(table, pair)->constraint;
 123         ASSERT(!edgeIsNull(constraint));
 124         return negate ? constraintNegate(constraint) : constraint;
 125 }
 126
 127 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) {
 128         Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
 129         Edge loop1 = constraintOR(This->cnf, 3, carray);
 130         Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
 131         Edge loop2 = constraintOR(This->cnf, 3, carray2 );
 132         return constraintAND2(This->cnf, loop1, loop2);
 133 }
 134
 135 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
 136         ASSERT(constraint->order->type == PARTIAL);
 137         return E_BOGUS;
 138 }