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