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 getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
  18         uint64_t value=0;
  19         for(int i=elemEnc->numVars-1;i>=0;i--) {
  20                 value=value<<1;
  21                 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
  22                         value |= 1;
  23         }
  24         return value;
  25 }
  26
  27 uint64_t getElementValueOneHotSATTranslator(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 getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc){
  38         uint index=0;
  39         for(int i=elemEnc->numVars-1;i>=0;i--) {
  40                 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
  41                         index = i;
  42         }
  43         ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
  44         return elemEnc->encodingArray[index];
  45 }
  46
  47 uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
  48         ElementEncoding* elemEnc = getElementEncoding(element);
  49         switch(elemEnc->type){
  50                 case ONEHOT:
  51                         getElementValueOneHotSATTranslator(This, elemEnc);
  52                         break;
  53                 case UNARY:
  54                         getElementValueUnarySATTranslator(This, elemEnc);
  55                         break;
  56                 case BINARYINDEX:
  57                         return getElementValueBinaryIndexSATTranslator(This, elemEnc);
  58                 case ONEHOTBINARY:
  59                         ASSERT(0);
  60                         break;
  61                 case BINARYVAL:
  62                         ASSERT(0);
  63                         break;
  64                 default:
  65                         ASSERT(0);
  66                         break;
  67         }
  68         return -1;
  69 }
  70
  71 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
  72         int index = getEdgeVar( ((BooleanVar*) boolean)->var );
  73         return This->satEncoder->cnf->solver->solution[index] == true;
  74 }