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