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
  17 void naiveEncodingDecision(CSolver* csolver, SATEncoder* encoder){
  18         uint size = getSizeVectorElement(csolver->allElements);
  19         for(uint i=0; i<size; i++){
  20                 Element* element = getVectorElement(csolver->allElements, i);
  21                 switch(GETELEMENTTYPE(element)){
  22                         case ELEMSET:
  23                                 setElementEncodingType(getElementEncoding(element), BINARYINDEX);
  24                                 //FIXME:Should be moved to SATEncoder
  25                                 baseBinaryIndexElementAssign(getElementEncoding(element));
  26                                 generateElementEncodingVariables(encoder,getElementEncoding(element));
  27                                 //
  28                                 break;
  29                         case ELEMFUNCRETURN:
  30                                 setFunctionEncodingType(getElementFunctionEncoding((ElementFunction*)element),
  31                                         ENUMERATEIMPLICATIONS);
  32                                 break;
  33                         default:
  34                                 ASSERT(0);
  35                 }
  36         }
  37
  38         size = getSizeVectorBoolean(csolver->allBooleans);
  39         for(uint i=0; i<size; i++){
  40                 Boolean* boolean = getVectorBoolean(csolver->allBooleans, i);
  41                 switch(GETBOOLEANTYPE(boolean)){
  42                         case PREDICATEOP:
  43                                 setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)boolean),
  44                                         ENUMERATEIMPLICATIONS);
  45                                 break;
  46                         case ORDERCONST:
  47                                 setOrderEncodingType( ((BooleanOrder*)boolean)->order, PAIRWISE );
  48                                 break;
  49                         default:
  50                                 continue;
  51                 }
  52         }
  53 }
  54
  55 void baseBinaryIndexElementAssign(ElementEncoding *This) {
  56         Element * element=This->element;
  57         ASSERT(element->type == ELEMSET);
  58         Set * set= ((ElementSet*)element)->set;
  59         ASSERT(set->isRange==false);
  60         uint size=getSizeVectorInt(set->members);
  61         uint encSize=NEXTPOW2(size);
  62         allocEncodingArrayElement(This, encSize);
  63         allocInUseArrayElement(This, encSize);
  64
  65         for(uint i=0;i<size;i++) {
  66                 This->encodingArray[i]=getVectorInt(set->members, i);
  67                 setInUseElement(This, i);
  68         }
  69         This->numVars = NUMBITS(size-1);
  70         This->variables = ourmalloc(sizeof(Constraint*)* This->numVars);
  71
  72
  73 }
  74
  75