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 (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
  14                         index |= 1;
  15         }
  16         model_print("index:%u\tencArraySize:%u\tisInUseElement:%u\n", index, elemEnc->encArraySize, isinUseElement(elemEnc, index));
  17         ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
  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->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
  26                         value |= 1;
  27         }
  28         if (elemEnc->isBinaryValSigned &&
  29                         This->satEncoder->cnf->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->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
  42                         index = i;
  43         }
  44         ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, 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->satEncoder->cnf->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 getSetElement(getElementSet(element), 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->satEncoder->cnf->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 UNORDERED;
  94         return getValueCNF(This->satEncoder->cnf, var)? FIRST: SECOND;
  95 }
  96