constraint.cc

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