src/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 "inc_solver.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::dumpConstraint(IncrementalSolver *solver) {
  73         if (type==VAR) {
  74                 solver->addClauseLiteral(numoperandsorvar);
  75                 solver->addClauseLiteral(0);
  76         } else if (type==NOTVAR) {
  77                 solver->addClauseLiteral(-numoperandsorvar);
  78                 solver->addClauseLiteral(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                                 solver->addClauseLiteral(c->numoperandsorvar);
  85                         } else if (c->type==NOTVAR) {
  86                                 solver->addClauseLiteral(-c->numoperandsorvar);
  87                         } else ASSERT(0);
  88                 }
  89                 solver->addClauseLiteral(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(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)));
 224                 //flip the last one
 225         }
 226 }
 227
 228 Constraint * generateEquivConstraint(uint numvars, Constraint **var1, Constraint **var2) {
 229         if (numvars==0)
 230                 return &ctrue;
 231         Constraint *array[numvars*2];
 232         for(uint i=0;i<numvars;i++) {
 233                 array[i*2]=new Constraint(OR, var1[i]->clone()->negate(), var2[i]);
 234                 array[i*2+1]=new Constraint(OR, var1[i], var2[i]->clone()->negate());
 235         }
 236         return new Constraint(AND, numvars*2, array);
 237 }
 238
 239 Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) {
 240         Constraint * imp1=new Constraint(OR, var1->clone()->negate(), var2);
 241         Constraint * imp2=new Constraint(OR, var1, var2->clone()->negate());
 242
 243         return new Constraint(AND, imp1, imp2);
 244 }
 245
 246 bool mergeandfree(ModelVector<Constraint *> * to, ModelVector<Constraint *> * from) {
 247         for(uint i=0;i<from->size();i++) {
 248                 Constraint *c=(*from)[i];
 249                 if (c->type==TRUE)
 250                         continue;
 251                 if (c->type==FALSE) {
 252                         for(uint j=i+1;j<from->size();j++)
 253                                 (*from)[j]->freerec();
 254                         for(uint j=0;j<to->size();j++)
 255                                 (*to)[j]->freerec();
 256                         to->clear();
 257                         to->push_back(&ctrue);
 258                         delete from;
 259                         return true;
 260                 }
 261                 to->push_back(c);
 262         }
 263         delete from;
 264         return false;
 265 }
 266
 267 ModelVector<Constraint *> * Constraint::simplify() {
 268         switch(type) {
 269         case TRUE:
 270         case VAR:
 271         case NOTVAR:
 272         case FALSE: {
 273                 ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
 274                 vec->push_back(this);
 275                 return vec;
 276         }
 277         case AND: {
 278                 ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
 279                 for(uint i=0;i<numoperandsorvar;i++) {
 280                         ModelVector<Constraint *> *subvec=operands[i]->simplify();
 281                         if (mergeandfree(vec, subvec)) {
 282                                 for(uint j=i+1;j<numoperandsorvar;j++) {
 283                                         operands[j]->freerec();
 284                                 }
 285                                 this->free();
 286                                 return vec;
 287                         }
 288                 }
 289                 this->free();
 290                 return vec;
 291         }
 292         case OR: {
 293                 for(uint i=0;i<numoperandsorvar;i++) {
 294                         Constraint *c=operands[i];
 295                         switch(c->type) {
 296                         case TRUE: {
 297                                 ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
 298                                 vec->push_back(c);
 299                                 this->freerec();
 300                                 return vec;
 301                         }
 302                         case FALSE: {
 303                                 Constraint *array[numoperandsorvar-1];
 304                                 uint index=0;
 305                                 for(uint j=0;j<numoperandsorvar;j++) {
 306                                         if (j!=i)
 307                                                 array[index++]=operands[j];
 308                                 }
 309                                 Constraint *cn=new Constraint(OR, index, array);
 310                                 ModelVector<Constraint *> *vec=cn->simplify();
 311                                 this->free();
 312                                 return vec;
 313                         }
 314                         case VAR:
 315                         case NOTVAR:
 316                                 break;
 317                         case OR: {
 318                                 uint nsize=numoperandsorvar+c->numoperandsorvar-1;
 319                                 Constraint *array[nsize];
 320                                 uint index=0;
 321                                 for(uint j=0;j<numoperandsorvar;j++)
 322                                         if (j!=i)
 323                                                 array[index++]=operands[j];
 324                                 for(uint j=0;j<c->numoperandsorvar;j++)
 325                                         array[index++]=c->operands[j];
 326                                 Constraint *cn=new Constraint(OR, nsize, array);
 327                                 ModelVector<Constraint *> *vec=cn->simplify();
 328                                 this->free();
 329                                 c->free();
 330                                 return vec;
 331                         }
 332                         case IMPLIES: {
 333                                 uint nsize=numoperandsorvar+1;
 334                                 Constraint *array[nsize];
 335                                 uint index=0;
 336                                 for(uint j=0;j<numoperandsorvar;j++)
 337                                         if (j!=i)
 338                                                 array[index++]=operands[j];
 339                                 array[index++]=c->operands[0]->negate();
 340                                 array[index++]=c->operands[1];
 341                                 Constraint *cn=new Constraint(OR, nsize, array);
 342                                 ModelVector<Constraint *> *vec=cn->simplify();
 343                                 this->free();
 344                                 c->free();
 345                                 return vec;
 346                         }
 347                         case AND: {
 348                                 Constraint *array[numoperandsorvar];
 349
 350                                 ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
 351                                 for(uint j=0;j<c->numoperandsorvar;j++) {
 352                                         //copy other elements
 353                                         for(uint k=0;k<numoperandsorvar;k++) {
 354                                                 if (k!=i) {
 355                                                         array[k]=operands[k]->clone();
 356                                                 }
 357                                         }
 358
 359                                         array[i]=c->operands[j]->clone();
 360                                         Constraint *cn=new Constraint(OR, numoperandsorvar, array);
 361                                         ModelVector<Constraint *> * newvec=cn->simplify();
 362                                         if (mergeandfree(vec, newvec)) {
 363                                                 this->freerec();
 364                                                 return vec;
 365                                         }
 366                                 }
 367                                 this->freerec();
 368                                 return vec;
 369                         }
 370                         default:
 371                                 ASSERT(0);
 372                         }
 373                         //continue on to next item
 374                 }
 375                 ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
 376                 if (numoperandsorvar==1) {
 377                         Constraint *c=operands[0];
 378                         this->freerec();
 379                         vec->push_back(c);
 380                 } else
 381                         vec->push_back(this);
 382                 return vec;
 383         }
 384         case IMPLIES: {
 385                 Constraint *cn=new Constraint(OR, operands[0]->negate(), operands[1]);
 386                 ModelVector<Constraint *> *vec=cn->simplify();
 387                 this->free();
 388                 return vec;
 389         }
 390         default:
 391                 ASSERT(0);
 392                 return NULL;
 393         }
 394 }
 395
 396 Constraint * Constraint::negate() {
 397         switch(type) {
 398         case TRUE:
 399                 return &cfalse;
 400         case FALSE:
 401                 return &ctrue;
 402         case NOTVAR:
 403         case VAR:
 404                 return this->neg;
 405         case IMPLIES: {
 406                 Constraint *l=operands[0];
 407                 Constraint *r=operands[1];
 408                 operands[0]=r;
 409                 operands[1]=l;
 410                 return this;
 411         }
 412         case AND:
 413         case OR: {
 414                 for(uint i=0;i<numoperandsorvar;i++) {
 415                         operands[i]=operands[i]->negate();
 416                 }
 417                 type=(type==AND) ? OR : AND;
 418                 return this;
 419         }
 420         default:
 421                 ASSERT(0);
 422                 return NULL;
 423         }
 424 }