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 "polarityassignment.h"
  15 #include <strings.h>
  16
  17 void naiveEncodingDecision(CSolver* This) {
  18         for (uint i=0; i < getSizeVectorBoolean(This->constraints); i++) {
  19                 Boolean* boolean = getVectorBoolean(This->constraints, i);
  20                 naiveEncodingConstraint(boolean);
  21                 assignPolarityAndBooleanValue(boolean);
  22         }
  23 }
  24
  25 void naiveEncodingConstraint(Boolean * This) {
  26         switch(GETBOOLEANTYPE(This)) {
  27         case BOOLEANVAR: {
  28                 return;
  29         }
  30         case ORDERCONST: {
  31                 setOrderEncodingType( ((BooleanOrder*)This)->order, 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 = getPredicateFunctionEncoding(This);
  55         if (getFunctionEncodingType(encoding) == FUNC_UNASSIGNED)
  56                 setFunctionEncodingType(getPredicateFunctionEncoding(This), 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 }