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                         return getElementValueUnaryConstraint(This, elem, value);
  13                 case BINARYINDEX:
  14                         return getElementValueBinaryIndexConstraint(This, elem, value);
  15                 case ONEHOTBINARY:
  16                         ASSERT(0);
  17                         break;
  18                 case BINARYVAL:
  19                         return getElementValueBinaryValueConstraint(This, elem, value);
  20                         break;
  21                 default:
  22                         ASSERT(0);
  23                         break;
  24         }
  25         return E_BOGUS;
  26 }
  27
  28 Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint64_t value) {
  29         ASTNodeType type = GETELEMENTTYPE(elem);
  30         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
  31         ElementEncoding* elemEnc = getElementEncoding(elem);
  32         for(uint i=0; i<elemEnc->encArraySize; i++){
  33                 if(isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
  34                         return (elemEnc->numVars == 0) ? E_True: generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
  35                 }
  36         }
  37         return E_False;
  38 }
  39
  40 Edge getElementValueOneHotConstraint(SATEncoder * This, Element* elem, uint64_t value) {
  41         ASTNodeType type = GETELEMENTTYPE(elem);
  42         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
  43         ElementEncoding* elemEnc = getElementEncoding(elem);
  44         for(uint i=0; i<elemEnc->encArraySize; i++){
  45                 if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
  46                         return elemEnc->variables[i];
  47                 }
  48         }
  49         return E_BOGUS;
  50 }
  51
  52 Edge getElementValueUnaryConstraint(SATEncoder * This, Element* elem, uint64_t value) {
  53         ASTNodeType type = GETELEMENTTYPE(elem);
  54         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
  55         ElementEncoding* elemEnc = getElementEncoding(elem);
  56         for(uint i=0; i<elemEnc->encArraySize; i++){
  57                 if (isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value) {
  58                         if (i==0)
  59                                 return constraintNegate(elemEnc->variables[0]);
  60                         else if ((i+1)==elemEnc->encArraySize)
  61                                 return elemEnc->variables[i-1];
  62                         else
  63                                 return constraintAND2(This->cnf, elemEnc->variables[i-1], constraintNegate(elemEnc->variables[i]));
  64                 }
  65         }
  66         return E_BOGUS;
  67 }
  68
  69 Edge getElementValueBinaryValueConstraint(SATEncoder * This, Element* element, uint64_t value){
  70         ASTNodeType type = GETELEMENTTYPE(element);
  71         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
  72         ElementEncoding* elemEnc = getElementEncoding(element);
  73         if (elemEnc->low <= elemEnc->high) {
  74                 if (value < elemEnc->low || value > elemEnc->high)
  75                         return E_False;
  76         } else {
  77                 //Range wraps around 0
  78                 if (value < elemEnc->low && value > elemEnc->high)
  79                         return E_False;
  80         }
  81
  82         uint64_t valueminusoffset=value-elemEnc->offset;
  83         return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, valueminusoffset);
  84 }
  85
  86 void allocElementConstraintVariables(ElementEncoding* This, uint numVars) {
  87         This->numVars = numVars;
  88         This->variables = ourmalloc(sizeof(Edge) * numVars);
  89 }
  90
  91 void generateBinaryValueEncodingVars(SATEncoder* This, ElementEncoding* encoding){
  92         ASSERT(encoding->type==BINARYVAL);
  93         allocElementConstraintVariables(encoding, encoding->numBits);
  94         getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
  95 }
  96
  97 void generateBinaryIndexEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
  98         ASSERT(encoding->type==BINARYINDEX);
  99         allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize-1));
 100         getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
 101 }
 102
 103 void generateOneHotEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
 104         allocElementConstraintVariables(encoding, encoding->encArraySize);
 105         getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
 106         for(uint i=0;i<encoding->numVars;i++) {
 107                 for(uint j=i+1;j<encoding->numVars;j++) {
 108                         addConstraintCNF(This->cnf, constraintNegate(constraintAND2(This->cnf, encoding->variables[i], encoding->variables[j])));
 109                 }
 110         }
 111         addConstraintCNF(This->cnf, constraintOR(This->cnf, encoding->numVars, encoding->variables));
 112 }
 113
 114 void generateUnaryEncodingVars(SATEncoder *This, ElementEncoding *encoding) {
 115         allocElementConstraintVariables(encoding, encoding->encArraySize-1);
 116         getArrayNewVarsSATEncoder(This, encoding->numVars, encoding->variables);
 117         //Add unary constraint
 118         for(uint i=1;i<encoding->numVars;i++) {
 119                 addConstraintCNF(This->cnf, constraintOR2(This->cnf, encoding->variables[i-1], constraintNegate(encoding->variables[i])));
 120         }
 121 }
 122
 123 void generateElementEncoding(SATEncoder* This, Element * element) {
 124         ElementEncoding* encoding = getElementEncoding(element);
 125         ASSERT(encoding->type!=ELEM_UNASSIGNED);
 126         if(encoding->variables!=NULL)
 127                 return;
 128         switch(encoding->type) {
 129         case ONEHOT:
 130                 generateOneHotEncodingVars(This, encoding);
 131                 return;
 132         case BINARYINDEX:
 133                 generateBinaryIndexEncodingVars(This, encoding);
 134                 return;
 135         case UNARY:
 136                 generateUnaryEncodingVars(This, encoding);
 137                 return;
 138         case ONEHOTBINARY:
 139                 return;
 140         case BINARYVAL:
 141                 generateBinaryValueEncodingVars(This, encoding);
 142                 return;
 143         default:
 144                 ASSERT(0);
 145         }
 146 }
 147