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(uint 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         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(uint i=elemEnc->numVars-1;i>=0;i--) {
  23                 value=value<<1;
  24                 if (getValueSolver(This->satEncoder->cnf->solver, 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(uint i=0; i< elemEnc->numVars; i++) {
  40                 if (getValueSolver(This->satEncoder->cnf->solver, 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 (! getValueSolver(This->satEncoder->cnf->solver, 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                         return getElementValueOneHotSATTranslator(This, elemEnc);
  65                 case UNARY:
  66                         return getElementValueUnarySATTranslator(This, elemEnc);
  67                 case BINARYINDEX:
  68                         return getElementValueBinaryIndexSATTranslator(This, elemEnc);
  69                 case ONEHOTBINARY:
  70                         ASSERT(0);
  71                         break;
  72                 case BINARYVAL:
  73                         ASSERT(0);
  74                         break;
  75                 default:
  76                         ASSERT(0);
  77                         break;
  78         }
  79         return -1;
  80 }
  81
  82 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
  83         int index = getEdgeVar( ((BooleanVar*) boolean)->var );
  84         return getValueSolver(This->satEncoder->cnf->solver, index);
  85 }
  86
  87 HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second){
  88         ASSERT(order->orderPairTable!= NULL);
  89         OrderPair pair={first, second, E_NULL};
  90         Edge var = getOrderConstraint(order->orderPairTable, &pair);
  91         if(edgeIsNull(var))
  92                 return UNORDERED;
  93         return getValueCNF(This->satEncoder->cnf, var)? FIRST: SECOND;
  94 }
  95