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