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