Base Commit
[satune.git] / 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)));                                                                                                                                                                                                                                                //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 }