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 "satfuncopencoder.h"
  15
  16 //TODO: Should handle sharing of AST Nodes without recoding them a second time
  17
  18 SATEncoder *allocSATEncoder(CSolver *solver) {
  19         SATEncoder *This = (SATEncoder *)ourmalloc(sizeof (SATEncoder));
  20         This->solver = solver;
  21         This->varcount = 1;
  22         This->cnf = createCNF();
  23         return This;
  24 }
  25
  26 void deleteSATEncoder(SATEncoder *This) {
  27         deleteCNF(This->cnf);
  28         ourfree(This);
  29 }
  30
  31 void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) {
  32         HSIteratorBoolean *iterator=csolver->constraints.iterator();
  33         while(iterator->hasNext()) {
  34                 Boolean *constraint = iterator->next();
  35                 model_print("Encoding All ...\n\n");
  36                 Edge c = encodeConstraintSATEncoder(This, constraint);
  37                 model_print("Returned Constraint in EncodingAll:\n");
  38                 addConstraintCNF(This->cnf, c);
  39         }
  40         delete iterator;
  41 }
  42
  43 Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
  44         switch (GETBOOLEANTYPE(constraint)) {
  45         case ORDERCONST:
  46                 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
  47         case BOOLEANVAR:
  48                 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
  49         case LOGICOP:
  50                 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
  51         case PREDICATEOP:
  52                 return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
  53         default:
  54                 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
  55                 exit(-1);
  56         }
  57 }
  58
  59 void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray) {
  60         for (uint i = 0; i < num; i++)
  61                 carray[i] = getNewVarSATEncoder(encoder);
  62 }
  63
  64 Edge getNewVarSATEncoder(SATEncoder *This) {
  65         return constraintNewVar(This->cnf);
  66 }
  67
  68 Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) {
  69         if (edgeIsNull(constraint->var)) {
  70                 constraint->var = getNewVarSATEncoder(This);
  71         }
  72         return constraint->var;
  73 }
  74
  75 Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) {
  76         Edge array[constraint->inputs.getSize()];
  77         for (uint i = 0; i < constraint->inputs.getSize(); i++)
  78                 array[i] = encodeConstraintSATEncoder(This, constraint->inputs.get(i));
  79
  80         switch (constraint->op) {
  81         case L_AND:
  82                 return constraintAND(This->cnf, constraint->inputs.getSize(), array);
  83         case L_OR:
  84                 return constraintOR(This->cnf, constraint->inputs.getSize(), array);
  85         case L_NOT:
  86                 return constraintNegate(array[0]);
  87         case L_XOR:
  88                 return constraintXOR(This->cnf, array[0], array[1]);
  89         case L_IMPLIES:
  90                 return constraintIMPLIES(This->cnf, array[0], array[1]);
  91         default:
  92                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
  93                 exit(-1);
  94         }
  95 }
  96
  97 Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
  98         switch (GETPREDICATETYPE(constraint->predicate) ) {
  99         case TABLEPRED:
 100                 return encodeTablePredicateSATEncoder(This, constraint);
 101         case OPERATORPRED:
 102                 return encodeOperatorPredicateSATEncoder(This, constraint);
 103         default:
 104                 ASSERT(0);
 105         }
 106         return E_BOGUS;
 107 }
 108
 109 Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
 110         switch (constraint->encoding.type) {
 111         case ENUMERATEIMPLICATIONS:
 112         case ENUMERATEIMPLICATIONSNEGATE:
 113                 return encodeEnumTablePredicateSATEncoder(This, constraint);
 114         case CIRCUIT:
 115                 ASSERT(0);
 116                 break;
 117         default:
 118                 ASSERT(0);
 119         }
 120         return E_BOGUS;
 121 }
 122
 123 void encodeElementSATEncoder(SATEncoder *encoder, Element *This) {
 124         switch ( GETELEMENTTYPE(This) ) {
 125         case ELEMFUNCRETURN:
 126                 generateElementEncoding(encoder, This);
 127                 encodeElementFunctionSATEncoder(encoder, (ElementFunction *) This);
 128                 break;
 129         case ELEMSET:
 130                 generateElementEncoding(encoder, This);
 131                 return;
 132         case ELEMCONST:
 133                 return;
 134         default:
 135                 ASSERT(0);
 136         }
 137 }
 138
 139 void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
 140         switch (GETFUNCTIONTYPE(This->function)) {
 141         case TABLEFUNC:
 142                 encodeTableElementFunctionSATEncoder(encoder, This);
 143                 break;
 144         case OPERATORFUNC:
 145                 encodeOperatorElementFunctionSATEncoder(encoder, This);
 146                 break;
 147         default:
 148                 ASSERT(0);
 149         }
 150 }
 151
 152 void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
 153         switch (getElementFunctionEncoding(This)->type) {
 154         case ENUMERATEIMPLICATIONS:
 155                 encodeEnumTableElemFunctionSATEncoder(encoder, This);
 156                 break;
 157         case CIRCUIT:
 158                 ASSERT(0);
 159                 break;
 160         default:
 161                 ASSERT(0);
 162         }
 163 }