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"
14 Constraint ctrue(TRUE);
15 Constraint cfalse(FALSE);
17 Constraint::Constraint(CType t, Constraint *l, Constraint *r) :
20 operands((Constraint **)model_malloc(2*sizeof(Constraint *))),
24 //if (type==IMPLIES) {
26 // operands[0]=l->negate();
33 Constraint::Constraint(CType t, Constraint *l) :
36 operands((Constraint **)model_malloc(sizeof(Constraint *))),
42 Constraint::Constraint(CType t, uint num, Constraint **array) :
44 numoperandsorvar(num),
45 operands((Constraint **)model_malloc(num*sizeof(Constraint *))),
48 memcpy(operands, array, num*sizeof(Constraint *));
51 Constraint::Constraint(CType t) :
53 numoperandsorvar(0xffffffff),
59 Constraint::Constraint(CType t, uint v) :
67 Constraint::~Constraint() {
72 void Constraint::printDIMACS(ConstGen *cg) {
74 cg->printConstraint(numoperandsorvar);
75 cg->printConstraint(0);
76 } else if (type==NOTVAR) {
77 cg->printNegConstraint(numoperandsorvar);
78 cg->printConstraint(0);
81 for(uint i=0;i<numoperandsorvar;i++) {
82 Constraint *c=operands[i];
84 cg->printConstraint(c->numoperandsorvar);
85 } else if (c->type==NOTVAR) {
86 cg->printNegConstraint(c->numoperandsorvar);
89 cg->printConstraint(0);
93 void Constraint::free() {
108 void Constraint::freerec() {
118 if (operands!=NULL) {
119 for(uint i=0;i<numoperandsorvar;i++)
120 operands[i]->freerec();
128 void Constraint::print() {
134 model_print("false");
138 operands[0]->print();
142 operands[1]->print();
148 for(uint i=0;i<numoperandsorvar;i++) {
155 operands[i]->print();
160 model_print("t%u",numoperandsorvar);
163 model_print("!t%u",numoperandsorvar);
170 Constraint * Constraint::clone() {
178 return new Constraint(IMPLIES, operands[0]->clone(), operands[1]->clone());
181 Constraint *array[numoperandsorvar];
182 for(uint i=0;i<numoperandsorvar;i++) {
183 array[i]=operands[i]->clone();
185 return new Constraint(type, numoperandsorvar, array);
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();
200 return new Constraint(AND, numvars, carray);
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];
212 for(uint j=0;j<numvars;j++) {
214 orarray[ori++]=vars[j]->negate();
217 //no ones to flip, so bail now...
219 return new Constraint(AND, andi, andarray);
221 andarray[andi++]=new Constraint(OR, ori, orarray);
223 value=value+(1<<(__builtin_ctz(value))); //flip the last one
227 Constraint * generateEquivConstraint(uint numvars, Constraint **var1, Constraint **var2) {
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());
235 return new Constraint(AND, numvars*2, array);
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());
242 return new Constraint(AND, imp1, imp2);
245 bool mergeandfree(ModelVector<Constraint *> * to, ModelVector<Constraint *> * from) {
246 for(uint i=0;i<from->size();i++) {
247 Constraint *c=(*from)[i];
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++)
256 to->push_back(&ctrue);
266 ModelVector<Constraint *> * Constraint::simplify() {
272 ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
273 vec->push_back(this);
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();
292 for(uint i=0;i<numoperandsorvar;i++) {
293 Constraint *c=operands[i];
296 ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
302 Constraint *array[numoperandsorvar-1];
304 for(uint j=0;j<numoperandsorvar;j++) {
306 array[index++]=operands[j];
308 Constraint *cn=new Constraint(OR, index, array);
309 ModelVector<Constraint *> *vec=cn->simplify();
317 uint nsize=numoperandsorvar+c->numoperandsorvar-1;
318 Constraint *array[nsize];
320 for(uint j=0;j<numoperandsorvar;j++)
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();
332 uint nsize=numoperandsorvar+1;
333 Constraint *array[nsize];
335 for(uint j=0;j<numoperandsorvar;j++)
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();
347 Constraint *array[numoperandsorvar];
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++) {
354 array[k]=operands[k]->clone();
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)) {
372 //continue on to next item
374 ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
375 if (numoperandsorvar==1) {
376 Constraint *c=operands[0];
380 vec->push_back(this);
384 Constraint *cn=new Constraint(OR, operands[0]->negate(), operands[1]);
385 ModelVector<Constraint *> *vec=cn->simplify();
395 Constraint * Constraint::negate() {
405 Constraint *l=operands[0];
406 Constraint *r=operands[1];
413 for(uint i=0;i<numoperandsorvar;i++) {
414 operands[i]=operands[i]->negate();
416 type=(type==AND) ? OR : AND;