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         /** We really should not walk the free list to generate constraint
  26                         variables...walk the constraint tree instead.  Or even better
  27                         yet, just do this as you need to during the encodeAllSATEncoder
  28                         walk.  */
  29
  30 //      FIXME!!!!(); // Make sure Hamed sees comment above
  31
  32         uint size = getSizeVectorElement(csolver->allElements);
  33         for(uint i=0; i<size; i++){
  34                 Element* element = getVectorElement(csolver->allElements, i);
  35                 generateElementEncodingVariables(This,getElementEncoding(element));
  36         }
  37 }
  38
  39
  40 Constraint * getElementValueConstraint(Element* This, uint64_t value) {
  41         switch(getElementEncoding(This)->type){
  42                 case ONEHOT:
  43                         ASSERT(0);
  44                         break;
  45                 case UNARY:
  46                         ASSERT(0);
  47                         break;
  48                 case BINARYINDEX:
  49                         ASSERT(0);
  50                         break;
  51                 case ONEHOTBINARY:
  52                         return getElementValueBinaryIndexConstraint(This, value);
  53                         break;
  54                 case BINARYVAL:
  55                         ASSERT(0);
  56                         break;
  57                 default:
  58                         ASSERT(0);
  59                         break;
  60         }
  61         return NULL;
  62 }
  63 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
  64         ASTNodeType type = GETELEMENTTYPE(This);
  65         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
  66         ElementEncoding* elemEnc = getElementEncoding(This);
  67         for(uint i=0; i<elemEnc->encArraySize; i++){
  68                 if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
  69                         return generateBinaryConstraint(elemEnc->numVars,
  70                                 elemEnc->variables, i);
  71                 }
  72         }
  73         ASSERT(0);
  74         return NULL;
  75 }
  76
  77 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
  78         VectorBoolean *constraints=csolver->constraints;
  79         uint size=getSizeVectorBoolean(constraints);
  80         for(uint i=0;i<size;i++) {
  81                 Boolean *constraint=getVectorBoolean(constraints, i);
  82                 encodeConstraintSATEncoder(This, constraint);
  83         }
  84
  85         size = getSizeVectorElement(csolver->allElements);
  86         for(uint i=0; i<size; i++){
  87                 Element* element = getVectorElement(csolver->allElements, i);
  88                 switch(GETELEMENTTYPE(element)){
  89                         case ELEMFUNCRETURN:
  90                                 encodeFunctionElementSATEncoder(This, (ElementFunction*) element);
  91                                 break;
  92                         default:
  93                                 continue;
  94                                 //ElementSets that aren't used in any constraints/functions
  95                                 //will be eliminated.
  96                 }
  97         }
  98 }
  99
 100 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
 101         switch(GETBOOLEANTYPE(constraint)) {
 102         case ORDERCONST:
 103                 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
 104         case BOOLEANVAR:
 105                 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
 106         case LOGICOP:
 107                 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
 108         case PREDICATEOP:
 109                 return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
 110         default:
 111                 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
 112                 exit(-1);
 113         }
 114 }
 115
 116 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
 117         for(uint i=0;i<num;i++)
 118                 carray[i]=getNewVarSATEncoder(encoder);
 119 }
 120
 121 Constraint * getNewVarSATEncoder(SATEncoder *This) {
 122         Constraint * var=allocVarConstraint(VAR, This->varcount);
 123         Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
 124         setNegConstraint(var, varneg);
 125         setNegConstraint(varneg, var);
 126         return var;
 127 }
 128
 129 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
 130         if (constraint->var == NULL) {
 131                 constraint->var=getNewVarSATEncoder(This);
 132         }
 133         return constraint->var;
 134 }
 135
 136 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
 137         Constraint * array[getSizeArrayBoolean(&constraint->inputs)];
 138         for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
 139                 array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
 140
 141         switch(constraint->op) {
 142         case L_AND:
 143                 return allocArrayConstraint(AND, getSizeArrayBoolean(&constraint->inputs), array);
 144         case L_OR:
 145                 return allocArrayConstraint(OR, getSizeArrayBoolean(&constraint->inputs), array);
 146         case L_NOT:
 147                 ASSERT(constraint->numArray==1);
 148                 return negateConstraint(array[0]);
 149         case L_XOR: {
 150                 ASSERT(constraint->numArray==2);
 151                 Constraint * nleft=negateConstraint(cloneConstraint(array[0]));
 152                 Constraint * nright=negateConstraint(cloneConstraint(array[1]));
 153                 return allocConstraint(OR,
 154                                                                                                          allocConstraint(AND, array[0], nright),
 155                                                                                                          allocConstraint(AND, nleft, array[1]));
 156         }
 157         case L_IMPLIES:
 158                 ASSERT(constraint->numArray==2);
 159                 return allocConstraint(IMPLIES, array[0], array[1]);
 160         default:
 161                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
 162                 exit(-1);
 163         }
 164 }
 165
 166 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
 167         switch( constraint->order->type){
 168                 case PARTIAL:
 169                         return encodePartialOrderSATEncoder(This, constraint);
 170                 case TOTAL:
 171                         return encodeTotalOrderSATEncoder(This, constraint);
 172                 default:
 173                         ASSERT(0);
 174         }
 175         return NULL;
 176 }
 177
 178 Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
 179         ASSERT(boolOrder->order->type == TOTAL);
 180         HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
 181         if( containsBoolConst(boolToConsts, boolOrder) ){
 182                 return getBoolConst(boolToConsts, boolOrder);
 183         } else {
 184                 Constraint* constraint = getNewVarSATEncoder(This);
 185                 putBoolConst(boolToConsts,boolOrder, constraint);
 186                 VectorBoolean* orderConstrs = &boolOrder->order->constraints;
 187                 uint size= getSizeVectorBoolean(orderConstrs);
 188                 for(uint i=0; i<size; i++){
 189                         ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
 190                         BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i);
 191                         BooleanOrder* newBool;
 192                         Constraint *first, *second;
 193                         if(tmp->second==boolOrder->first){
 194                                 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second);
 195                                 first = encodeTotalOrderSATEncoder(This, tmp);
 196                                 second = constraint;
 197
 198                         }else if (boolOrder->second == tmp->first){
 199                                 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,boolOrder->first,tmp->second);
 200                                 first = constraint;
 201                                 second = encodeTotalOrderSATEncoder(This, tmp);
 202                         }else
 203                                 continue;
 204                         Constraint* transConstr= encodeTotalOrderSATEncoder(This, newBool);
 205                         generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
 206                 }
 207                 return constraint;
 208         }
 209
 210         return NULL;
 211 }
 212
 213 Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *first,Constraint *second,Constraint *third){
 214         //FIXME: first we should add the the constraint to the satsolver!
 215         return allocConstraint(IMPLIES, allocConstraint(AND, first, second), third);
 216 }
 217
 218 Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
 219         return NULL;
 220 }
 221
 222 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
 223         //TO IMPLEMENT
 224
 225         return NULL;
 226 }
 227
 228 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
 229         switch(GETFUNCTIONTYPE(This->function)){
 230                 case TABLEFUNC:
 231                         return encodeTableElementFunctionSATEncoder(encoder, This);
 232                 case OPERATORFUNC:
 233                         return encodeOperatorElementFunctionSATEncoder(encoder, This);
 234                 default:
 235                         ASSERT(0);
 236         }
 237         return NULL;
 238 }
 239
 240 Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 241         switch(getElementFunctionEncoding(This)->type){
 242                 case ENUMERATEIMPLICATIONS:
 243                         return encodeEnumTableElemFunctionSATEncoder(encoder, This);
 244                         break;
 245                 case CIRCUIT:
 246                         ASSERT(0);
 247                         break;
 248                 default:
 249                         ASSERT(0);
 250         }
 251         return NULL;
 252 }
 253
 254 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 255         //FIXME: for now it just adds/substracts inputs exhustively
 256         return NULL;
 257 }
 258
 259 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 260         ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
 261         ArrayElement* elements= &This->inputs;
 262         Table* table = ((FunctionTable*) (This->function))->table;
 263         uint size = getSizeVectorTableEntry(&table->entries);
 264         Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
 265         for(uint i=0; i<size; i++){
 266                 TableEntry* entry = getVectorTableEntry(&table->entries, i);
 267                 uint inputNum =getSizeArrayElement(elements);
 268                 Element* el= getArrayElement(elements, i);
 269                 Constraint* carray[inputNum];
 270                 for(uint j=0; j<inputNum; j++){
 271                         carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
 272                 }
 273                 Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
 274                         getElementValueBinaryIndexConstraint((Element*)This, entry->output));
 275                 constraints[i]=row;
 276         }
 277         Constraint* result = allocArrayConstraint(OR, size, constraints);
 278         return result;
 279 }