src/Encoders/naiveencoder.c

   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         for (uint i=0; i < getSizeVectorBoolean(This->constraints); i++) {
  18                 naiveEncodingConstraint(getVectorBoolean(This->constraints, i));
  19         }
  20 }
  21
  22 void naiveEncodingConstraint(Boolean * This) {
  23         switch(GETBOOLEANTYPE(This)) {
  24         case BOOLEANVAR: {
  25                 return;
  26         }
  27         case ORDERCONST: {
  28                 setOrderEncodingType( ((BooleanOrder*)This)->order, PAIRWISE );
  29                 return;
  30         }
  31         case LOGICOP: {
  32                 naiveEncodingLogicOp((BooleanLogic *) This);
  33                 return;
  34         }
  35         case PREDICATEOP: {
  36                 naiveEncodingPredicate((BooleanPredicate *) This);
  37                 return;
  38         }
  39         default:
  40                 ASSERT(0);
  41         }
  42 }
  43
  44 void naiveEncodingLogicOp(BooleanLogic * This) {
  45         for(uint i=0; i < getSizeArrayBoolean(&This->inputs); i++) {
  46                 naiveEncodingConstraint(getArrayBoolean(&This->inputs, i));
  47         }
  48 }
  49
  50 void naiveEncodingPredicate(BooleanPredicate * This) {
  51         FunctionEncoding *encoding = getPredicateFunctionEncoding(This);
  52         if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
  53                 setFunctionEncodingType(getPredicateFunctionEncoding(This), ENUMERATEIMPLICATIONS);
  54
  55         for(uint i=0; i < getSizeArrayElement(&This->inputs); i++) {
  56                 Element *element=getArrayElement(&This->inputs, i);
  57                 naiveEncodingElement(element);
  58         }
  59 }
  60
  61 void naiveEncodingElement(Element * This) {
  62         ElementEncoding * encoding = getElementEncoding(This);
  63         if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
  64                 setElementEncodingType(encoding, BINARYINDEX);
  65                 encodingArrayInitialization(encoding);
  66         }
  67
  68         if(GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
  69                 ElementFunction *function=(ElementFunction *) This;
  70                 for(uint i=0; i < getSizeArrayElement(&function->inputs); i++) {
  71                         Element * element=getArrayElement(&function->inputs, i);
  72                         naiveEncodingElement(element);
  73                 }
  74                 FunctionEncoding *encoding = getElementFunctionEncoding(function);
  75                 if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
  76                         setFunctionEncodingType(getElementFunctionEncoding(function), ENUMERATEIMPLICATIONS);
  77         }
  78 }
  79
  80 uint getSizeEncodingArray(ElementEncoding *This, uint setSize){
  81         switch(This->type){
  82                 case BINARYINDEX:
  83                         return NEXTPOW2(setSize);
  84                 case ONEHOT:
  85                 case UNARY:
  86                         return setSize;
  87                 default:
  88                         ASSERT(0);
  89         }
  90         return -1;
  91 }
  92
  93 void encodingArrayInitialization(ElementEncoding *This) {
  94         Element * element=This->element;
  95         Set * set= getElementSet(element);
  96         ASSERT(set->isRange==false);
  97         uint size=getSizeVectorInt(set->members);
  98         uint encSize=getSizeEncodingArray(This, size);
  99         allocEncodingArrayElement(This, encSize);
 100         allocInUseArrayElement(This, encSize);
 101         for(uint i=0;i<size;i++) {
 102                 This->encodingArray[i]=getVectorInt(set->members, i);
 103                 setInUseElement(This, i);
 104         }
 105 }