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