commit after resolving conflicts
[satune.git] / 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 }