src/Translator/sattranslator.cc

   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 (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )))
  14                         index |= 1;
  15         }
  16         if (elemEnc->encArraySize <= index || !elemEnc->isinUseElement(index))
  17                 model_print("WARNING: Element has undefined value!\n");
  18         return elemEnc->encodingArray[index];
  19 }
  20
  21 uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
  22         uint64_t value = 0;
  23         for (int i = elemEnc->numVars - 1; i >= 0; i--) {
  24                 value = value << 1;
  25                 if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) )
  26                         value |= 1;
  27         }
  28         if (elemEnc->isBinaryValSigned &&
  29                         This->getSATEncoder()->getCNF()->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
  30                 //Do sign extension of negative number
  31                 uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
  32                 value += highbits;
  33         }
  34         value += elemEnc->offset;
  35         return value;
  36 }
  37
  38 uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
  39         uint index = 0;
  40         bool overflow = true;
  41         for (uint i = 0; i < elemEnc->numVars; i++) {
  42                 if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] ))){
  43                         index = i;
  44                         overflow = false;
  45                 }
  46         }
  47         if(overflow)
  48                 model_print("WARNING: Element has undefined value!\n");
  49         ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
  50         return elemEnc->encodingArray[index];
  51 }
  52
  53 uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
  54         uint i;
  55         for (i = 0; i < elemEnc->numVars; i++) {
  56                 if (!getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) ) {
  57                         break;
  58                 }
  59         }
  60
  61         return elemEnc->encodingArray[i];
  62 }
  63
  64 uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
  65         ElementEncoding *elemEnc = element->getElementEncoding();
  66         if (elemEnc->numVars == 0)//case when the set has only one item
  67                 return element->getRange()->getElement(0);
  68         switch (elemEnc->type) {
  69         case ONEHOT:
  70                 return getElementValueOneHotSATTranslator(This, elemEnc);
  71         case UNARY:
  72                 return getElementValueUnarySATTranslator(This, elemEnc);
  73         case BINARYINDEX:
  74                 return getElementValueBinaryIndexSATTranslator(This, elemEnc);
  75                 break;
  76         case BINARYVAL:
  77                 ASSERT(0);
  78                 break;
  79         default:
  80                 ASSERT(0);
  81                 break;
  82         }
  83         return -1;
  84 }
  85
  86 bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
  87         if (boolean->boolVal == BV_MUSTBETRUE)
  88                 return true;
  89         else if (boolean->boolVal == BV_MUSTBEFALSE)
  90                 return false;
  91         else {
  92                 int index = getEdgeVar( ((BooleanVar *) boolean)->var );
  93                 return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);
  94         }
  95 }
  96
  97