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