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