src/Backend/constraint.c

   1 /*      Copyright (c) 2015 Regents of the University of California
   2  *
   3  *      Author: Brian Demsky <bdemsky@uci.edu>
   4  *
   5  *      This program is free software; you can redistribute it and/or
   6  *      modify it under the terms of the GNU General Public License
   7  *      version 2 as published by the Free Software Foundation.
   8  */
   9
  10 #include "constraint.h"
  11 #include "mymemory.h"
  12 #include "inc_solver.h"
  13
  14 Constraint ctrue={TRUE, 0xffffffff, NULL, NULL};
  15 Constraint cfalse={FALSE, 0xffffffff, NULL, NULL};
  16
  17 Constraint * allocConstraint(CType t, Constraint *l, Constraint *r) {
  18         Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
  19         This->type=t;
  20         This->numoperandsorvar=2;
  21         This->operands=(Constraint **)ourmalloc(2*sizeof(Constraint *));
  22         This->neg=NULL;
  23         ASSERT(l!=NULL);
  24         //if (type==IMPLIES) {
  25         //type=OR;
  26         //      operands[0]=l->negate();
  27         //      } else {
  28         This->operands[0]=l;
  29         //      }
  30         This->operands[1]=r;
  31         return This;
  32 }
  33
  34 Constraint * allocUnaryConstraint(CType t, Constraint *l) {
  35         Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
  36         This->type=t;
  37         This->numoperandsorvar=1;
  38         This->operands=(Constraint **) ourmalloc(sizeof(Constraint *));
  39         This->neg=NULL;
  40         This->operands[0]=l;
  41         return This;
  42 }
  43
  44 Constraint * allocArrayConstraint(CType t, uint num, Constraint **array) {
  45         Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
  46         This->type=t;
  47         This->numoperandsorvar=num;
  48         This->operands=(Constraint **) ourmalloc(num*sizeof(Constraint *));
  49         This->neg=NULL;
  50         memcpy(This->operands, array, num*sizeof(Constraint *));
  51         return This;
  52 }
  53
  54 Constraint * allocVarConstraint(CType t, uint v) {
  55         Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
  56         This->type=t;
  57         This->numoperandsorvar=v;
  58         This->operands=NULL;
  59         This->neg=NULL;
  60         return This;
  61 }
  62
  63 void deleteConstraint(Constraint *This) {
  64         if (This->operands!=NULL)
  65                 ourfree(This->operands);
  66         ourfree(This);
  67 }
  68
  69 void dumpConstraint(Constraint * This, IncrementalSolver *solver) {
  70         if (This->type==VAR) {
  71                 addClauseLiteral(solver, This->numoperandsorvar);
  72                 addClauseLiteral(solver, 0);
  73         } else if (This->type==NOTVAR) {
  74                 addClauseLiteral(solver, -This->numoperandsorvar);
  75                 addClauseLiteral(solver, 0);
  76         } else {
  77                 ASSERT(This->type==OR);
  78                 for(uint i=0;i<This->numoperandsorvar;i++) {
  79                         Constraint *c=This->operands[i];
  80                         if (c->type==VAR) {
  81                                 addClauseLiteral(solver, c->numoperandsorvar);
  82                         } else if (c->type==NOTVAR) {
  83                                 addClauseLiteral(solver, -c->numoperandsorvar);
  84                         } else ASSERT(0);
  85                 }
  86                 addClauseLiteral(solver, 0);
  87         }
  88 }
  89
  90 void internalfreeConstraint(Constraint * This) {
  91         switch(This->type) {
  92         case TRUE:
  93         case FALSE:
  94         case NOTVAR:
  95         case VAR:
  96                 return;
  97         case BOGUS:
  98                 ASSERT(0);
  99         default:
 100                 This->type=BOGUS;
 101                 deleteConstraint(This);
 102         }
 103 }
 104
 105 void freerecConstraint(Constraint *This) {
 106         switch(This->type) {
 107         case TRUE:
 108         case FALSE:
 109         case NOTVAR:
 110         case VAR:
 111                 return;
 112         case BOGUS:
 113                 ASSERT(0);
 114         default:
 115                 if (This->operands!=NULL) {
 116                         for(uint i=0;i<This->numoperandsorvar;i++)
 117                                 freerecConstraint(This->operands[i]);
 118                 }
 119                 This->type=BOGUS;
 120                 deleteConstraint(This);
 121         }
 122 }
 123
 124
 125 void printConstraint(Constraint * This) {
 126         switch(This->type) {
 127         case TRUE:
 128                 model_print("true");
 129                 break;
 130         case FALSE:
 131                 model_print("false");
 132                 break;
 133         case IMPLIES:
 134                 model_print("(");
 135                 printConstraint(This->operands[0]);
 136                 model_print(")");
 137                 model_print("=>");
 138                 model_print("(");
 139                 printConstraint(This->operands[1]);
 140                 model_print(")");
 141                 break;
 142         case AND:
 143         case OR:
 144                 model_print("(");
 145                 for(uint i=0;i<This->numoperandsorvar;i++) {
 146                         if (i!=0) {
 147                                 if (This->type==AND)
 148                                         model_print(" ^ ");
 149                                 else
 150                                         model_print(" v ");
 151                         }
 152                         printConstraint(This->operands[i]);
 153                 }
 154                 model_print(")");
 155                 break;
 156         case VAR:
 157                 model_print("t%u",This->numoperandsorvar);
 158                 break;
 159         case NOTVAR:
 160                 model_print("!t%u",This->numoperandsorvar);
 161                 break;
 162         default:
 163                 model_print("In printingConstraint: %d", This->type);
 164                 ASSERT(0);
 165         }
 166 }
 167
 168 Constraint * cloneConstraint(Constraint * This) {
 169         switch(This->type) {
 170         case TRUE:
 171         case FALSE:
 172         case VAR:
 173         case NOTVAR:
 174                 return This;
 175         case IMPLIES:
 176                 return allocConstraint(IMPLIES, cloneConstraint(This->operands[0]), cloneConstraint(This->operands[1]));
 177         case AND:
 178         case OR: {
 179                 Constraint *array[This->numoperandsorvar];
 180                 for(uint i=0;i<This->numoperandsorvar;i++) {
 181                         array[i]=cloneConstraint(This->operands[i]);
 182                 }
 183                 return allocArrayConstraint(This->type, This->numoperandsorvar, array);
 184         }
 185         default:
 186                 ASSERT(0);
 187                 return NULL;
 188         }
 189 }
 190
 191 Constraint * generateBinaryConstraint(uint numvars, Constraint ** vars, uint value) {
 192         Constraint *carray[numvars];
 193         for(uint j=0;j<numvars;j++) {
 194                 carray[j]=((value&1)==1) ? vars[j] : negateConstraint(vars[j]);
 195                 value=value>>1;
 196         }
 197
 198         return allocArrayConstraint(AND, numvars, carray);
 199 }
 200
 201 /** Generates a constraint to ensure that all encodings are less than value */
 202 Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value) {
 203         Constraint *orarray[numvars];
 204         Constraint *andarray[numvars];
 205         uint andi=0;
 206
 207         while(true) {
 208                 uint val=value;
 209                 uint ori=0;
 210                 for(uint j=0;j<numvars;j++) {
 211                         if ((val&1)==1)
 212                                 orarray[ori++]=negateConstraint(vars[j]);
 213                         val=val>>1;
 214                 }
 215                 //no ones to flip, so bail now...
 216                 if (ori==0) {
 217                         return allocArrayConstraint(AND, andi, andarray);
 218                 }
 219                 andarray[andi++]=allocArrayConstraint(OR, ori, orarray);
 220
 221                 value=value+(1<<(__builtin_ctz(value)));
 222                 //flip the last one
 223         }
 224 }
 225
 226 Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2) {
 227         if (numvars==0)
 228                 return &ctrue;
 229         Constraint *array[numvars*2];
 230         for(uint i=0;i<numvars;i++) {
 231                 array[i*2]=allocConstraint(OR, negateConstraint(cloneConstraint(var1[i])), var2[i]);
 232                 array[i*2+1]=allocConstraint(OR, var1[i], negateConstraint(cloneConstraint(var2[i])));
 233         }
 234         return allocArrayConstraint(AND, numvars*2, array);
 235 }
 236
 237 Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) {
 238         Constraint * imp1=allocConstraint(OR, negateConstraint(cloneConstraint(var1)), var2);
 239         Constraint * imp2=allocConstraint(OR, var1, negateConstraint(cloneConstraint(var2)));
 240
 241         return allocConstraint(AND, imp1, imp2);
 242 }
 243
 244 bool mergeandfree(VectorConstraint * to, VectorConstraint * from) {
 245         for(uint i=0;i<getSizeVectorConstraint(from);i++) {
 246                 Constraint *c=getVectorConstraint(from, i);
 247                 if (c->type==TRUE)
 248                         continue;
 249                 if (c->type==FALSE) {
 250                         for(uint j=i+1;j<getSizeVectorConstraint(from);j++)
 251                                 freerecConstraint(getVectorConstraint(from,j));
 252                         for(uint j=0;j<getSizeVectorConstraint(to);j++)
 253                                 freerecConstraint(getVectorConstraint(to, j));
 254                         clearVectorConstraint(to);
 255                         pushVectorConstraint(to, &ctrue);
 256                         deleteVectorConstraint(from);
 257                         return true;
 258                 }
 259                 pushVectorConstraint(to, c);
 260         }
 261         deleteVectorConstraint(from);
 262         return false;
 263 }
 264
 265 VectorConstraint * simplifyConstraint(Constraint * This) {
 266         switch(This->type) {
 267         case TRUE:
 268         case VAR:
 269         case NOTVAR:
 270         case FALSE: {
 271                 VectorConstraint * vec=allocDefVectorConstraint();
 272                 pushVectorConstraint(vec, This);
 273                 return vec;
 274         }
 275         case AND: {
 276                 VectorConstraint *vec=allocDefVectorConstraint();
 277                 for(uint i=0;i<This->numoperandsorvar;i++) {
 278                         VectorConstraint * subvec=simplifyConstraint(This->operands[i]);
 279                         if (mergeandfree(vec, subvec)) {
 280                                 for(uint j=i+1;j<This->numoperandsorvar;j++) {
 281                                         freerecConstraint(This->operands[j]);
 282                                 }
 283                                 internalfreeConstraint(This);
 284                                 return vec;
 285                         }
 286                 }
 287                 internalfreeConstraint(This);
 288                 return vec;
 289         }
 290         case OR: {
 291                 for(uint i=0;i<This->numoperandsorvar;i++) {
 292                         Constraint *c=This->operands[i];
 293                         switch(c->type) {
 294                         case TRUE: {
 295                                 VectorConstraint * vec=allocDefVectorConstraint();
 296                                 pushVectorConstraint(vec, c);
 297                                 freerecConstraint(This);
 298                                 return vec;
 299                         }
 300                         case FALSE: {
 301                                 Constraint *array[This->numoperandsorvar-1];
 302                                 uint index=0;
 303                                 for(uint j=0;j<This->numoperandsorvar;j++) {
 304                                         if (j!=i)
 305                                                 array[index++]=This->operands[j];
 306                                 }
 307                                 Constraint *cn=allocArrayConstraint(OR, index, array);
 308                                 VectorConstraint *vec=simplifyConstraint(cn);
 309                                 internalfreeConstraint(This);
 310                                 return vec;
 311                         }
 312                         case VAR:
 313                         case NOTVAR:
 314                                 break;
 315                         case OR: {
 316                                 uint nsize=This->numoperandsorvar+c->numoperandsorvar-1;
 317                                 Constraint *array[nsize];
 318                                 uint index=0;
 319                                 for(uint j=0;j<This->numoperandsorvar;j++)
 320                                         if (j!=i)
 321                                                 array[index++]=This->operands[j];
 322                                 for(uint j=0;j<c->numoperandsorvar;j++)
 323                                         array[index++]=c->operands[j];
 324                                 Constraint *cn=allocArrayConstraint(OR, nsize, array);
 325                                 VectorConstraint *vec=simplifyConstraint(cn);
 326                                 internalfreeConstraint(This);
 327                                 internalfreeConstraint(c);
 328                                 return vec;
 329                         }
 330                         case IMPLIES: {
 331                                 uint nsize=This->numoperandsorvar+1;
 332                                 Constraint *array[nsize];
 333                                 uint index=0;
 334                                 for(uint j=0;j<This->numoperandsorvar;j++)
 335                                         if (j!=i)
 336                                                 array[index++]=This->operands[j];
 337                                 array[index++]=negateConstraint(c->operands[0]);
 338                                 array[index++]=c->operands[1];
 339                                 Constraint *cn=allocArrayConstraint(OR, nsize, array);
 340                                 VectorConstraint *vec=simplifyConstraint(cn);
 341                                 internalfreeConstraint(This);
 342                                 internalfreeConstraint(c);
 343                                 return vec;
 344                         }
 345                         case AND: {
 346                                 Constraint *array[This->numoperandsorvar];
 347
 348                                 VectorConstraint *vec=allocDefVectorConstraint();
 349                                 for(uint j=0;j<c->numoperandsorvar;j++) {
 350                                         //copy other elements
 351                                         for(uint k=0;k<This->numoperandsorvar;k++) {
 352                                                 if (k!=i) {
 353                                                         array[k]=cloneConstraint(This->operands[k]);
 354                                                 }
 355                                         }
 356
 357                                         array[i]=cloneConstraint(c->operands[j]);
 358                                         Constraint *cn=allocArrayConstraint(OR, This->numoperandsorvar, array);
 359                                         VectorConstraint * newvec=simplifyConstraint(cn);
 360                                         if (mergeandfree(vec, newvec)) {
 361                                                 freerecConstraint(This);
 362                                                 return vec;
 363                                         }
 364                                 }
 365                                 freerecConstraint(This);
 366                                 return vec;
 367                         }
 368                         default:
 369                                 ASSERT(0);
 370                         }
 371                         //continue on to next item
 372                 }
 373                 VectorConstraint * vec=allocDefVectorConstraint();
 374                 if (This->numoperandsorvar==1) {
 375                         Constraint *c=This->operands[0];
 376                         freerecConstraint(This);
 377                         pushVectorConstraint(vec, c);
 378                 } else
 379                         pushVectorConstraint(vec, This);
 380                 return vec;
 381         }
 382         case IMPLIES: {
 383                 Constraint *cn=allocConstraint(OR, negateConstraint(This->operands[0]), This->operands[1]);
 384                 VectorConstraint * vec=simplifyConstraint(cn);
 385                 internalfreeConstraint(This);
 386                 return vec;
 387         }
 388         default:
 389                 ASSERT(0);
 390                 return NULL;
 391         }
 392 }
 393
 394 Constraint * negateConstraint(Constraint * This) {
 395         switch(This->type) {
 396         case TRUE:
 397                 return &cfalse;
 398         case FALSE:
 399                 return &ctrue;
 400         case NOTVAR:
 401         case VAR:
 402                 return This->neg;
 403         case IMPLIES: {
 404                 Constraint *l=This->operands[0];
 405                 Constraint *r=This->operands[1];
 406                 This->operands[0]=r;
 407                 This->operands[1]=l;
 408                 return This;
 409         }
 410         case AND:
 411         case OR: {
 412                 for(uint i=0;i<This->numoperandsorvar;i++) {
 413                         This->operands[i]=negateConstraint(This->operands[i]);
 414                 }
 415                 This->type=(This->type==AND) ? OR : AND;
 416                 return This;
 417         }
 418         default:
 419                 ASSERT(0);
 420                 return NULL;
 421         }
 422 }