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