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
  13
  14 SATEncoder * allocSATEncoder() {
  15         SATEncoder *This=ourmalloc(sizeof (SATEncoder));
  16         This->varcount=1;
  17         return This;
  18 }
  19
  20 void deleteSATEncoder(SATEncoder *This) {
  21         ourfree(This);
  22 }
  23
  24 void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
  25         uint size = getSizeVectorElement(csolver->allElements);
  26         for(uint i=0; i<size; i++){
  27                 Element* element = getVectorElement(csolver->allElements, i);
  28                 generateElementEncodingVariables(This,getElementEncoding(element));
  29         }
  30 }
  31
  32 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
  33         VectorBoolean *constraints=csolver->constraints;
  34         uint size=getSizeVectorBoolean(constraints);
  35         for(uint i=0;i<size;i++) {
  36                 Boolean *constraint=getVectorBoolean(constraints, i);
  37                 encodeConstraintSATEncoder(This, constraint);
  38         }
  39
  40         size = getSizeVectorElement(csolver->allElements);
  41         for(uint i=0; i<size; i++){
  42                 Element* element = getVectorElement(csolver->allElements, i);
  43                 switch(GETELEMENTTYPE(element)){
  44                         case ELEMFUNCRETURN:
  45                                 encodeFunctionElementSATEncoder(This, (ElementFunction*) element);
  46                                 break;
  47                         default:
  48                                 continue;
  49                                 //ElementSets that aren't used in any constraints/functions
  50                                 //will be eliminated.
  51                 }
  52         }
  53 }
  54
  55 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
  56         switch(GETBOOLEANTYPE(constraint)) {
  57         case ORDERCONST:
  58                 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
  59         case BOOLEANVAR:
  60                 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
  61         case LOGICOP:
  62                 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
  63         case PREDICATEOP:
  64                 return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
  65         default:
  66                 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
  67                 exit(-1);
  68         }
  69 }
  70
  71 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
  72         for(uint i=0;i<num;i++)
  73                 carray[i]=getNewVarSATEncoder(encoder);
  74 }
  75
  76 Constraint * getNewVarSATEncoder(SATEncoder *This) {
  77         Constraint * var=allocVarConstraint(VAR, This->varcount);
  78         Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
  79         setNegConstraint(var, varneg);
  80         setNegConstraint(varneg, var);
  81         return var;
  82 }
  83
  84 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
  85         if (constraint->var == NULL) {
  86                 constraint->var=getNewVarSATEncoder(This);
  87         }
  88         return constraint->var;
  89 }
  90
  91 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
  92         Constraint * array[getSizeArrayBoolean(&constraint->inputs)];
  93         for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
  94                 array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
  95
  96         switch(constraint->op) {
  97         case L_AND:
  98                 return allocArrayConstraint(AND, getSizeArrayBoolean(&constraint->inputs), array);
  99         case L_OR:
 100                 return allocArrayConstraint(OR, getSizeArrayBoolean(&constraint->inputs), array);
 101         case L_NOT:
 102                 ASSERT(constraint->numArray==1);
 103                 return negateConstraint(array[0]);
 104         case L_XOR: {
 105                 ASSERT(constraint->numArray==2);
 106                 Constraint * nleft=negateConstraint(cloneConstraint(array[0]));
 107                 Constraint * nright=negateConstraint(cloneConstraint(array[1]));
 108                 return allocConstraint(OR,
 109                                                                                                          allocConstraint(AND, array[0], nright),
 110                                                                                                          allocConstraint(AND, nleft, array[1]));
 111         }
 112         case L_IMPLIES:
 113                 ASSERT(constraint->numArray==2);
 114                 return allocConstraint(IMPLIES, array[0], array[1]);
 115         default:
 116                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
 117                 exit(-1);
 118         }
 119 }
 120
 121 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
 122         if(constraint->var== NULL){
 123                 constraint->var = getNewVarSATEncoder(This);
 124         }
 125         return constraint->var;
 126 }
 127
 128 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
 129         //TO IMPLEMENT
 130
 131         return NULL;
 132 }
 133
 134 Constraint* encodeFunctionElementSATEncoder(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 NULL;
 144 }
 145
 146 Constraint* 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 NULL;
 158 }
 159
 160 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 161         //FIXME: for now it just adds/substracts inputs exhustively
 162         return NULL;
 163 }
 164
 165 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 166         ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
 167         ArrayElement* elements= &This->inputs;
 168         Table* table = ((FunctionTable*) (This->function))->table;
 169         uint size = getSizeVectorTableEntry(&table->entries);
 170         Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
 171         for(uint i=0; i<size; i++){
 172                 TableEntry* entry = getVectorTableEntry(&table->entries, i);
 173                 uint inputNum =getSizeArrayElement(elements);
 174                 Element* el= getArrayElement(elements, i);
 175                 Constraint* carray[inputNum];
 176                 for(uint j=0; j<inputNum; j++){
 177                          carray[inputNum] = getElementValueBinaryIndexConstraint(el, entry->inputs[j]);
 178                 }
 179                 Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
 180                         getElementValueBinaryIndexConstraint((Element*)This, entry->output));
 181                 constraints[i]=row;
 182         }
 183         Constraint* result = allocArrayConstraint(OR, size, constraints);
 184         return result;
 185 }