src/Backend/satencoder.c

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