src/Backend/sattranslator.c

   1 #include "sattranslator.h"
   2 #include "element.h"
   3 #include "csolver.h"
   4 #include "satencoder.h"
   5 #include "set.h"
   6 #include "order.h"
   7 #include "orderpair.h"
   8
   9 uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
  10         uint index=0;
  11         for(int i=elemEnc->numVars-1;i>=0;i--) {
  12                 index=index<<1;
  13                 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
  14                         index |= 1;
  15         }
  16         ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
  17         return elemEnc->encodingArray[index];
  18 }
  19
  20 uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
  21         uint64_t value=0;
  22         for(int i=elemEnc->numVars-1;i>=0;i--) {
  23                 value=value<<1;
  24                 if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
  25                         value |= 1;
  26         }
  27         if (elemEnc->isBinaryValSigned &&
  28                         This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars-1])]) {
  29                 //Do sign extension of negative number
  30                 uint64_t highbits=0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
  31                 value+=highbits;
  32         }
  33         value+=elemEnc->offset;
  34         return value;
  35 }
  36
  37 uint64_t getElementValueOneHotSATTranslator(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 getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc){
  48         uint i;
  49         for(i=0;i<elemEnc->numVars;i++) {
  50                 if (!This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ]) {
  51                         break;
  52                 }
  53         }
  54
  55         return elemEnc->encodingArray[i];
  56 }
  57
  58 uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
  59         ElementEncoding* elemEnc = getElementEncoding(element);
  60         if(elemEnc->numVars == 0)       //case when the set has only one item
  61                 return getSetElement(getElementSet(element), 0);
  62         switch(elemEnc->type){
  63                 case ONEHOT:
  64                         getElementValueOneHotSATTranslator(This, elemEnc);
  65                         break;
  66                 case UNARY:
  67                         getElementValueUnarySATTranslator(This, elemEnc);
  68                         break;
  69                 case BINARYINDEX:
  70                         return getElementValueBinaryIndexSATTranslator(This, elemEnc);
  71                 case ONEHOTBINARY:
  72                         ASSERT(0);
  73                         break;
  74                 case BINARYVAL:
  75                         ASSERT(0);
  76                         break;
  77                 default:
  78                         ASSERT(0);
  79                         break;
  80         }
  81         return -1;
  82 }
  83
  84 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
  85         int index = getEdgeVar( ((BooleanVar*) boolean)->var );
  86         return This->satEncoder->cnf->solver->solution[index] == true;
  87 }
  88
  89 HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, BooleanOrder* boolOrder){
  90         ASSERT(boolOrder->order->orderPairTable!= NULL);
  91         OrderPair pair={boolOrder->first, boolOrder->second, E_NULL};
  92         Edge var = getOrderConstraint(boolOrder->order->orderPairTable, & pair);
  93         if(edgeIsNull(var))
  94                 return UNORDERED;
  95         int index = getEdgeVar( var );
  96         return This->satEncoder->cnf->solver->solution[index] ? FIRST: SECOND;
  97 }
  98