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