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
   7 SATEncoder * allocSATEncoder() {
   8         SATEncoder *This=ourmalloc(sizeof (SATEncoder));
   9         This->varcount=1;
  10         return This;
  11 }
  12
  13 void deleteSATEncoder(SATEncoder *This) {
  14         ourfree(This);
  15 }
  16
  17 void encodeAllSATEncoder(SATEncoder * This, CSolver *csolver) {
  18         VectorBoolean *constraints=csolver->constraints;
  19         uint size=getSizeVectorBoolean(constraints);
  20         for(uint i=0;i<size;i++) {
  21                 Boolean *constraint=getVectorBoolean(constraints, i);
  22                 encodeConstraintSATEncoder(This, constraint);
  23         }
  24 }
  25
  26 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
  27         switch(GETBOOLEANTYPE(constraint)) {
  28         case ORDERCONST:
  29                 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
  30         case BOOLEANVAR:
  31                 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
  32         case LOGICOP:
  33                 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
  34         default:
  35                 printf("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
  36                 exit(-1);
  37         }
  38 }
  39
  40 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
  41         return NULL;
  42 }
  43
  44 Constraint * getNewVarSATEncoder(SATEncoder *This) {
  45         Constraint * var=allocVarConstraint(VAR, This->varcount);
  46         Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
  47         setNegConstraint(var, varneg);
  48         setNegConstraint(varneg, var);
  49         return var;
  50 }
  51
  52 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
  53         if (constraint->var == NULL) {
  54                 constraint->var=getNewVarSATEncoder(This);
  55         }
  56         return constraint->var;
  57 }
  58
  59 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
  60         Constraint * array[constraint->numArray];
  61         for(uint i=0;i<constraint->numArray;i++)
  62                 array[i]=encodeConstraintSATEncoder(This, constraint->array[i]);
  63
  64         switch(constraint->op) {
  65         case L_AND:
  66                 return allocArrayConstraint(AND, constraint->numArray, array);
  67         case L_OR:
  68                 return allocArrayConstraint(OR, constraint->numArray, array);
  69         case L_NOT:
  70                 return negateConstraint(allocConstraint(OR, array[0], NULL));
  71         case L_XOR: {
  72                 Constraint * nleft=negateConstraint(cloneConstraint(array[0]));
  73                 Constraint * nright=negateConstraint(cloneConstraint(array[1]));
  74                 return allocConstraint(OR,
  75                                                                                                          allocConstraint(AND, array[0], nright),
  76                                                                                                          allocConstraint(AND, nleft, array[1]));
  77         }
  78         case L_IMPLIES:
  79                 return allocConstraint(IMPLIES, array[0], array[1]);
  80         default:
  81                 printf("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
  82                 exit(-1);
  83         }
  84
  85         return NULL;
  86 }