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);
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::dumpConstraint(IncrementalSolver *solver) {
74 solver->addClauseLiteral(numoperandsorvar);
75 solver->addClauseLiteral(0);
76 } else if (type==NOTVAR) {
77 solver->addClauseLiteral(-numoperandsorvar);
78 solver->addClauseLiteral(0);
81 for(uint i=0;i<numoperandsorvar;i++) {
82 Constraint *c=operands[i];
84 solver->addClauseLiteral(c->numoperandsorvar);
85 } else if (c->type==NOTVAR) {
86 solver->addClauseLiteral(-c->numoperandsorvar);
89 solver->addClauseLiteral(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(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)));
228 Constraint * generateEquivConstraint(uint numvars, Constraint **var1, Constraint **var2) {
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());
236 return new Constraint(AND, numvars*2, array);
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());
243 return new Constraint(AND, imp1, imp2);
246 bool mergeandfree(ModelVector<Constraint *> * to, ModelVector<Constraint *> * from) {
247 for(uint i=0;i<from->size();i++) {
248 Constraint *c=(*from)[i];
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++)
257 to->push_back(&ctrue);
267 ModelVector<Constraint *> * Constraint::simplify() {
273 ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
274 vec->push_back(this);
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();
293 for(uint i=0;i<numoperandsorvar;i++) {
294 Constraint *c=operands[i];
297 ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
303 Constraint *array[numoperandsorvar-1];
305 for(uint j=0;j<numoperandsorvar;j++) {
307 array[index++]=operands[j];
309 Constraint *cn=new Constraint(OR, index, array);
310 ModelVector<Constraint *> *vec=cn->simplify();
318 uint nsize=numoperandsorvar+c->numoperandsorvar-1;
319 Constraint *array[nsize];
321 for(uint j=0;j<numoperandsorvar;j++)
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();
333 uint nsize=numoperandsorvar+1;
334 Constraint *array[nsize];
336 for(uint j=0;j<numoperandsorvar;j++)
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();
348 Constraint *array[numoperandsorvar];
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++) {
355 array[k]=operands[k]->clone();
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)) {
373 //continue on to next item
375 ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
376 if (numoperandsorvar==1) {
377 Constraint *c=operands[0];
381 vec->push_back(this);
385 Constraint *cn=new Constraint(OR, operands[0]->negate(), operands[1]);
386 ModelVector<Constraint *> *vec=cn->simplify();
396 Constraint * Constraint::negate() {
406 Constraint *l=operands[0];
407 Constraint *r=operands[1];
414 for(uint i=0;i<numoperandsorvar;i++) {
415 operands[i]=operands[i]->negate();
417 type=(type==AND) ? OR : AND;