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