src/Backend/sattranslator.c

   1 #include "sattranslator.h"
   2 #include "element.h"
   3 #include "csolver.h"
   4 #include "satencoder.h"
   5 #include "set.h"
   6 #include "order.h"
   7 #include "orderpair.h"
   8
   9 uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
  10         uint index=0;
  11         for(int i=elemEnc->numVars-1;i>=0;i--) {
  12                 index=index<<1;
  13                 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
  14                         index |= 1;
  15         }
  16         ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
  17         return elemEnc->encodingArray[index];
  18 }
  19
  20 uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
  21         //THIS WILL PROBABLY BE WRONG SINCE THE VALUES CAN BE OFFSET
  22         uint64_t value=0;
  23         for(int i=elemEnc->numVars-1;i>=0;i--) {
  24                 value=value<<1;
  25                 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
  26                         value |= 1;
  27         }
  28         return value;
  29 }
  30
  31 uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){
  32         uint index=0;
  33         for(int i=elemEnc->numVars-1;i>=0;i--) {
  34                 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
  35                         index = i;
  36         }
  37         ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
  38         return elemEnc->encodingArray[index];
  39 }
  40
  41 uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc){
  42         uint i;
  43         for(i=0;i<elemEnc->numVars;i++) {
  44                 if (!This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ]) {
  45                         break;
  46                 }
  47         }
  48
  49         return elemEnc->encodingArray[i];
  50 }
  51
  52 uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
  53         ElementEncoding* elemEnc = getElementEncoding(element);
  54         if(elemEnc->numVars == 0)       //case when the set has only one item
  55                 return getSetElement(getElementSet(element), 0);
  56         switch(elemEnc->type){
  57                 case ONEHOT:
  58                         getElementValueOneHotSATTranslator(This, elemEnc);
  59                         break;
  60                 case UNARY:
  61                         getElementValueUnarySATTranslator(This, elemEnc);
  62                         break;
  63                 case BINARYINDEX:
  64                         return getElementValueBinaryIndexSATTranslator(This, elemEnc);
  65                 case ONEHOTBINARY:
  66                         ASSERT(0);
  67                         break;
  68                 case BINARYVAL:
  69                         ASSERT(0);
  70                         break;
  71                 default:
  72                         ASSERT(0);
  73                         break;
  74         }
  75         return -1;
  76 }
  77
  78 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
  79         int index = getEdgeVar( ((BooleanVar*) boolean)->var );
  80         return This->satEncoder->cnf->solver->solution[index] == true;
  81 }
  82
  83 HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second){
  84         ASSERT(order->orderPairTable!= NULL);
  85         OrderPair pair={first, second, E_NULL};
  86         Edge var = getOrderConstraint(order->orderPairTable, & pair);
  87         if(edgeIsNull(var))
  88                 return UNORDERED;
  89         int index = getEdgeVar( var );
  90         return This->satEncoder->cnf->solver->solution[index] ? FIRST: SECOND;
  91 }
  92