src/Backend/satencoder.cc

   1 #include "satencoder.h"
   2 #include "structs.h"
   3 #include "csolver.h"
   4 #include "boolean.h"
   5 #include "constraint.h"
   6 #include "common.h"
   7 #include "element.h"
   8 #include "function.h"
   9 #include "tableentry.h"
  10 #include "table.h"
  11 #include "order.h"
  12 #include "predicate.h"
  13 #include "set.h"
  14 #include "satfuncopencoder.h"
  15
  16 //TODO: Should handle sharing of AST Nodes without recoding them a second time
  17
  18 SATEncoder::SATEncoder(CSolver * _solver) :
  19         varcount(1),
  20         cnf(createCNF()),
  21         solver(_solver) {
  22 }
  23
  24 SATEncoder::~SATEncoder() {
  25         deleteCNF(cnf);
  26 }
  27
  28 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
  29         HSIteratorBoolean *iterator = csolver->getConstraints();
  30         while (iterator->hasNext()) {
  31                 Boolean *constraint = iterator->next();
  32                 model_print("Encoding All ...\n\n");
  33                 Edge c = encodeConstraintSATEncoder(constraint);
  34                 model_print("Returned Constraint in EncodingAll:\n");
  35                 ASSERT( !equalsEdge(c, E_BOGUS));
  36                 addConstraintCNF(cnf, c);
  37         }
  38         delete iterator;
  39 }
  40
  41 Edge SATEncoder::encodeConstraintSATEncoder(Boolean *constraint) {
  42         switch (GETBOOLEANTYPE(constraint)) {
  43         case ORDERCONST:
  44                 return encodeOrderSATEncoder(this, (BooleanOrder *) constraint);
  45         case BOOLEANVAR:
  46                 return encodeVarSATEncoder(this, (BooleanVar *) constraint);
  47         case LOGICOP:
  48                 return encodeLogicSATEncoder(this, (BooleanLogic *) constraint);
  49         case PREDICATEOP:
  50                 return encodePredicateSATEncoder(this, (BooleanPredicate *) constraint);
  51         default:
  52                 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
  53                 exit(-1);
  54         }
  55 }
  56
  57 void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray) {
  58         for (uint i = 0; i < num; i++)
  59                 carray[i] = getNewVarSATEncoder(encoder);
  60 }
  61
  62 Edge getNewVarSATEncoder(SATEncoder *This) {
  63         return constraintNewVar(This->cnf);
  64 }
  65
  66 Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) {
  67         if (edgeIsNull(constraint->var)) {
  68                 constraint->var = getNewVarSATEncoder(This);
  69         }
  70         return constraint->var;
  71 }
  72
  73 Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) {
  74         Edge array[constraint->inputs.getSize()];
  75         for (uint i = 0; i < constraint->inputs.getSize(); i++)
  76                 array[i] = This->encodeConstraintSATEncoder(constraint->inputs.get(i));
  77
  78         switch (constraint->op) {
  79         case L_AND:
  80                 return constraintAND(This->cnf, constraint->inputs.getSize(), array);
  81         case L_OR:
  82                 return constraintOR(This->cnf, constraint->inputs.getSize(), array);
  83         case L_NOT:
  84                 return constraintNegate(array[0]);
  85         case L_XOR:
  86                 return constraintXOR(This->cnf, array[0], array[1]);
  87         case L_IMPLIES:
  88                 return constraintIMPLIES(This->cnf, array[0], array[1]);
  89         default:
  90                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
  91                 exit(-1);
  92         }
  93 }
  94
  95 Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
  96         switch (GETPREDICATETYPE(constraint->predicate) ) {
  97         case TABLEPRED:
  98                 return encodeTablePredicateSATEncoder(This, constraint);
  99         case OPERATORPRED:
 100                 return encodeOperatorPredicateSATEncoder(This, constraint);
 101         default:
 102                 ASSERT(0);
 103         }
 104         return E_BOGUS;
 105 }
 106
 107 Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
 108         switch (constraint->encoding.type) {
 109         case ENUMERATEIMPLICATIONS:
 110         case ENUMERATEIMPLICATIONSNEGATE:
 111                 return encodeEnumTablePredicateSATEncoder(This, constraint);
 112         case CIRCUIT:
 113                 ASSERT(0);
 114                 break;
 115         default:
 116                 ASSERT(0);
 117         }
 118         return E_BOGUS;
 119 }
 120
 121 void encodeElementSATEncoder(SATEncoder *encoder, Element *This) {
 122         switch ( GETELEMENTTYPE(This) ) {
 123         case ELEMFUNCRETURN:
 124                 generateElementEncoding(encoder, This);
 125                 encodeElementFunctionSATEncoder(encoder, (ElementFunction *) This);
 126                 break;
 127         case ELEMSET:
 128                 generateElementEncoding(encoder, This);
 129                 return;
 130         case ELEMCONST:
 131                 return;
 132         default:
 133                 ASSERT(0);
 134         }
 135 }
 136
 137 void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
 138         switch (GETFUNCTIONTYPE(This->function)) {
 139         case TABLEFUNC:
 140                 encodeTableElementFunctionSATEncoder(encoder, This);
 141                 break;
 142         case OPERATORFUNC:
 143                 encodeOperatorElementFunctionSATEncoder(encoder, This);
 144                 break;
 145         default:
 146                 ASSERT(0);
 147         }
 148 }
 149
 150 void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
 151         switch (getElementFunctionEncoding(This)->type) {
 152         case ENUMERATEIMPLICATIONS:
 153                 encodeEnumTableElemFunctionSATEncoder(encoder, This);
 154                 break;
 155         case CIRCUIT:
 156                 ASSERT(0);
 157                 break;
 158         default:
 159                 ASSERT(0);
 160         }
 161 }