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 "orderpair.h"
  14 #include "set.h"
  15
  16 SATEncoder * allocSATEncoder() {
  17         SATEncoder *This=ourmalloc(sizeof (SATEncoder));
  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         /** We really should not walk the free list to generate constraint
  28                         variables...walk the constraint tree instead.  Or even better
  29                         yet, just do this as you need to during the encodeAllSATEncoder
  30                         walk.  */
  31
  32 //      FIXME!!!!(); // Make sure Hamed sees comment above
  33
  34         uint size = getSizeVectorElement(csolver->allElements);
  35         for(uint i=0; i<size; i++){
  36                 Element* element = getVectorElement(csolver->allElements, i);
  37                 generateElementEncodingVariables(This,getElementEncoding(element));
  38         }
  39 }
  40
  41
  42 Constraint * getElementValueConstraint(Element* This, uint64_t value) {
  43         switch(getElementEncoding(This)->type){
  44                 case ONEHOT:
  45                         ASSERT(0);
  46                         break;
  47                 case UNARY:
  48                         ASSERT(0);
  49                         break;
  50                 case BINARYINDEX:
  51                         ASSERT(0);
  52                         break;
  53                 case ONEHOTBINARY:
  54                         return getElementValueBinaryIndexConstraint(This, value);
  55                         break;
  56                 case BINARYVAL:
  57                         ASSERT(0);
  58                         break;
  59                 default:
  60                         ASSERT(0);
  61                         break;
  62         }
  63         return NULL;
  64 }
  65 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
  66         ASTNodeType type = GETELEMENTTYPE(This);
  67         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
  68         ElementEncoding* elemEnc = getElementEncoding(This);
  69         for(uint i=0; i<elemEnc->encArraySize; i++){
  70                 if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
  71                         return generateBinaryConstraint(elemEnc->numVars,
  72                                 elemEnc->variables, i);
  73                 }
  74         }
  75         ASSERT(0);
  76         return NULL;
  77 }
  78
  79 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
  80         VectorBoolean *constraints=csolver->constraints;
  81         uint size=getSizeVectorBoolean(constraints);
  82         for(uint i=0;i<size;i++) {
  83                 Boolean *constraint=getVectorBoolean(constraints, i);
  84                 encodeConstraintSATEncoder(This, constraint);
  85         }
  86
  87 //      FIXME: Following line for element!
  88 //      size = getSizeVectorElement(csolver->allElements);
  89 //      for(uint i=0; i<size; i++){
  90 //              Element* element = getVectorElement(csolver->allElements, i);
  91 //              switch(GETELEMENTTYPE(element)){
  92 //                      case ELEMFUNCRETURN:
  93 //                              encodeFunctionElementSATEncoder(This, (ElementFunction*) element);
  94 //                              break;
  95 //                      default:
  96 //                              continue;
  97 //                              //ElementSets that aren't used in any constraints/functions
  98 //                              //will be eliminated.
  99 //              }
 100 //      }
 101 }
 102
 103 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
 104         switch(GETBOOLEANTYPE(constraint)) {
 105         case ORDERCONST:
 106                 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
 107         case BOOLEANVAR:
 108                 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
 109         case LOGICOP:
 110                 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
 111         case PREDICATEOP:
 112                 return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
 113         default:
 114                 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
 115                 exit(-1);
 116         }
 117 }
 118
 119 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
 120         for(uint i=0;i<num;i++)
 121                 carray[i]=getNewVarSATEncoder(encoder);
 122 }
 123
 124 Constraint * getNewVarSATEncoder(SATEncoder *This) {
 125         Constraint * var=allocVarConstraint(VAR, This->varcount);
 126         Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
 127         setNegConstraint(var, varneg);
 128         setNegConstraint(varneg, var);
 129         return var;
 130 }
 131
 132 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
 133         if (constraint->var == NULL) {
 134                 constraint->var=getNewVarSATEncoder(This);
 135         }
 136         return constraint->var;
 137 }
 138
 139 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
 140         Constraint * array[getSizeArrayBoolean(&constraint->inputs)];
 141         for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
 142                 array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
 143
 144         switch(constraint->op) {
 145         case L_AND:
 146                 return allocArrayConstraint(AND, getSizeArrayBoolean(&constraint->inputs), array);
 147         case L_OR:
 148                 return allocArrayConstraint(OR, getSizeArrayBoolean(&constraint->inputs), array);
 149         case L_NOT:
 150                 ASSERT(constraint->numArray==1);
 151                 return negateConstraint(array[0]);
 152         case L_XOR: {
 153                 ASSERT(constraint->numArray==2);
 154                 Constraint * nleft=negateConstraint(cloneConstraint(array[0]));
 155                 Constraint * nright=negateConstraint(cloneConstraint(array[1]));
 156                 return allocConstraint(OR,
 157                                                                                                          allocConstraint(AND, array[0], nright),
 158                                                                                                          allocConstraint(AND, nleft, array[1]));
 159         }
 160         case L_IMPLIES:
 161                 ASSERT(constraint->numArray==2);
 162                 return allocConstraint(IMPLIES, array[0], array[1]);
 163         default:
 164                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
 165                 exit(-1);
 166         }
 167 }
 168
 169
 170 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
 171         switch( constraint->order->type){
 172                 case PARTIAL:
 173                         return encodePartialOrderSATEncoder(This, constraint);
 174                 case TOTAL:
 175                         return encodeTotalOrderSATEncoder(This, constraint);
 176                 default:
 177                         ASSERT(0);
 178         }
 179         return NULL;
 180 }
 181
 182
 183 Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
 184         ASSERT(boolOrder->order->type == TOTAL);
 185         HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
 186         OrderPair* pair = allocOrderPair(boolOrder->first, boolOrder->second);
 187         if( !containsBoolConst(boolToConsts, pair) ){
 188                 createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
 189         }
 190         Constraint* constraint = getOrderConstraint(boolToConsts, pair);
 191         deleteOrderPair(pair);
 192         return constraint;
 193 }
 194
 195 void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
 196         ASSERT(order->type == TOTAL);
 197         VectorInt* mems = order->set->members;
 198         HashTableBoolConst* table = order->boolsToConstraints;
 199         uint size = getSizeVectorInt(mems);
 200         for(uint i=0; i<size; i++){
 201                 uint64_t valueI = getVectorInt(mems, i);
 202                 for(uint j=i+1; j<size;j++){
 203                         uint64_t valueJ = getVectorInt(mems, j);
 204                         OrderPair* pairIJ = allocOrderPair(valueI, valueJ);
 205                         ASSERT(!containsBoolConst(table, pairIJ));
 206                         Constraint* constIJ = getNewVarSATEncoder(This);
 207                         putBoolConst(table, pairIJ, constIJ);
 208                         for(uint k=j+1; k<size; k++){
 209                                 uint64_t valueK = getVectorInt(mems, k);
 210                                 OrderPair* pairJK = allocOrderPair(valueJ, valueK);
 211                                 OrderPair* pairIK = allocOrderPair(valueI, valueK);
 212                                 Constraint* constJK, *constIK;
 213                                 if(!containsBoolConst(table, pairJK)){
 214                                         constJK = getNewVarSATEncoder(This);
 215                                         putBoolConst(table, pairJK, constJK);
 216                                 }
 217                                 if(!containsBoolConst(table, pairIK)){
 218                                         constIK = getNewVarSATEncoder(This);
 219                                         putBoolConst(table, pairIK, constIK);
 220                                 }
 221                                 generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK);
 222                         }
 223                 }
 224         }
 225 }
 226
 227 Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
 228         ASSERT(pair->first!= pair->second);
 229         Constraint* constraint= getBoolConst(table, pair);
 230         ASSERT(constraint!= NULL);
 231         if(pair->first > pair->second)
 232                 return constraint;
 233         else
 234                 return negateConstraint(constraint);
 235 }
 236
 237 Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK){
 238         //FIXME: first we should add the the constraint to the satsolver!
 239         Constraint *carray[] = {constIJ, constJK, negateConstraint(constIK)};
 240         Constraint * loop1= allocArrayConstraint(OR, 3, carray);
 241         Constraint * carray2[] = {negateConstraint(constIJ), negateConstraint(constJK), constIK};
 242         Constraint * loop2= allocArrayConstraint(OR, 3,carray2 );
 243         return allocConstraint(AND, loop1, loop2);
 244 }
 245
 246 Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
 247         // FIXME: we can have this implementation for partial order. Basically,
 248         // we compute the transitivity between two order constraints specified by the client! (also can be used
 249         // when client specify sparse constraints for the total order!)
 250         ASSERT(boolOrder->order->type == PARTIAL);
 251 /*
 252         HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
 253         if( containsBoolConst(boolToConsts, boolOrder) ){
 254                 return getBoolConst(boolToConsts, boolOrder);
 255         } else {
 256                 Constraint* constraint = getNewVarSATEncoder(This);
 257                 putBoolConst(boolToConsts,boolOrder, constraint);
 258                 VectorBoolean* orderConstrs = &boolOrder->order->constraints;
 259                 uint size= getSizeVectorBoolean(orderConstrs);
 260                 for(uint i=0; i<size; i++){
 261                         ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
 262                         BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i);
 263                         BooleanOrder* newBool;
 264                         Constraint* first, *second;
 265                         if(tmp->second==boolOrder->first){
 266                                 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second);
 267                                 first = encodeTotalOrderSATEncoder(This, tmp);
 268                                 second = constraint;
 269
 270                         }else if (boolOrder->second == tmp->first){
 271                                 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,boolOrder->first,tmp->second);
 272                                 first = constraint;
 273                                 second = encodeTotalOrderSATEncoder(This, tmp);
 274                         }else
 275                                 continue;
 276                         Constraint* transConstr= encodeTotalOrderSATEncoder(This, newBool);
 277                         generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
 278                 }
 279                 return constraint;
 280         }
 281 */
 282         return NULL;
 283 }
 284
 285 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
 286         switch(GETPREDICATETYPE(constraint) ){
 287                 case TABLEPRED:
 288                         return encodeTablePredicateSATEncoder(This, constraint);
 289                 case OPERATORPRED:
 290                         return encodeOperatorPredicateSATEncoder(This, constraint);
 291                 default:
 292                         ASSERT(0);
 293         }
 294         return NULL;
 295 }
 296
 297 Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 298         switch(constraint->encoding.type){
 299                 case ENUMERATEIMPLICATIONS:
 300                         return encodeEnumTablePredicateSATEncoder(This, constraint);
 301                 case CIRCUIT:
 302                         ASSERT(0);
 303                         break;
 304                 default:
 305                         ASSERT(0);
 306         }
 307         return NULL;
 308 }
 309
 310 Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 311         VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
 312         uint size = getSizeVectorTableEntry(entries);
 313         for(uint i=0; i<size; i++){
 314                 TableEntry* entry = getVectorTableEntry(entries, i);
 315
 316         }
 317         return NULL;
 318 }
 319
 320 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 321         switch(constraint->encoding.type){
 322                 case ENUMERATEIMPLICATIONS:
 323                         break;
 324                 case CIRCUIT:
 325                         break;
 326                 default:
 327                         ASSERT(0);
 328         }
 329         return NULL;
 330 }
 331
 332 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
 333         switch(GETFUNCTIONTYPE(This->function)){
 334                 case TABLEFUNC:
 335                         return encodeTableElementFunctionSATEncoder(encoder, This);
 336                 case OPERATORFUNC:
 337                         return encodeOperatorElementFunctionSATEncoder(encoder, This);
 338                 default:
 339                         ASSERT(0);
 340         }
 341         return NULL;
 342 }
 343
 344 Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 345         switch(getElementFunctionEncoding(This)->type){
 346                 case ENUMERATEIMPLICATIONS:
 347                         return encodeEnumTableElemFunctionSATEncoder(encoder, This);
 348                         break;
 349                 case CIRCUIT:
 350                         ASSERT(0);
 351                         break;
 352                 default:
 353                         ASSERT(0);
 354         }
 355         return NULL;
 356 }
 357
 358 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 359         //FIXME: for now it just adds/substracts inputs exhustively
 360         return NULL;
 361 }
 362
 363 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 364         ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
 365         ArrayElement* elements= &This->inputs;
 366         Table* table = ((FunctionTable*) (This->function))->table;
 367         uint size = getSizeVectorTableEntry(&table->entries);
 368         Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
 369         for(uint i=0; i<size; i++){
 370                 TableEntry* entry = getVectorTableEntry(&table->entries, i);
 371                 uint inputNum =getSizeArrayElement(elements);
 372                 Element* el= getArrayElement(elements, i);
 373                 Constraint* carray[inputNum];
 374                 for(uint j=0; j<inputNum; j++){
 375                         carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
 376                 }
 377                 Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
 378                         getElementValueBinaryIndexConstraint((Element*)This, entry->output));
 379                 constraints[i]=row;
 380         }
 381         Constraint* result = allocArrayConstraint(OR, size, constraints);
 382         return result;
 383 }