src/Backend/satelemencoder.cc

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