src/Backend/sattranslator.c

   1 #include "sattranslator.h"
   2 #include "element.h"
   3 #include "csolver.h"
   4 #include "satencoder.h"
   5
   6 uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
   7         uint index=0;
   8         for(int i=elemEnc->numVars-1;i>=0;i--) {
   9                 index=index<<1;
  10                 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
  11                         index |= 1;
  12         }
  13         ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
  14         return elemEnc->encodingArray[index];
  15 }
  16
  17 uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){
  18         uint index=0;
  19         for(int i=elemEnc->numVars-1;i>=0;i--) {
  20                 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
  21                         index = i;
  22         }
  23         ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
  24         return elemEnc->encodingArray[index];
  25 }
  26
  27 uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc){
  28         uint index=0;
  29         for(int i=elemEnc->numVars-1;i>=0;i--) {
  30                 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
  31                         index = i;
  32         }
  33         ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
  34         return elemEnc->encodingArray[index];
  35 }
  36
  37 uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
  38         ElementEncoding* elemEnc = getElementEncoding(element);
  39         switch(elemEnc->type){
  40                 case ONEHOT:
  41                         getElementValueOneHotSATTranslator(This, elemEnc);
  42                         break;
  43                 case UNARY:
  44                         getElementValueUnarySATTranslator(This, elemEnc);
  45                         break;
  46                 case BINARYINDEX:
  47                         return getElementValueBinaryIndexSATTranslator(This, elemEnc);
  48                 case ONEHOTBINARY:
  49                         ASSERT(0);
  50                         break;
  51                 case BINARYVAL:
  52                         ASSERT(0);
  53                         break;
  54                 default:
  55                         ASSERT(0);
  56                         break;
  57         }
  58         return -1;
  59 }
  60
  61 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
  62         int index = getEdgeVar( ((BooleanVar*) boolean)->var );
  63         return This->satEncoder->cnf->solver->solution[index] == true;
  64 }