src/Encoders/naiveencoder.cc

   1 #include "naiveencoder.h"
   2 #include "elementencoding.h"
   3 #include "element.h"
   4 #include "functionencoding.h"
   5 #include "function.h"
   6 #include "set.h"
   7 #include "common.h"
   8 #include "structs.h"
   9 #include "csolver.h"
  10 #include "boolean.h"
  11 #include "table.h"
  12 #include "tableentry.h"
  13 #include "order.h"
  14 #include <strings.h>
  15
  16 void naiveEncodingDecision(CSolver *This) {
  17         HSIteratorBoolean *iterator=iteratorBoolean(This->constraints);
  18         while(hasNextBoolean(iterator)) {
  19                 Boolean *boolean = nextBoolean(iterator);
  20                 naiveEncodingConstraint(boolean);
  21         }
  22         deleteIterBoolean(iterator);
  23 }
  24
  25 void naiveEncodingConstraint(Boolean *This) {
  26         switch (GETBOOLEANTYPE(This)) {
  27         case BOOLEANVAR: {
  28                 return;
  29         }
  30         case ORDERCONST: {
  31                 ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
  32                 return;
  33         }
  34         case LOGICOP: {
  35                 naiveEncodingLogicOp((BooleanLogic *) This);
  36                 return;
  37         }
  38         case PREDICATEOP: {
  39                 naiveEncodingPredicate((BooleanPredicate *) This);
  40                 return;
  41         }
  42         default:
  43                 ASSERT(0);
  44         }
  45 }
  46
  47 void naiveEncodingLogicOp(BooleanLogic *This) {
  48         for (uint i = 0; i < getSizeArrayBoolean(&This->inputs); i++) {
  49                 naiveEncodingConstraint(getArrayBoolean(&This->inputs, i));
  50         }
  51 }
  52
  53 void naiveEncodingPredicate(BooleanPredicate *This) {
  54         FunctionEncoding *encoding = This->getFunctionEncoding();
  55         if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
  56                 setFunctionEncodingType(This->getFunctionEncoding(), ENUMERATEIMPLICATIONS);
  57
  58         for (uint i = 0; i < getSizeArrayElement(&This->inputs); i++) {
  59                 Element *element = getArrayElement(&This->inputs, i);
  60                 naiveEncodingElement(element);
  61         }
  62 }
  63
  64 void naiveEncodingElement(Element *This) {
  65         ElementEncoding *encoding = getElementEncoding(This);
  66         if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
  67                 setElementEncodingType(encoding, BINARYINDEX);
  68                 encodingArrayInitialization(encoding);
  69         }
  70
  71         if (GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
  72                 ElementFunction *function = (ElementFunction *) This;
  73                 for (uint i = 0; i < getSizeArrayElement(&function->inputs); i++) {
  74                         Element *element = getArrayElement(&function->inputs, i);
  75                         naiveEncodingElement(element);
  76                 }
  77                 FunctionEncoding *encoding = getElementFunctionEncoding(function);
  78                 if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
  79                         setFunctionEncodingType(getElementFunctionEncoding(function), ENUMERATEIMPLICATIONS);
  80         }
  81 }
  82
  83 uint getSizeEncodingArray(ElementEncoding *This, uint setSize) {
  84         switch (This->type) {
  85         case BINARYINDEX:
  86                 return NEXTPOW2(setSize);
  87         case ONEHOT:
  88         case UNARY:
  89                 return setSize;
  90         default:
  91                 ASSERT(0);
  92         }
  93         return -1;
  94 }
  95
  96 void encodingArrayInitialization(ElementEncoding *This) {
  97         Element *element = This->element;
  98         Set *set = getElementSet(element);
  99         ASSERT(set->isRange == false);
 100         uint size = getSizeVectorInt(set->members);
 101         uint encSize = getSizeEncodingArray(This, size);
 102         allocEncodingArrayElement(This, encSize);
 103         allocInUseArrayElement(This, encSize);
 104         for (uint i = 0; i < size; i++) {
 105                 This->encodingArray[i] = getVectorInt(set->members, i);
 106                 setInUseElement(This, i);
 107         }
 108 }