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