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