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                 return;
  53
  54         setFunctionEncodingType(getPredicateFunctionEncoding(This), ENUMERATEIMPLICATIONS);
  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                 return;
  65
  66         setElementEncodingType(encoding, BINARYINDEX);
  67         baseBinaryIndexElementAssign(encoding);
  68
  69         if(GETELEMENTTYPE(This) == ELEMFUNCRETURN) {
  70                 ElementFunction *function=(ElementFunction *) This;
  71                 for(uint i=0; i < getSizeArrayElement(&function->inputs); i++) {
  72                         Element * element=getArrayElement(&function->inputs, i);
  73                         naiveEncodingElement(element);
  74                 }
  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 }