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