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