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                 model_print("In printingConstraint: %d", This->type);
 163                 ASSERT(0);
 164         }
 165 }
 166
 167 Constraint * cloneConstraint(Constraint * This) {
 168         switch(This->type) {
 169         case TRUE:
 170         case FALSE:
 171         case VAR:
 172         case NOTVAR:
 173                 return This;
 174         case IMPLIES:
 175                 return allocConstraint(IMPLIES, cloneConstraint(This->operands[0]), cloneConstraint(This->operands[1]));
 176         case AND:
 177         case OR: {
 178                 Constraint *array[This->numoperandsorvar];
 179                 for(uint i=0;i<This->numoperandsorvar;i++) {
 180                         array[i]=cloneConstraint(This->operands[i]);
 181                 }
 182                 return allocArrayConstraint(This->type, This->numoperandsorvar, array);
 183         }
 184         default:
 185                 ASSERT(0);
 186                 return NULL;
 187         }
 188 }
 189
 190 Constraint * generateBinaryConstraint(uint numvars, Constraint ** vars, uint value) {
 191         Constraint *carray[numvars];
 192         for(uint j=0;j<numvars;j++) {
 193                 carray[j]=((value&1)==1) ? vars[j] : negateConstraint(vars[j]);
 194                 value=value>>1;
 195         }
 196
 197         return allocArrayConstraint(AND, numvars, carray);
 198 }
 199
 200 /** Generates a constraint to ensure that all encodings are less than value */
 201 Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value) {
 202         Constraint *orarray[numvars];
 203         Constraint *andarray[numvars];
 204         uint andi=0;
 205
 206         while(true) {
 207                 uint val=value;
 208                 uint ori=0;
 209                 for(uint j=0;j<numvars;j++) {
 210                         if ((val&1)==1)
 211                                 orarray[ori++]=negateConstraint(vars[j]);
 212                         val=val>>1;
 213                 }
 214                 //no ones to flip, so bail now...
 215                 if (ori==0) {
 216                         return allocArrayConstraint(AND, andi, andarray);
 217                 }
 218                 andarray[andi++]=allocArrayConstraint(OR, ori, orarray);
 219
 220                 value=value+(1<<(__builtin_ctz(value)));
 221                 //flip the last one
 222         }
 223 }
 224
 225 Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2) {
 226         if (numvars==0)
 227                 return &ctrue;
 228         Constraint *array[numvars*2];
 229         for(uint i=0;i<numvars;i++) {
 230                 array[i*2]=allocConstraint(OR, negateConstraint(cloneConstraint(var1[i])), var2[i]);
 231                 array[i*2+1]=allocConstraint(OR, var1[i], negateConstraint(cloneConstraint(var2[i])));
 232         }
 233         return allocArrayConstraint(AND, numvars*2, array);
 234 }
 235
 236 Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) {
 237         Constraint * imp1=allocConstraint(OR, negateConstraint(cloneConstraint(var1)), var2);
 238         Constraint * imp2=allocConstraint(OR, var1, negateConstraint(cloneConstraint(var2)));
 239
 240         return allocConstraint(AND, imp1, imp2);
 241 }
 242
 243 bool mergeandfree(VectorConstraint * to, VectorConstraint * from) {
 244         for(uint i=0;i<getSizeVectorConstraint(from);i++) {
 245                 Constraint *c=getVectorConstraint(from, i);
 246                 if (c->type==TRUE)
 247                         continue;
 248                 if (c->type==FALSE) {
 249                         for(uint j=i+1;j<getSizeVectorConstraint(from);j++)
 250                                 freerecConstraint(getVectorConstraint(from,j));
 251                         for(uint j=0;j<getSizeVectorConstraint(to);j++)
 252                                 freerecConstraint(getVectorConstraint(to, j));
 253                         clearVectorConstraint(to);
 254                         pushVectorConstraint(to, &ctrue);
 255                         deleteVectorConstraint(from);
 256                         return true;
 257                 }
 258                 pushVectorConstraint(to, c);
 259         }
 260         deleteVectorConstraint(from);
 261         return false;
 262 }
 263
 264 VectorConstraint * simplifyConstraint(Constraint * This) {
 265         switch(This->type) {
 266         case TRUE:
 267         case VAR:
 268         case NOTVAR:
 269         case FALSE: {
 270                 VectorConstraint * vec=allocDefVectorConstraint();
 271                 pushVectorConstraint(vec, This);
 272                 return vec;
 273         }
 274         case AND: {
 275                 VectorConstraint *vec=allocDefVectorConstraint();
 276                 for(uint i=0;i<This->numoperandsorvar;i++) {
 277                         VectorConstraint * subvec=simplifyConstraint(This->operands[i]);
 278                         if (mergeandfree(vec, subvec)) {
 279                                 for(uint j=i+1;j<This->numoperandsorvar;j++) {
 280                                         freerecConstraint(This->operands[j]);
 281                                 }
 282                                 internalfreeConstraint(This);
 283                                 return vec;
 284                         }
 285                 }
 286                 internalfreeConstraint(This);
 287                 return vec;
 288         }
 289         case OR: {
 290                 for(uint i=0;i<This->numoperandsorvar;i++) {
 291                         Constraint *c=This->operands[i];
 292                         switch(c->type) {
 293                         case TRUE: {
 294                                 VectorConstraint * vec=allocDefVectorConstraint();
 295                                 pushVectorConstraint(vec, c);
 296                                 freerecConstraint(This);
 297                                 return vec;
 298                         }
 299                         case FALSE: {
 300                                 Constraint *array[This->numoperandsorvar-1];
 301                                 uint index=0;
 302                                 for(uint j=0;j<This->numoperandsorvar;j++) {
 303                                         if (j!=i)
 304                                                 array[index++]=This->operands[j];
 305                                 }
 306                                 Constraint *cn=allocArrayConstraint(OR, index, array);
 307                                 VectorConstraint *vec=simplifyConstraint(cn);
 308                                 internalfreeConstraint(This);
 309                                 return vec;
 310                         }
 311                         case VAR:
 312                         case NOTVAR:
 313                                 break;
 314                         case OR: {
 315                                 uint nsize=This->numoperandsorvar+c->numoperandsorvar-1;
 316                                 Constraint *array[nsize];
 317                                 uint index=0;
 318                                 for(uint j=0;j<This->numoperandsorvar;j++)
 319                                         if (j!=i)
 320                                                 array[index++]=This->operands[j];
 321                                 for(uint j=0;j<c->numoperandsorvar;j++)
 322                                         array[index++]=c->operands[j];
 323                                 Constraint *cn=allocArrayConstraint(OR, nsize, array);
 324                                 VectorConstraint *vec=simplifyConstraint(cn);
 325                                 internalfreeConstraint(This);
 326                                 internalfreeConstraint(c);
 327                                 return vec;
 328                         }
 329                         case IMPLIES: {
 330                                 uint nsize=This->numoperandsorvar+1;
 331                                 Constraint *array[nsize];
 332                                 uint index=0;
 333                                 for(uint j=0;j<This->numoperandsorvar;j++)
 334                                         if (j!=i)
 335                                                 array[index++]=This->operands[j];
 336                                 array[index++]=negateConstraint(c->operands[0]);
 337                                 array[index++]=c->operands[1];
 338                                 Constraint *cn=allocArrayConstraint(OR, nsize, array);
 339                                 VectorConstraint *vec=simplifyConstraint(cn);
 340                                 internalfreeConstraint(This);
 341                                 internalfreeConstraint(c);
 342                                 return vec;
 343                         }
 344                         case AND: {
 345                                 Constraint *array[This->numoperandsorvar];
 346
 347                                 VectorConstraint *vec=allocDefVectorConstraint();
 348                                 for(uint j=0;j<c->numoperandsorvar;j++) {
 349                                         //copy other elements
 350                                         for(uint k=0;k<This->numoperandsorvar;k++) {
 351                                                 if (k!=i) {
 352                                                         array[k]=cloneConstraint(This->operands[k]);
 353                                                 }
 354                                         }
 355
 356                                         array[i]=cloneConstraint(c->operands[j]);
 357                                         Constraint *cn=allocArrayConstraint(OR, This->numoperandsorvar, array);
 358                                         VectorConstraint * newvec=simplifyConstraint(cn);
 359                                         if (mergeandfree(vec, newvec)) {
 360                                                 freerecConstraint(This);
 361                                                 return vec;
 362                                         }
 363                                 }
 364                                 freerecConstraint(This);
 365                                 return vec;
 366                         }
 367                         default:
 368                                 ASSERT(0);
 369                         }
 370                         //continue on to next item
 371                 }
 372                 VectorConstraint * vec=allocDefVectorConstraint();
 373                 if (This->numoperandsorvar==1) {
 374                         Constraint *c=This->operands[0];
 375                         freerecConstraint(This);
 376                         pushVectorConstraint(vec, c);
 377                 } else
 378                         pushVectorConstraint(vec, This);
 379                 return vec;
 380         }
 381         case IMPLIES: {
 382                 Constraint *cn=allocConstraint(OR, negateConstraint(This->operands[0]), This->operands[1]);
 383                 VectorConstraint * vec=simplifyConstraint(cn);
 384                 internalfreeConstraint(This);
 385                 return vec;
 386         }
 387         default:
 388                 ASSERT(0);
 389                 return NULL;
 390         }
 391 }
 392
 393 Constraint * negateConstraint(Constraint * This) {
 394         switch(This->type) {
 395         case TRUE:
 396                 return &cfalse;
 397         case FALSE:
 398                 return &ctrue;
 399         case NOTVAR:
 400         case VAR:
 401                 return This->neg;
 402         case IMPLIES: {
 403                 Constraint *l=This->operands[0];
 404                 Constraint *r=This->operands[1];
 405                 This->operands[0]=r;
 406                 This->operands[1]=l;
 407                 return This;
 408         }
 409         case AND:
 410         case OR: {
 411                 for(uint i=0;i<This->numoperandsorvar;i++) {
 412                         This->operands[i]=negateConstraint(This->operands[i]);
 413                 }
 414                 This->type=(This->type==AND) ? OR : AND;
 415                 return This;
 416         }
 417         default:
 418                 ASSERT(0);
 419                 return NULL;
 420         }
 421 }