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 }