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