1 /* Copyright (c) 2015 Regents of the University of California
3 * Author: Brian Demsky <bdemsky@uci.edu>
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.
10 #include "constraint.h"
12 #include "inc_solver.h"
14 Constraint ctrue={TRUE, 0xffffffff, NULL, NULL};
15 Constraint cfalse={FALSE, 0xffffffff, NULL, NULL};
17 Constraint * allocConstraint(CType t, Constraint *l, Constraint *r) {
18 Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
20 This->numoperandsorvar=2;
21 This->operands=(Constraint **)ourmalloc(2*sizeof(Constraint *));
24 //if (type==IMPLIES) {
26 // operands[0]=l->negate();
34 Constraint * allocUnaryConstraint(CType t, Constraint *l) {
35 Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
37 This->numoperandsorvar=1;
38 This->operands=(Constraint **) ourmalloc(sizeof(Constraint *));
44 Constraint * allocArrayConstraint(CType t, uint num, Constraint **array) {
45 Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
47 This->numoperandsorvar=num;
48 This->operands=(Constraint **) ourmalloc(num*sizeof(Constraint *));
50 memcpy(This->operands, array, num*sizeof(Constraint *));
54 Constraint * allocVarConstraint(CType t, uint v) {
55 Constraint *This=(Constraint *) ourmalloc(sizeof(Constraint));
57 This->numoperandsorvar=v;
63 void deleteConstraint(Constraint *This) {
64 if (This->operands!=NULL)
65 ourfree(This->operands);
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);
76 ASSERT(This->type==OR);
77 for(uint i=0;i<This->numoperandsorvar;i++) {
78 Constraint *c=This->operands[i];
80 addClauseLiteral(solver, c->numoperandsorvar);
81 } else if (c->type==NOTVAR) {
82 addClauseLiteral(solver, -c->numoperandsorvar);
85 addClauseLiteral(solver, 0);
89 void internalfreeConstraint(Constraint * This) {
104 void freerecConstraint(Constraint *This) {
114 if (This->operands!=NULL) {
115 for(uint i=0;i<This->numoperandsorvar;i++)
116 freerecConstraint(This->operands[i]);
119 deleteConstraint(This);
124 void printConstraint(Constraint * This) {
130 model_print("false");
134 printConstraint(This->operands[0]);
138 printConstraint(This->operands[1]);
144 for(uint i=0;i<This->numoperandsorvar;i++) {
151 printConstraint(This->operands[i]);
156 model_print("t%u",This->numoperandsorvar);
159 model_print("!t%u",This->numoperandsorvar);
166 Constraint * cloneConstraint(Constraint * This) {
174 return allocConstraint(IMPLIES, cloneConstraint(This->operands[0]), cloneConstraint(This->operands[1]));
177 Constraint *array[This->numoperandsorvar];
178 for(uint i=0;i<This->numoperandsorvar;i++) {
179 array[i]=cloneConstraint(This->operands[i]);
181 return allocArrayConstraint(This->type, This->numoperandsorvar, array);
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]);
196 return allocArrayConstraint(AND, numvars, carray);
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];
208 for(uint j=0;j<numvars;j++) {
210 orarray[ori++]=negateConstraint(vars[j]);
213 //no ones to flip, so bail now...
215 return allocArrayConstraint(AND, andi, andarray);
217 andarray[andi++]=allocArrayConstraint(OR, ori, orarray);
219 value=value+(1<<(__builtin_ctz(value)));
224 Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2) {
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])));
232 return allocArrayConstraint(AND, numvars*2, array);
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)));
239 return allocConstraint(AND, imp1, imp2);
242 bool mergeandfree(VectorConstraint * to, VectorConstraint * from) {
243 for(uint i=0;i<getSizeVectorConstraint(from);i++) {
244 Constraint *c=getVectorConstraint(from, i);
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);
257 pushVectorConstraint(to, c);
259 deleteVectorConstraint(from);
263 VectorConstraint * simplifyConstraint(Constraint * This) {
269 VectorConstraint * vec=allocDefVectorConstraint();
270 pushVectorConstraint(vec, This);
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]);
281 internalfreeConstraint(This);
285 internalfreeConstraint(This);
289 for(uint i=0;i<This->numoperandsorvar;i++) {
290 Constraint *c=This->operands[i];
293 VectorConstraint * vec=allocDefVectorConstraint();
294 pushVectorConstraint(vec, c);
295 freerecConstraint(This);
299 Constraint *array[This->numoperandsorvar-1];
301 for(uint j=0;j<This->numoperandsorvar;j++) {
303 array[index++]=This->operands[j];
305 Constraint *cn=allocArrayConstraint(OR, index, array);
306 VectorConstraint *vec=simplifyConstraint(cn);
307 internalfreeConstraint(This);
314 uint nsize=This->numoperandsorvar+c->numoperandsorvar-1;
315 Constraint *array[nsize];
317 for(uint j=0;j<This->numoperandsorvar;j++)
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);
329 uint nsize=This->numoperandsorvar+1;
330 Constraint *array[nsize];
332 for(uint j=0;j<This->numoperandsorvar;j++)
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);
344 Constraint *array[This->numoperandsorvar];
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++) {
351 array[k]=cloneConstraint(This->operands[k]);
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);
363 freerecConstraint(This);
369 //continue on to next item
371 VectorConstraint * vec=allocDefVectorConstraint();
372 if (This->numoperandsorvar==1) {
373 Constraint *c=This->operands[0];
374 freerecConstraint(This);
375 pushVectorConstraint(vec, c);
377 pushVectorConstraint(vec, This);
381 Constraint *cn=allocConstraint(OR, negateConstraint(This->operands[0]), This->operands[1]);
382 VectorConstraint * vec=simplifyConstraint(cn);
383 internalfreeConstraint(This);
392 Constraint * negateConstraint(Constraint * This) {
402 Constraint *l=This->operands[0];
403 Constraint *r=This->operands[1];
410 for(uint i=0;i<This->numoperandsorvar;i++) {
411 This->operands[i]=negateConstraint(This->operands[i]);
413 This->type=(This->type==AND) ? OR : AND;