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