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(CSolver *solver) {
  19         SATEncoder *This = 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=iteratorBoolean(csolver->constraints);
  33         while(hasNextBoolean(iterator)) {
  34                 Boolean *constraint = nextBoolean(iterator);
  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         deleteIterBoolean(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[getSizeArrayBoolean(&constraint->inputs)];
  77         for (uint i = 0; i < getSizeArrayBoolean(&constraint->inputs); i++)
  78                 array[i] = encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
  79
  80         switch (constraint->op) {
  81         case L_AND:
  82                 return constraintAND(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
  83         case L_OR:
  84                 return constraintOR(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
  85         case L_NOT:
  86                 ASSERT( getSizeArrayBoolean(&constraint->inputs) == 1);
  87                 return constraintNegate(array[0]);
  88         case L_XOR:
  89                 ASSERT( getSizeArrayBoolean(&constraint->inputs) == 2);
  90                 return constraintXOR(This->cnf, array[0], array[1]);
  91         case L_IMPLIES:
  92                 ASSERT( getSizeArrayBoolean( &constraint->inputs) == 2);
  93                 return constraintIMPLIES(This->cnf, array[0], array[1]);
  94         default:
  95                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
  96                 exit(-1);
  97         }
  98 }
  99
 100 Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
 101         switch (GETPREDICATETYPE(constraint->predicate) ) {
 102         case TABLEPRED:
 103                 return encodeTablePredicateSATEncoder(This, constraint);
 104         case OPERATORPRED:
 105                 return encodeOperatorPredicateSATEncoder(This, constraint);
 106         default:
 107                 ASSERT(0);
 108         }
 109         return E_BOGUS;
 110 }
 111
 112 Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
 113         switch (constraint->encoding.type) {
 114         case ENUMERATEIMPLICATIONS:
 115         case ENUMERATEIMPLICATIONSNEGATE:
 116                 return encodeEnumTablePredicateSATEncoder(This, constraint);
 117         case CIRCUIT:
 118                 ASSERT(0);
 119                 break;
 120         default:
 121                 ASSERT(0);
 122         }
 123         return E_BOGUS;
 124 }
 125
 126 void encodeElementSATEncoder(SATEncoder *encoder, Element *This) {
 127         switch ( GETELEMENTTYPE(This) ) {
 128         case ELEMFUNCRETURN:
 129                 generateElementEncoding(encoder, This);
 130                 encodeElementFunctionSATEncoder(encoder, (ElementFunction *) This);
 131                 break;
 132         case ELEMSET:
 133                 generateElementEncoding(encoder, This);
 134                 return;
 135         case ELEMCONST:
 136                 return;
 137         default:
 138                 ASSERT(0);
 139         }
 140 }
 141
 142 void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
 143         switch (GETFUNCTIONTYPE(This->function)) {
 144         case TABLEFUNC:
 145                 encodeTableElementFunctionSATEncoder(encoder, This);
 146                 break;
 147         case OPERATORFUNC:
 148                 encodeOperatorElementFunctionSATEncoder(encoder, This);
 149                 break;
 150         default:
 151                 ASSERT(0);
 152         }
 153 }
 154
 155 void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
 156         switch (getElementFunctionEncoding(This)->type) {
 157         case ENUMERATEIMPLICATIONS:
 158                 encodeEnumTableElemFunctionSATEncoder(encoder, This);
 159                 break;
 160         case CIRCUIT:
 161                 ASSERT(0);
 162                 break;
 163         default:
 164                 ASSERT(0);
 165         }
 166 }