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