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         case BOOLCONST:
  68                 result = ((BooleanConst *) constraint)->isTrue() ? E_True : E_False;
  69                 break;
  70         default:
  71                 model_print("Unhandled case in encodeConstraintSATEncoder %u", constraint->type);
  72                 exit(-1);
  73         }
  74         Polarity p = constraint->polarity;
  75         uint pSize = constraint->parents.getSize();
  76         if ((pSize > 1 && p != P_BOTHTRUEFALSE ) || pSize > 2) {
  77                 Edge e = getNewVarSATEncoder();
  78                 generateProxy(cnf, result, e, p);
  79                 booledgeMap.put(constraint, e.node_ptr);
  80                 result = e;
  81         }
  82
  83         return c.isNegated() ? constraintNegate(result) : result;
  84 }
  85
  86 void SATEncoder::getArrayNewVarsSATEncoder(uint num, Edge *carray) {
  87         for (uint i = 0; i < num; i++)
  88                 carray[i] = getNewVarSATEncoder();
  89 }
  90
  91 Edge SATEncoder::getNewVarSATEncoder() {
  92         return constraintNewVar(cnf);
  93 }
  94
  95 Edge SATEncoder::encodeVarSATEncoder(BooleanVar *constraint) {
  96         if (edgeIsNull(constraint->var)) {
  97                 constraint->var = getNewVarSATEncoder();
  98         }
  99         return constraint->var;
 100 }
 101
 102 Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
 103         Edge array[constraint->inputs.getSize()];
 104         for (uint i = 0; i < constraint->inputs.getSize(); i++)
 105                 array[i] = encodeConstraintSATEncoder(constraint->inputs.get(i));
 106
 107         switch (constraint->op) {
 108         case SATC_AND:
 109                 return constraintAND(cnf, constraint->inputs.getSize(), array);
 110         case SATC_NOT:
 111                 return constraintNegate(array[0]);
 112         case SATC_IFF:
 113                 ASSERT(constraint->inputs.getSize() == 2);
 114                 return constraintIFF(cnf, array[0], array[1]);
 115         case SATC_OR:
 116         case SATC_XOR:
 117         case SATC_IMPLIES:
 118         //Don't handle, translate these away...
 119         default:
 120                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
 121                 exit(-1);
 122         }
 123 }
 124
 125 Edge SATEncoder::encodePredicateSATEncoder(BooleanPredicate *constraint) {
 126         switch (constraint->predicate->type) {
 127         case TABLEPRED:
 128                 return encodeTablePredicateSATEncoder(constraint);
 129         case OPERATORPRED:
 130                 return encodeOperatorPredicateSATEncoder(constraint);
 131         default:
 132                 ASSERT(0);
 133         }
 134         return E_BOGUS;
 135 }
 136
 137 Edge SATEncoder::encodeTablePredicateSATEncoder(BooleanPredicate *constraint) {
 138         switch (constraint->encoding.type) {
 139         case ENUMERATEIMPLICATIONS:
 140         case ENUMERATEIMPLICATIONSNEGATE:
 141                 return encodeEnumTablePredicateSATEncoder(constraint);
 142         case CIRCUIT:
 143                 ASSERT(0);
 144                 break;
 145         default:
 146                 ASSERT(0);
 147         }
 148         return E_BOGUS;
 149 }
 150
 151 void SATEncoder::encodeElementSATEncoder(Element *element) {
 152         /* Check to see if we have already encoded this element. */
 153         if (element->getElementEncoding()->variables != NULL)
 154                 return;
 155
 156         /* Need to encode. */
 157         switch ( element->type) {
 158         case ELEMFUNCRETURN:
 159                 generateElementEncoding(element);
 160                 encodeElementFunctionSATEncoder((ElementFunction *) element);
 161                 break;
 162         case ELEMSET:
 163                 generateElementEncoding(element);
 164                 return;
 165         case ELEMCONST:
 166                 return;
 167         default:
 168                 ASSERT(0);
 169         }
 170 }
 171
 172 void SATEncoder::encodeElementFunctionSATEncoder(ElementFunction *function) {
 173         switch (function->getFunction()->type) {
 174         case TABLEFUNC:
 175                 encodeTableElementFunctionSATEncoder(function);
 176                 break;
 177         case OPERATORFUNC:
 178                 encodeOperatorElementFunctionSATEncoder(function);
 179                 break;
 180         default:
 181                 ASSERT(0);
 182         }
 183 }
 184
 185 void SATEncoder::encodeTableElementFunctionSATEncoder(ElementFunction *function) {
 186         switch (function->getElementFunctionEncoding()->type) {
 187         case ENUMERATEIMPLICATIONS:
 188                 encodeEnumTableElemFunctionSATEncoder(function);
 189                 break;
 190         case CIRCUIT:
 191                 ASSERT(0);
 192                 break;
 193         default:
 194                 ASSERT(0);
 195         }
 196 }