src/Encoders/naiveencoder.cc

   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 "tunable.h"
  15 #include <strings.h>
  16
  17 void naiveEncodingDecision(CSolver *This) {
  18         SetIteratorBooleanEdge *iterator = This->getConstraints();
  19         while (iterator->hasNext()) {
  20                 BooleanEdge b = iterator->next();
  21                 naiveEncodingConstraint(This, b.getBoolean());
  22         }
  23         delete iterator;
  24 }
  25
  26 void naiveEncodingConstraint(CSolver *csolver, Boolean *This) {
  27         switch (This->type) {
  28         case BOOLEANVAR: {
  29                 return;
  30         }
  31         case ORDERCONST: {
  32                 if (((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
  33                         ((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
  34                 return;
  35         }
  36         case LOGICOP: {
  37                 naiveEncodingLogicOp(csolver, (BooleanLogic *) This);
  38                 return;
  39         }
  40         case PREDICATEOP: {
  41                 naiveEncodingPredicate(csolver, (BooleanPredicate *) This);
  42                 return;
  43         }
  44         default:
  45                 ASSERT(0);
  46         }
  47 }
  48
  49 void naiveEncodingLogicOp(CSolver *csolver, BooleanLogic *This) {
  50         for (uint i = 0; i < This->inputs.getSize(); i++) {
  51                 naiveEncodingConstraint(csolver, This->inputs.get(i).getBoolean());
  52         }
  53 }
  54
  55 void naiveEncodingPredicate(CSolver *csolver, BooleanPredicate *This) {
  56         FunctionEncoding *encoding = This->getFunctionEncoding();
  57         if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
  58                 This->getFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
  59
  60         for (uint i = 0; i < This->inputs.getSize(); i++) {
  61                 Element *element = This->inputs.get(i);
  62                 naiveEncodingElement(csolver, element);
  63         }
  64 }
  65
  66 void naiveEncodingElement(CSolver *csolver, Element *This) {
  67         ElementEncoding *encoding = This->getElementEncoding();
  68         if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
  69                 if (This->type != ELEMCONST) {
  70                         model_print("INFO: naive encoder is making the decision about element %p....\n", This);
  71                 }
  72                 uint enc = csolver->getTuner()->getVarTunable(This->getRange()->getType(), NODEENCODING, &NodeEncodingDesc);
  73                 if (enc == ELEM_UNASSIGNED)
  74                         enc = csolver->getTuner()->getTunable(NAIVEENCODER, &NaiveEncodingDesc);
  75                 encoding->setElementEncodingType((ElementEncodingType)enc);
  76                 encoding->encodingArrayInitialization();
  77         }
  78
  79         if (This->type == ELEMFUNCRETURN) {
  80                 ElementFunction *function = (ElementFunction *) This;
  81                 for (uint i = 0; i < function->inputs.getSize(); i++) {
  82                         Element *element = function->inputs.get(i);
  83                         naiveEncodingElement(csolver, element);
  84                 }
  85                 FunctionEncoding *encoding = function->getElementFunctionEncoding();
  86                 if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
  87                         function->getElementFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
  88         }
  89 }
  90