#include "constraint.h"
#include "mymemory.h"
-#include "inc_solver.h"
+//#include "inc_solver.h"
-Constraint ctrue(TRUE);
-Constraint cfalse(FALSE);
+Constraint ctrue={TRUE, 0xffffffff, NULL, NULL};
+Constraint cfalse={FALSE, 0xffffffff, NULL, NULL};
-Constraint::Constraint(CType t, Constraint *l, Constraint *r) :
- type(t),
- numoperandsorvar(2),
- operands((Constraint **)model_malloc(2*sizeof(Constraint *))),
- neg(NULL)
-{
+Constraint * allocConstraint(CType t, Constraint *l, Constraint *r) {
+ Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint));
+ this->type=t;
+ this->numoperandsorvar=2;
+ this->operands=(Constraint **)ourmalloc(2*sizeof(Constraint *));
+ this->neg=NULL;
ASSERT(l!=NULL);
//if (type==IMPLIES) {
//type=OR;
// operands[0]=l->negate();
// } else {
- operands[0]=l;
+ this->operands[0]=l;
// }
- operands[1]=r;
+ this->operands[1]=r;
+ return this;
}
-Constraint::Constraint(CType t, Constraint *l) :
- type(t),
- numoperandsorvar(1),
- operands((Constraint **)model_malloc(sizeof(Constraint *))),
- neg(NULL)
-{
- operands[0]=l;
+Constraint * allocUnaryConstraint(CType t, Constraint *l) {
+ Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint));
+ this->type=t;
+ this->numoperandsorvar=1;
+ this->operands=(Constraint **) ourmalloc(sizeof(Constraint *));
+ this->neg=NULL;
+ this->operands[0]=l;
+ return this;
}
-Constraint::Constraint(CType t, uint num, Constraint **array) :
- type(t),
- numoperandsorvar(num),
- operands((Constraint **)model_malloc(num*sizeof(Constraint *))),
- neg(NULL)
-{
- memcpy(operands, array, num*sizeof(Constraint *));
+Constraint * allocArrayConstraint(CType t, uint num, Constraint **array) {
+ Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint));
+ this->type=t;
+ this->numoperandsorvar=num;
+ this->operands=(Constraint **) ourmalloc(num*sizeof(Constraint *));
+ this->neg=NULL;
+ memcpy(this->operands, array, num*sizeof(Constraint *));
+ return this;
}
-Constraint::Constraint(CType t) :
- type(t),
- numoperandsorvar(0xffffffff),
- operands(NULL),
- neg(NULL)
-{
+Constraint * allocVarConstraint(CType t, uint v) {
+ Constraint *this=(Constraint *) ourmalloc(sizeof(Constraint));
+ this->type=t;
+ this->numoperandsorvar=v;
+ this->operands=NULL;
+ this->neg=NULL;
+ return this;
}
-Constraint::Constraint(CType t, uint v) :
- type(t),
- numoperandsorvar(v),
- operands(NULL),
- neg(NULL)
-{
+void freeConstraint(Constraint *this) {
+ if (this->operands!=NULL)
+ ourfree(this->operands);
}
-Constraint::~Constraint() {
- if (operands!=NULL)
- model_free(operands);
-}
-
-void Constraint::dumpConstraint(IncrementalSolver *solver) {
- if (type==VAR) {
- solver->addClauseLiteral(numoperandsorvar);
+/*void dumpConstraint(Constraint * this, IncrementalSolver *solver) {
+ if (this->type==VAR) {
+ solver->addClauseLiteral(this->numoperandsorvar);
solver->addClauseLiteral(0);
- } else if (type==NOTVAR) {
- solver->addClauseLiteral(-numoperandsorvar);
+ } else if (this->type==NOTVAR) {
+ solver->addClauseLiteral(-this->numoperandsorvar);
solver->addClauseLiteral(0);
} else {
- ASSERT(type==OR);
- for(uint i=0;i<numoperandsorvar;i++) {
- Constraint *c=operands[i];
+ ASSERT(this->type==OR);
+ for(uint i=0;i<this->numoperandsorvar;i++) {
+ Constraint *c=this->operands[i];
if (c->type==VAR) {
solver->addClauseLiteral(c->numoperandsorvar);
} else if (c->type==NOTVAR) {
}
solver->addClauseLiteral(0);
}
-}
+ }*/
-void Constraint::free() {
- switch(type) {
+void internalfreeConstraint(Constraint * this) {
+ switch(this->type) {
case TRUE:
case FALSE:
case NOTVAR:
case BOGUS:
ASSERT(0);
default:
- type=BOGUS;
- delete this;
+ this->type=BOGUS;
+ ourfree(this);
}
}
-void Constraint::freerec() {
- switch(type) {
+void freerecConstraint(Constraint *this) {
+ switch(this->type) {
case TRUE:
case FALSE:
case NOTVAR:
case BOGUS:
ASSERT(0);
default:
- if (operands!=NULL) {
- for(uint i=0;i<numoperandsorvar;i++)
- operands[i]->freerec();
+ if (this->operands!=NULL) {
+ for(uint i=0;i<this->numoperandsorvar;i++)
+ freerecConstraint(this->operands[i]);
}
- type=BOGUS;
- delete this;
+ this->type=BOGUS;
+ freeConstraint(this);
}
}
-void Constraint::print() {
- switch(type) {
+void printConstraint(Constraint * this) {
+ switch(this->type) {
case TRUE:
model_print("true");
break;
break;
case IMPLIES:
model_print("(");
- operands[0]->print();
+ printConstraint(this->operands[0]);
model_print(")");
model_print("=>");
model_print("(");
- operands[1]->print();
+ printConstraint(this->operands[1]);
model_print(")");
break;
case AND:
case OR:
model_print("(");
- for(uint i=0;i<numoperandsorvar;i++) {
+ for(uint i=0;i<this->numoperandsorvar;i++) {
if (i!=0) {
- if (type==AND)
+ if (this->type==AND)
model_print(" ^ ");
else
model_print(" v ");
}
- operands[i]->print();
+ printConstraint(this->operands[i]);
}
model_print(")");
break;
case VAR:
- model_print("t%u",numoperandsorvar);
+ model_print("t%u",this->numoperandsorvar);
break;
case NOTVAR:
- model_print("!t%u",numoperandsorvar);
+ model_print("!t%u",this->numoperandsorvar);
break;
default:
ASSERT(0);
}
}
-Constraint * Constraint::clone() {
- switch(type) {
+Constraint * cloneConstraint(Constraint * this) {
+ switch(this->type) {
case TRUE:
case FALSE:
case VAR:
case NOTVAR:
return this;
case IMPLIES:
- return new Constraint(IMPLIES, operands[0]->clone(), operands[1]->clone());
+ return allocConstraint(IMPLIES, cloneConstraint(this->operands[0]), cloneConstraint(this->operands[1]));
case AND:
case OR: {
- Constraint *array[numoperandsorvar];
- for(uint i=0;i<numoperandsorvar;i++) {
- array[i]=operands[i]->clone();
+ Constraint *array[this->numoperandsorvar];
+ for(uint i=0;i<this->numoperandsorvar;i++) {
+ array[i]=cloneConstraint(this->operands[i]);
}
- return new Constraint(type, numoperandsorvar, array);
+ return allocArrayConstraint(this->type, this->numoperandsorvar, array);
}
default:
ASSERT(0);
Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value) {
Constraint *carray[numvars];
for(uint j=0;j<numvars;j++) {
- carray[j]=((value&1)==1) ? vars[j] : vars[j]->negate();
+ carray[j]=((value&1)==1) ? vars[j] : negateConstraint(vars[j]);
value=value>>1;
}
- return new Constraint(AND, numvars, carray);
+ return allocArrayConstraint(AND, numvars, carray);
}
/** Generates a constraint to ensure that all encodings are less than value */
uint ori=0;
for(uint j=0;j<numvars;j++) {
if ((val&1)==1)
- orarray[ori++]=vars[j]->negate();
+ orarray[ori++]=negateConstraint(vars[j]);
val=val>>1;
}
//no ones to flip, so bail now...
if (ori==0) {
- return new Constraint(AND, andi, andarray);
+ return allocArrayConstraint(AND, andi, andarray);
}
- andarray[andi++]=new Constraint(OR, ori, orarray);
+ andarray[andi++]=allocArrayConstraint(OR, ori, orarray);
value=value+(1<<(__builtin_ctz(value)));
//flip the last one
}
}
-Constraint * generateEquivConstraint(uint numvars, Constraint **var1, Constraint **var2) {
+Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2) {
if (numvars==0)
return &ctrue;
Constraint *array[numvars*2];
for(uint i=0;i<numvars;i++) {
- array[i*2]=new Constraint(OR, var1[i]->clone()->negate(), var2[i]);
- array[i*2+1]=new Constraint(OR, var1[i], var2[i]->clone()->negate());
+ array[i*2]=allocConstraint(OR, negateConstraint(cloneConstraint(var1[i])), var2[i]);
+ array[i*2+1]=allocConstraint(OR, var1[i], negateConstraint(cloneConstraint(var2[i])));
}
- return new Constraint(AND, numvars*2, array);
+ return allocArrayConstraint(AND, numvars*2, array);
}
Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2) {
- Constraint * imp1=new Constraint(OR, var1->clone()->negate(), var2);
- Constraint * imp2=new Constraint(OR, var1, var2->clone()->negate());
-
- return new Constraint(AND, imp1, imp2);
+ Constraint * imp1=allocConstraint(OR, negateConstraint(cloneConstraint(var1)), var2);
+ Constraint * imp2=allocConstraint(OR, var1, negateConstraint(cloneConstraint(var2)));
+
+ return allocConstraint(AND, imp1, imp2);
}
-bool mergeandfree(ModelVector<Constraint *> * to, ModelVector<Constraint *> * from) {
- for(uint i=0;i<from->size();i++) {
- Constraint *c=(*from)[i];
+bool mergeandfree(VectorConstraint * to, VectorConstraint * from) {
+ for(uint i=0;i<getSizeVectorConstraint(from);i++) {
+ Constraint *c=getVectorConstraint(from, i);
if (c->type==TRUE)
continue;
if (c->type==FALSE) {
- for(uint j=i+1;j<from->size();j++)
- (*from)[j]->freerec();
- for(uint j=0;j<to->size();j++)
- (*to)[j]->freerec();
- to->clear();
- to->push_back(&ctrue);
- delete from;
+ for(uint j=i+1;j<getSizeVectorConstraint(from);j++)
+ freerecConstraint(getVectorConstraint(from,j));
+ for(uint j=0;j<getSizeVectorConstraint(to);j++)
+ freerecConstraint(getVectorConstraint(to, j));
+ clearVectorConstraint(to);
+ pushVectorConstraint(to, &ctrue);
+ freeVectorConstraint(from);
return true;
}
- to->push_back(c);
+ pushVectorConstraint(to, c);
}
- delete from;
+ freeVectorConstraint(from);
return false;
}
-ModelVector<Constraint *> * Constraint::simplify() {
- switch(type) {
+VectorConstraint * simplifyConstraint(Constraint * this) {
+ switch(this->type) {
case TRUE:
case VAR:
case NOTVAR:
case FALSE: {
- ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
- vec->push_back(this);
+ VectorConstraint * vec=allocDefVectorConstraint();
+ pushVectorConstraint(vec, this);
return vec;
}
case AND: {
- ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
- for(uint i=0;i<numoperandsorvar;i++) {
- ModelVector<Constraint *> *subvec=operands[i]->simplify();
+ VectorConstraint *vec=allocDefVectorConstraint();
+ for(uint i=0;i<this->numoperandsorvar;i++) {
+ VectorConstraint * subvec=simplifyConstraint(this->operands[i]);
if (mergeandfree(vec, subvec)) {
- for(uint j=i+1;j<numoperandsorvar;j++) {
- operands[j]->freerec();
+ for(uint j=i+1;j<this->numoperandsorvar;j++) {
+ freerecConstraint(this->operands[j]);
}
- this->free();
+ internalfreeConstraint(this);
return vec;
}
}
- this->free();
+ internalfreeConstraint(this);
return vec;
}
case OR: {
- for(uint i=0;i<numoperandsorvar;i++) {
- Constraint *c=operands[i];
+ for(uint i=0;i<this->numoperandsorvar;i++) {
+ Constraint *c=this->operands[i];
switch(c->type) {
case TRUE: {
- ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
- vec->push_back(c);
- this->freerec();
+ VectorConstraint * vec=allocDefVectorConstraint();
+ pushVectorConstraint(vec, c);
+ freerecConstraint(this);
return vec;
}
case FALSE: {
- Constraint *array[numoperandsorvar-1];
+ Constraint *array[this->numoperandsorvar-1];
uint index=0;
- for(uint j=0;j<numoperandsorvar;j++) {
+ for(uint j=0;j<this->numoperandsorvar;j++) {
if (j!=i)
- array[index++]=operands[j];
+ array[index++]=this->operands[j];
}
- Constraint *cn=new Constraint(OR, index, array);
- ModelVector<Constraint *> *vec=cn->simplify();
- this->free();
+ Constraint *cn=allocArrayConstraint(OR, index, array);
+ VectorConstraint *vec=simplifyConstraint(cn);
+ internalfreeConstraint(this);
return vec;
}
case VAR:
case NOTVAR:
break;
case OR: {
- uint nsize=numoperandsorvar+c->numoperandsorvar-1;
+ uint nsize=this->numoperandsorvar+c->numoperandsorvar-1;
Constraint *array[nsize];
uint index=0;
- for(uint j=0;j<numoperandsorvar;j++)
+ for(uint j=0;j<this->numoperandsorvar;j++)
if (j!=i)
- array[index++]=operands[j];
+ array[index++]=this->operands[j];
for(uint j=0;j<c->numoperandsorvar;j++)
array[index++]=c->operands[j];
- Constraint *cn=new Constraint(OR, nsize, array);
- ModelVector<Constraint *> *vec=cn->simplify();
- this->free();
- c->free();
+ Constraint *cn=allocArrayConstraint(OR, nsize, array);
+ VectorConstraint *vec=simplifyConstraint(cn);
+ internalfreeConstraint(this);
+ internalfreeConstraint(c);
return vec;
}
case IMPLIES: {
- uint nsize=numoperandsorvar+1;
+ uint nsize=this->numoperandsorvar+1;
Constraint *array[nsize];
uint index=0;
- for(uint j=0;j<numoperandsorvar;j++)
+ for(uint j=0;j<this->numoperandsorvar;j++)
if (j!=i)
- array[index++]=operands[j];
- array[index++]=c->operands[0]->negate();
+ array[index++]=this->operands[j];
+ array[index++]=negateConstraint(c->operands[0]);
array[index++]=c->operands[1];
- Constraint *cn=new Constraint(OR, nsize, array);
- ModelVector<Constraint *> *vec=cn->simplify();
- this->free();
- c->free();
+ Constraint *cn=allocArrayConstraint(OR, nsize, array);
+ VectorConstraint *vec=simplifyConstraint(cn);
+ internalfreeConstraint(this);
+ internalfreeConstraint(c);
return vec;
}
case AND: {
- Constraint *array[numoperandsorvar];
+ Constraint *array[this->numoperandsorvar];
- ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
+ VectorConstraint *vec=allocDefVectorConstraint();
for(uint j=0;j<c->numoperandsorvar;j++) {
//copy other elements
- for(uint k=0;k<numoperandsorvar;k++) {
+ for(uint k=0;k<this->numoperandsorvar;k++) {
if (k!=i) {
- array[k]=operands[k]->clone();
+ array[k]=cloneConstraint(this->operands[k]);
}
}
- array[i]=c->operands[j]->clone();
- Constraint *cn=new Constraint(OR, numoperandsorvar, array);
- ModelVector<Constraint *> * newvec=cn->simplify();
+ array[i]=cloneConstraint(c->operands[j]);
+ Constraint *cn=allocArrayConstraint(OR, this->numoperandsorvar, array);
+ VectorConstraint * newvec=simplifyConstraint(cn);
if (mergeandfree(vec, newvec)) {
- this->freerec();
+ freerecConstraint(this);
return vec;
}
}
- this->freerec();
+ freerecConstraint(this);
return vec;
}
default:
}
//continue on to next item
}
- ModelVector<Constraint *> *vec=new ModelVector<Constraint *>();
- if (numoperandsorvar==1) {
- Constraint *c=operands[0];
- this->freerec();
- vec->push_back(c);
+ VectorConstraint * vec=allocDefVectorConstraint();
+ if (this->numoperandsorvar==1) {
+ Constraint *c=this->operands[0];
+ freerecConstraint(this);
+ pushVectorConstraint(vec, c);
} else
- vec->push_back(this);
+ pushVectorConstraint(vec, this);
return vec;
}
case IMPLIES: {
- Constraint *cn=new Constraint(OR, operands[0]->negate(), operands[1]);
- ModelVector<Constraint *> *vec=cn->simplify();
- this->free();
+ Constraint *cn=allocConstraint(OR, negateConstraint(this->operands[0]), this->operands[1]);
+ VectorConstraint * vec=simplifyConstraint(cn);
+ internalfreeConstraint(this);
return vec;
}
default:
}
}
-Constraint * Constraint::negate() {
- switch(type) {
+Constraint * negateConstraint(Constraint * this) {
+ switch(this->type) {
case TRUE:
return &cfalse;
case FALSE:
case VAR:
return this->neg;
case IMPLIES: {
- Constraint *l=operands[0];
- Constraint *r=operands[1];
- operands[0]=r;
- operands[1]=l;
+ Constraint *l=this->operands[0];
+ Constraint *r=this->operands[1];
+ this->operands[0]=r;
+ this->operands[1]=l;
return this;
}
case AND:
case OR: {
- for(uint i=0;i<numoperandsorvar;i++) {
- operands[i]=operands[i]->negate();
+ for(uint i=0;i<this->numoperandsorvar;i++) {
+ this->operands[i]=negateConstraint(this->operands[i]);
}
- type=(type==AND) ? OR : AND;
+ this->type=(this->type==AND) ? OR : AND;
return this;
}
default:
projects / satune.git / blobdiff