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 }
  67
  68 void dumpConstraint(Constraint * This, IncrementalSolver *solver) {
  69         if (This->type==VAR) {
  70                 addClauseLiteral(solver, This->numoperandsorvar);
  71                 addClauseLiteral(solver, 0);
  72         } else if (This->type==NOTVAR) {
  73                 addClauseLiteral(solver, -This->numoperandsorvar);
  74                 addClauseLiteral(solver, 0);
  75         } else {
  76                 ASSERT(This->type==OR);
  77                 for(uint i=0;i<This->numoperandsorvar;i++) {
  78                         Constraint *c=This->operands[i];
  79                         if (c->type==VAR) {
  80                                 addClauseLiteral(solver, c->numoperandsorvar);
  81                         } else if (c->type==NOTVAR) {
  82                                 addClauseLiteral(solver, -c->numoperandsorvar);
  83                         } else ASSERT(0);
  84                 }
  85                 addClauseLiteral(solver, 0);
  86         }
  87 }
  88
  89 void internalfreeConstraint(Constraint * This) {
  90         switch(This->type) {
  91         case TRUE:
  92         case FALSE:
  93         case NOTVAR:
  94         case VAR:
  95                 return;
  96         case BOGUS:
  97                 ASSERT(0);
  98         default:
  99                 This->type=BOGUS;
 100                 ourfree(This);
 101         }
 102 }
 103
 104 void freerecConstraint(Constraint *This) {
 105         switch(This->type) {
 106         case TRUE:
 107         case FALSE:
 108         case NOTVAR:
 109         case VAR:
 110                 return;
 111         case BOGUS:
 112                 ASSERT(0);
 113         default:
 114                 if (This->operands!=NULL) {
 115                         for(uint i=0;i<This->numoperandsorvar;i++)
 116                                 freerecConstraint(This->operands[i]);
 117                 }
 118                 This->type=BOGUS;
 119                 deleteConstraint(This);
 120         }
 121 }
 122
 123
 124 void printConstraint(Constraint * This) {
 125         switch(This->type) {
 126         case TRUE:
 127                 model_print("true");
 128                 break;
 129         case FALSE:
 130                 model_print("false");
 131                 break;
 132         case IMPLIES:
 133                 model_print("(");
 134                 printConstraint(This->operands[0]);
 135                 model_print(")");
 136                 model_print("=>");
 137                 model_print("(");
 138                 printConstraint(This->operands[1]);
 139                 model_print(")");
 140                 break;
 141         case AND:
 142         case OR:
 143                 model_print("(");
 144                 for(uint i=0;i<This->numoperandsorvar;i++) {
 145                         if (i!=0) {
 146                                 if (This->type==AND)
 147                                         model_print(" ^ ");
 148                                 else
 149                                         model_print(" v ");
 150                         }
 151                         printConstraint(This->operands[i]);
 152                 }
 153                 model_print(")");
 154                 break;
 155         case VAR:
 156                 model_print("t%u",This->numoperandsorvar);
 157                 break;
 158         case NOTVAR:
 159                 model_print("!t%u",This->numoperandsorvar);
 160                 break;
 161         default:
 162                 ASSERT(0);
 163         }
 164 }
 165
 166 Constraint * cloneConstraint(Constraint * This) {
 167         switch(This->type) {
 168         case TRUE:
 169         case FALSE:
 170         case VAR:
 171         case NOTVAR:
 172                 return This;
 173         case IMPLIES:
 174                 return allocConstraint(IMPLIES, cloneConstraint(This->operands[0]), cloneConstraint(This->operands[1]));
 175         case AND:
 176         case OR: {
 177                 Constraint *array[This->numoperandsorvar];
 178                 for(uint i=0;i<This->numoperandsorvar;i++) {
 179                         array[i]=cloneConstraint(This->operands[i]);
 180                 }
 181                 return allocArrayConstraint(This->type, This->numoperandsorvar, array);
 182         }
 183         default:
 184                 ASSERT(0);
 185                 return NULL;
 186         }
 187 }
 188
 189 /** Generates a constraint to ensure that all encodings are less than value */
 190 Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value) {
 191         Constraint *orarray[numvars];
 192         Constraint *andarray[numvars];
 193         uint andi=0;
 194
 195         while(true) {
 196                 uint val=value;
 197                 uint ori=0;
 198                 for(uint j=0;j<numvars;j++) {
 199                         if ((val&1)==1)
 200                                 orarray[ori++]=negateConstraint(vars[j]);
 201                         val=val>>1;
 202                 }
 203                 //no ones to flip, so bail now...
 204                 if (ori==0) {
 205                         return allocArrayConstraint(AND, andi, andarray);
 206                 }
 207                 andarray[andi++]=allocArrayConstraint(OR, ori, orarray);
 208
 209                 value=value+(1<<(__builtin_ctz(value)));
 210                 //flip the last one
 211         }
 212 }
 213
 214 Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2) {
 215         if (numvars==0)
 216                 return &ctrue;
 217         Constraint *array[numvars*2];
 218         for(uint i=0;i<numvars;i++) {
 219                 array[i*2]=allocConstraint(OR, negateConstraint(cloneConstraint(var1[i])), var2[i]);
 220                 array[i*2+1]=allocConstraint(OR, var1[i], negateConstraint(cloneConstraint(var2[i])));
 221         }
 222         return allocArrayConstraint(AND, numvars*2, array);
 223 }
 224
 225 Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) {
 226         Constraint * imp1=allocConstraint(OR, negateConstraint(cloneConstraint(var1)), var2);
 227         Constraint * imp2=allocConstraint(OR, var1, negateConstraint(cloneConstraint(var2)));
 228
 229         return allocConstraint(AND, imp1, imp2);
 230 }
 231
 232 bool mergeandfree(VectorConstraint * to, VectorConstraint * from) {
 233         for(uint i=0;i<getSizeVectorConstraint(from);i++) {
 234                 Constraint *c=getVectorConstraint(from, i);
 235                 if (c->type==TRUE)
 236                         continue;
 237                 if (c->type==FALSE) {
 238                         for(uint j=i+1;j<getSizeVectorConstraint(from);j++)
 239                                 freerecConstraint(getVectorConstraint(from,j));
 240                         for(uint j=0;j<getSizeVectorConstraint(to);j++)
 241                                 freerecConstraint(getVectorConstraint(to, j));
 242                         clearVectorConstraint(to);
 243                         pushVectorConstraint(to, &ctrue);
 244                         deleteVectorConstraint(from);
 245                         return true;
 246                 }
 247                 pushVectorConstraint(to, c);
 248         }
 249         deleteVectorConstraint(from);
 250         return false;
 251 }
 252
 253 VectorConstraint * simplifyConstraint(Constraint * This) {
 254         switch(This->type) {
 255         case TRUE:
 256         case VAR:
 257         case NOTVAR:
 258         case FALSE: {
 259                 VectorConstraint * vec=allocDefVectorConstraint();
 260                 pushVectorConstraint(vec, This);
 261                 return vec;
 262         }
 263         case AND: {
 264                 VectorConstraint *vec=allocDefVectorConstraint();
 265                 for(uint i=0;i<This->numoperandsorvar;i++) {
 266                         VectorConstraint * subvec=simplifyConstraint(This->operands[i]);
 267                         if (mergeandfree(vec, subvec)) {
 268                                 for(uint j=i+1;j<This->numoperandsorvar;j++) {
 269                                         freerecConstraint(This->operands[j]);
 270                                 }
 271                                 internalfreeConstraint(This);
 272                                 return vec;
 273                         }
 274                 }
 275                 internalfreeConstraint(This);
 276                 return vec;
 277         }
 278         case OR: {
 279                 for(uint i=0;i<This->numoperandsorvar;i++) {
 280                         Constraint *c=This->operands[i];
 281                         switch(c->type) {
 282                         case TRUE: {
 283                                 VectorConstraint * vec=allocDefVectorConstraint();
 284                                 pushVectorConstraint(vec, c);
 285                                 freerecConstraint(This);
 286                                 return vec;
 287                         }
 288                         case FALSE: {
 289                                 Constraint *array[This->numoperandsorvar-1];
 290                                 uint index=0;
 291                                 for(uint j=0;j<This->numoperandsorvar;j++) {
 292                                         if (j!=i)
 293                                                 array[index++]=This->operands[j];
 294                                 }
 295                                 Constraint *cn=allocArrayConstraint(OR, index, array);
 296                                 VectorConstraint *vec=simplifyConstraint(cn);
 297                                 internalfreeConstraint(This);
 298                                 return vec;
 299                         }
 300                         case VAR:
 301                         case NOTVAR:
 302                                 break;
 303                         case OR: {
 304                                 uint nsize=This->numoperandsorvar+c->numoperandsorvar-1;
 305                                 Constraint *array[nsize];
 306                                 uint index=0;
 307                                 for(uint j=0;j<This->numoperandsorvar;j++)
 308                                         if (j!=i)
 309                                                 array[index++]=This->operands[j];
 310                                 for(uint j=0;j<c->numoperandsorvar;j++)
 311                                         array[index++]=c->operands[j];
 312                                 Constraint *cn=allocArrayConstraint(OR, nsize, array);
 313                                 VectorConstraint *vec=simplifyConstraint(cn);
 314                                 internalfreeConstraint(This);
 315                                 internalfreeConstraint(c);
 316                                 return vec;
 317                         }
 318                         case IMPLIES: {
 319                                 uint nsize=This->numoperandsorvar+1;
 320                                 Constraint *array[nsize];
 321                                 uint index=0;
 322                                 for(uint j=0;j<This->numoperandsorvar;j++)
 323                                         if (j!=i)
 324                                                 array[index++]=This->operands[j];
 325                                 array[index++]=negateConstraint(c->operands[0]);
 326                                 array[index++]=c->operands[1];
 327                                 Constraint *cn=allocArrayConstraint(OR, nsize, array);
 328                                 VectorConstraint *vec=simplifyConstraint(cn);
 329                                 internalfreeConstraint(This);
 330                                 internalfreeConstraint(c);
 331                                 return vec;
 332                         }
 333                         case AND: {
 334                                 Constraint *array[This->numoperandsorvar];
 335
 336                                 VectorConstraint *vec=allocDefVectorConstraint();
 337                                 for(uint j=0;j<c->numoperandsorvar;j++) {
 338                                         //copy other elements
 339                                         for(uint k=0;k<This->numoperandsorvar;k++) {
 340                                                 if (k!=i) {
 341                                                         array[k]=cloneConstraint(This->operands[k]);
 342                                                 }
 343                                         }
 344
 345                                         array[i]=cloneConstraint(c->operands[j]);
 346                                         Constraint *cn=allocArrayConstraint(OR, This->numoperandsorvar, array);
 347                                         VectorConstraint * newvec=simplifyConstraint(cn);
 348                                         if (mergeandfree(vec, newvec)) {
 349                                                 freerecConstraint(This);
 350                                                 return vec;
 351                                         }
 352                                 }
 353                                 freerecConstraint(This);
 354                                 return vec;
 355                         }
 356                         default:
 357                                 ASSERT(0);
 358                         }
 359                         //continue on to next item
 360                 }
 361                 VectorConstraint * vec=allocDefVectorConstraint();
 362                 if (This->numoperandsorvar==1) {
 363                         Constraint *c=This->operands[0];
 364                         freerecConstraint(This);
 365                         pushVectorConstraint(vec, c);
 366                 } else
 367                         pushVectorConstraint(vec, This);
 368                 return vec;
 369         }
 370         case IMPLIES: {
 371                 Constraint *cn=allocConstraint(OR, negateConstraint(This->operands[0]), This->operands[1]);
 372                 VectorConstraint * vec=simplifyConstraint(cn);
 373                 internalfreeConstraint(This);
 374                 return vec;
 375         }
 376         default:
 377                 ASSERT(0);
 378                 return NULL;
 379         }
 380 }
 381
 382 Constraint * negateConstraint(Constraint * This) {
 383         switch(This->type) {
 384         case TRUE:
 385                 return &cfalse;
 386         case FALSE:
 387                 return &ctrue;
 388         case NOTVAR:
 389         case VAR:
 390                 return This->neg;
 391         case IMPLIES: {
 392                 Constraint *l=This->operands[0];
 393                 Constraint *r=This->operands[1];
 394                 This->operands[0]=r;
 395                 This->operands[1]=l;
 396                 return This;
 397         }
 398         case AND:
 399         case OR: {
 400                 for(uint i=0;i<This->numoperandsorvar;i++) {
 401                         This->operands[i]=negateConstraint(This->operands[i]);
 402                 }
 403                 This->type=(This->type==AND) ? OR : AND;
 404                 return This;
 405         }
 406         default:
 407                 ASSERT(0);
 408                 return NULL;
 409         }
 410 }