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         }
  34         case PREDICATEOP: {
  35                 naiveEncodingPredicate((BooleanPredicate *) This);
  36                 return;
  37         }
  38         default:
  39                 ASSERT(0);
  40         }
  41 }
  42
  43 void naiveEncodingLogicOp(BooleanLogic * This) {
  44         for(uint i=0; i < getSizeArrayBoolean(&This->inputs); i++) {
  45                 naiveEncodingConstraint(getArrayBoolean(&This->inputs, i));
  46         }
  47 }
  48
  49 void naiveEncodingPredicate(BooleanPredicate * This) {
  50         FunctionEncoding *encoding = getPredicateFunctionEncoding(This);
  51         if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
  52                 setFunctionEncodingType(getPredicateFunctionEncoding(This), ENUMERATEIMPLICATIONS);
  53
  54         for(uint i=0; i < getSizeArrayElement(&This->inputs); i++) {
  55                 Element *element=getArrayElement(&This->inputs, i);
  56                 naiveEncodingElement(element);
  57         }
  58 }
  59
  60 void naiveEncodingElement(Element * This) {
  61         ElementEncoding * encoding = getElementEncoding(This);
  62         if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
  63                 setElementEncodingType(encoding, BINARYINDEX);
  64                 baseBinaryIndexElementAssign(encoding);
  65         }
  66
  67         if(GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
  68                 ElementFunction *function=(ElementFunction *) This;
  69                 for(uint i=0; i < getSizeArrayElement(&function->inputs); i++) {
  70                         Element * element=getArrayElement(&function->inputs, i);
  71                         naiveEncodingElement(element);
  72                 }
  73                 FunctionEncoding *encoding = getElementFunctionEncoding(function);
  74                 if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
  75                         setFunctionEncodingType(getElementFunctionEncoding(function), ENUMERATEIMPLICATIONS);
  76         }
  77 }
  78
  79 void baseBinaryIndexElementAssign(ElementEncoding *This) {
  80         Element * element=This->element;
  81         Set * set= getElementSet(element);
  82         ASSERT(set->isRange==false);
  83         uint size=getSizeVectorInt(set->members);
  84         uint encSize=NEXTPOW2(size);
  85         allocEncodingArrayElement(This, encSize);
  86         allocInUseArrayElement(This, encSize);
  87         for(uint i=0;i<size;i++) {
  88                 This->encodingArray[i]=getVectorInt(set->members, i);
  89                 setInUseElement(This, i);
  90         }
  91 }