src/Backend/satorderencoder.c

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