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