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         for (uint i = 0; i < elemEnc->numVars; i++) {
  41                 if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )))
  42                         index = i;
  43         }
  44         ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
  45         return elemEnc->encodingArray[index];
  46 }
  47
  48 uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
  49         uint i;
  50         for (i = 0; i < elemEnc->numVars; i++) {
  51                 if (!getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] )) ) {
  52                         break;
  53                 }
  54         }
  55
  56         return elemEnc->encodingArray[i];
  57 }
  58
  59 uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
  60         ElementEncoding *elemEnc = getElementEncoding(element);
  61         if (elemEnc->numVars == 0)//case when the set has only one item
  62                 return getElementSet(element)->getElement(0);
  63         switch (elemEnc->type) {
  64         case ONEHOT:
  65                 return getElementValueOneHotSATTranslator(This, elemEnc);
  66         case UNARY:
  67                 return getElementValueUnarySATTranslator(This, elemEnc);
  68         case BINARYINDEX:
  69                 return getElementValueBinaryIndexSATTranslator(This, elemEnc);
  70         case ONEHOTBINARY:
  71                 ASSERT(0);
  72                 break;
  73         case BINARYVAL:
  74                 ASSERT(0);
  75                 break;
  76         default:
  77                 ASSERT(0);
  78                 break;
  79         }
  80         return -1;
  81 }
  82
  83 bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
  84         int index = getEdgeVar( ((BooleanVar *) boolean)->var );
  85         return getValueSolver(This->getSATEncoder()->getCNF()->solver, index);
  86 }
  87
  88 HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second) {
  89         ASSERT(order->orderPairTable != NULL);
  90         OrderPair pair(first, second, E_NULL);
  91         Edge var = getOrderConstraint(order->orderPairTable, &pair);
  92         if (edgeIsNull(var))
  93                 return SATC_UNORDERED;
  94         return getValueCNF(This->getSATEncoder()->getCNF(), var) ? SATC_FIRST : SATC_SECOND;
  95 }
  96