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