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