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