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 getElementValueSATTranslator(CSolver* This, Element* element){
  17         switch(getElementEncoding(element)->type){
  18                 case ONEHOT:
  19                         ASSERT(0);
  20                         break;
  21                 case UNARY:
  22                         ASSERT(0);
  23                         break;
  24                 case BINARYINDEX:
  25                         return getElementValueBinaryIndexSATTranslator(This, getElementEncoding(element));
  26                 case ONEHOTBINARY:
  27                         ASSERT(0);
  28                         break;
  29                 case BINARYVAL:
  30                         ASSERT(0);
  31                         break;
  32                 default:
  33                         ASSERT(0);
  34                         break;
  35         }
  36 }
  37
  38 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
  39         int index = getEdgeVar( ((BooleanVar*) boolean)->var );
  40         return This->satEncoder->cnf->solver->solution[index] == true;
  41 }