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