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