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