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         uint csize =0;
  62         for(uint i=0; i<size; i++){
  63                 uint64_t valueI = getVectorInt(mems, i);
  64                 for(uint j=i+1; j<size;j++){
  65                         uint64_t valueJ = getVectorInt(mems, j);
  66                         OrderPair pairIJ = {valueI, valueJ};
  67                         Edge constIJ=getPairConstraint(This, table, & pairIJ);
  68                         for(uint k=j+1; k<size; k++){
  69                                 uint64_t valueK = getVectorInt(mems, k);
  70                                 OrderPair pairJK = {valueJ, valueK};
  71                                 OrderPair pairIK = {valueI, valueK};
  72                                 Edge constIK = getPairConstraint(This, table, & pairIK);
  73                                 Edge constJK = getPairConstraint(This, table, & pairJK);
  74                                 addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
  75                         }
  76                 }
  77         }
  78 }
  79
  80 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){
  81         ASSERT(pair->first!= pair->second);
  82         bool negate = false;
  83         OrderPair flipped;
  84         if (pair->first < pair->second) {
  85                 negate=true;
  86                 flipped.first=pair->second;
  87                 flipped.second=pair->first;
  88                 pair = &flipped;
  89         }
  90         if (!containsOrderPair(table, pair)) {
  91                 return E_NULL;
  92         }
  93         Edge constraint= getOrderPair(table, pair)->constraint;
  94         ASSERT(!edgeIsNull(constraint));
  95         return negate ? constraintNegate(constraint) : constraint;
  96 }
  97
  98 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){
  99         Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
 100         Edge loop1= constraintOR(This->cnf, 3, carray);
 101         Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
 102         Edge loop2= constraintOR(This->cnf, 3, carray2 );
 103         return constraintAND2(This->cnf, loop1, loop2);
 104 }
 105
 106 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
 107         ASSERT(constraint->order->type == PARTIAL);
 108         return E_BOGUS;
 109 }