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 uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){
  17         uint index=0;
  18         for(int i=elemEnc->numVars-1;i>=0;i--) {
  19                 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
  20                         index = i;
  21         }
  22         ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
  23         return elemEnc->encodingArray[index];
  24 }
  25 uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
  26         switch(getElementEncoding(element)->type){
  27                 case ONEHOT:
  28                         ASSERT(0);
  29                         break;
  30                 case UNARY:
  31                         ASSERT(0);
  32                         break;
  33                 case BINARYINDEX:
  34                         return getElementValueBinaryIndexSATTranslator(This, getElementEncoding(element));
  35                 case ONEHOTBINARY:
  36                         ASSERT(0);
  37                         break;
  38                 case BINARYVAL:
  39                         ASSERT(0);
  40                         break;
  41                 default:
  42                         ASSERT(0);
  43                         break;
  44         }
  45 }
  46
  47 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
  48         int index = getEdgeVar( ((BooleanVar*) boolean)->var );
  49         return This->satEncoder->cnf->solver->solution[index] == true;
  50 }