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