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         switch(getElementEncoding(elem)->type){
   9                 case ONEHOT:
  10                         return getElementValueOneHotConstraint(This, elem, value);
  11                 case UNARY:
  12                         ASSERT(0);
  13                         break;
  14                 case BINARYINDEX:
  15                         return getElementValueBinaryIndexConstraint(This, elem, value);
  16                 case ONEHOTBINARY:
  17                         ASSERT(0);
  18                         break;
  19                 case BINARYVAL:
  20                         ASSERT(0);
  21                         break;
  22                 default:
  23                         ASSERT(0);
  24                         break;
  25         }
  26         return E_BOGUS;
  27 }
  28
  29 Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint64_t value) {
  30         ASTNodeType type = GETELEMENTTYPE(elem);
  31         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
  32         ElementEncoding* elemEnc = getElementEncoding(elem);
  33         for(uint i=0; i<elemEnc->encArraySize; i++){
  34                 if(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
  35                         return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
  36                 }
  37         }
  38         return E_BOGUS;
  39 }
  40
  41 Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t value) {
  42         ASTNodeType type = GETELEMENTTYPE(elem);
  43         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
  44         ElementEncoding* elemEnc = getElementEncoding(elem);
  45         for(uint i=0; i<elemEnc->encArraySize; i++){
  46                 if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
  47                         return elemEnc->variables[i];
  48                 }
  49         }
  50         return E_BOGUS;
  51 }
  52
  53 void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
  54         This->numVars = numVars;
  55         This->variables = ourmalloc(sizeof(Edge) * numVars);
  56 }
  57
  58 void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
  59         ASSERT(encoding->type==BINARYINDEX);
  60         allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize-1));
  61         getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
  62 }
  63
  64 void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
  65         allocElementConstraintVariables(encoding, encoding->encArraySize);
  66         getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
  67         for(uint i=0;i<encoding->numVars;i++) {
  68                 for(uint j=0;j<encoding->numVars;j++) {
  69                         addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, encoding->variables[i], constraintNegate(encoding->variables[j])));
  70                 }
  71         }
  72 }
  73
  74 void generateElementEncoding(SATEncoder* This, Element * element) {
  75         ElementEncoding* encoding = getElementEncoding(element);
  76         ASSERT(encoding->type!=ELEM_UNASSIGNED);
  77         if(encoding->variables!=NULL)
  78                 return;
  79         switch(encoding->type) {
  80         case ONEHOT:
  81                 generateOneHotEncodingVars(This, encoding);
  82                 return;
  83         case BINARYINDEX:
  84                 generateBinaryIndexEncodingVars(This, encoding);
  85                 return;
  86         default:
  87                 ASSERT(0);
  88         }
  89 }
  90