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