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