src/Backend/satelemencoder.c

   1 #include "satencoder.h"
   2 #include "structs.h"
   3 #include "common.h"
   4 #include "ops.h"
   5 #include "element.h"
   6
   7 Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) {
   8         generateElementEncodingVariables(This, getElementEncoding(elem));
   9         switch(getElementEncoding(elem)->type){
  10                 case ONEHOT:
  11                         //FIXME
  12                         ASSERT(0);
  13                         break;
  14                 case UNARY:
  15                         ASSERT(0);
  16                         break;
  17                 case BINARYINDEX:
  18                         return getElementValueBinaryIndexConstraint(This, elem, value);
  19                         break;
  20                 case ONEHOTBINARY:
  21                         ASSERT(0);
  22                         break;
  23                 case BINARYVAL:
  24                         ASSERT(0);
  25                         break;
  26                 default:
  27                         ASSERT(0);
  28                         break;
  29         }
  30         return E_BOGUS;
  31 }
  32
  33 Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint64_t value) {
  34         ASTNodeType type = GETELEMENTTYPE(elem);
  35         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
  36         ElementEncoding* elemEnc = getElementEncoding(elem);
  37         for(uint i=0; i<elemEnc->encArraySize; i++){
  38                 if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
  39                         return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
  40                 }
  41         }
  42         return E_BOGUS;
  43 }
  44