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         SetIteratorBoolean *iterator = This->getConstraints();
  18         while (iterator->hasNext()) {
  19                 Boolean *boolean = iterator->next();
  20                 naiveEncodingConstraint(boolean);
  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                 ((BooleanOrder *) This)->order->setOrderEncodingType(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 < This->inputs.getSize(); i++) {
  49                 naiveEncodingConstraint(This->inputs.get(i));
  50         }
  51 }
  52
  53 void naiveEncodingPredicate(BooleanPredicate *This) {
  54         FunctionEncoding *encoding = This->getFunctionEncoding();
  55         if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
  56                 This->getFunctionEncoding()->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
  57
  58         for (uint i = 0; i < This->inputs.getSize(); i++) {
  59                 Element *element = This->inputs.get(i);
  60                 naiveEncodingElement(element);
  61         }
  62 }
  63
  64 void naiveEncodingElement(Element *This) {
  65         ElementEncoding *encoding = getElementEncoding(This);
  66         if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
  67                 encoding->setElementEncodingType(BINARYINDEX);
  68                 encoding->encodingArrayInitialization();
  69         }
  70
  71         if (This->type == ELEMFUNCRETURN) {
  72                 ElementFunction *function = (ElementFunction *) This;
  73                 for (uint i = 0; i < function->inputs.getSize(); i++) {
  74                         Element *element = function->inputs.get(i);
  75                         naiveEncodingElement(element);
  76                 }
  77                 FunctionEncoding *encoding = getElementFunctionEncoding(function);
  78                 if (encoding->getFunctionEncodingType() == FUNC_UNASSIGNED)
  79                         getElementFunctionEncoding(function)->setFunctionEncodingType(ENUMERATEIMPLICATIONS);
  80         }
  81 }
  82