From: bdemsky Date: Thu, 15 Jun 2017 04:41:13 +0000 (-0700) Subject: Convert constraint.c to C X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=f122ce0ab001618fb4936f179df1f560c7f9e63f;p=satune.git Convert constraint.c to C --- diff --git a/src/Makefile b/src/Makefile index 5694fe2..c9d2612 100644 --- a/src/Makefile +++ b/src/Makefile @@ -4,7 +4,7 @@ PHONY += directories MKDIR_P = mkdir -p OBJ_DIR = bin -C_SOURCES := set.c mutableset.c element.c function.c order.c table.c predicate.c boolean.c csolver.c structs.c +C_SOURCES := set.c mutableset.c element.c function.c order.c table.c predicate.c boolean.c csolver.c structs.c constraint.c OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o) diff --git a/src/constraint.c b/src/constraint.c index c8a622a..be7c73c 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -9,77 +9,73 @@ #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;itype==OR); + for(uint i=0;inumoperandsorvar;i++) { + Constraint *c=this->operands[i]; if (c->type==VAR) { solver->addClauseLiteral(c->numoperandsorvar); } else if (c->type==NOTVAR) { @@ -88,10 +84,10 @@ void Constraint::dumpConstraint(IncrementalSolver *solver) { } solver->addClauseLiteral(0); } -} + }*/ -void Constraint::free() { - switch(type) { +void internalfreeConstraint(Constraint * this) { + switch(this->type) { case TRUE: case FALSE: case NOTVAR: @@ -100,13 +96,13 @@ void Constraint::free() { 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: @@ -115,18 +111,18 @@ void Constraint::freerec() { case BOGUS: ASSERT(0); default: - if (operands!=NULL) { - for(uint i=0;ifreerec(); + if (this->operands!=NULL) { + for(uint i=0;inumoperandsorvar;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; @@ -135,54 +131,54 @@ void Constraint::print() { 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;inumoperandsorvar;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;iclone(); + Constraint *array[this->numoperandsorvar]; + for(uint i=0;inumoperandsorvar;i++) { + array[i]=cloneConstraint(this->operands[i]); } - return new Constraint(type, numoperandsorvar, array); + return allocArrayConstraint(this->type, this->numoperandsorvar, array); } default: ASSERT(0); @@ -193,11 +189,11 @@ Constraint * Constraint::clone() { Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value) { Constraint *carray[numvars]; for(uint j=0;jnegate(); + 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 */ @@ -211,160 +207,160 @@ Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value) uint ori=0; for(uint j=0;jnegate(); + 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;iclone()->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 * to, ModelVector * from) { - for(uint i=0;isize();i++) { - Constraint *c=(*from)[i]; +bool mergeandfree(VectorConstraint * to, VectorConstraint * from) { + for(uint i=0;itype==TRUE) continue; if (c->type==FALSE) { - for(uint j=i+1;jsize();j++) - (*from)[j]->freerec(); - for(uint j=0;jsize();j++) - (*to)[j]->freerec(); - to->clear(); - to->push_back(&ctrue); - delete from; + for(uint j=i+1;jpush_back(c); + pushVectorConstraint(to, c); } - delete from; + freeVectorConstraint(from); return false; } -ModelVector * Constraint::simplify() { - switch(type) { +VectorConstraint * simplifyConstraint(Constraint * this) { + switch(this->type) { case TRUE: case VAR: case NOTVAR: case FALSE: { - ModelVector *vec=new ModelVector(); - vec->push_back(this); + VectorConstraint * vec=allocDefVectorConstraint(); + pushVectorConstraint(vec, this); return vec; } case AND: { - ModelVector *vec=new ModelVector(); - for(uint i=0;i *subvec=operands[i]->simplify(); + VectorConstraint *vec=allocDefVectorConstraint(); + for(uint i=0;inumoperandsorvar;i++) { + VectorConstraint * subvec=simplifyConstraint(this->operands[i]); if (mergeandfree(vec, subvec)) { - for(uint j=i+1;jfreerec(); + for(uint j=i+1;jnumoperandsorvar;j++) { + freerecConstraint(this->operands[j]); } - this->free(); + internalfreeConstraint(this); return vec; } } - this->free(); + internalfreeConstraint(this); return vec; } case OR: { - for(uint i=0;inumoperandsorvar;i++) { + Constraint *c=this->operands[i]; switch(c->type) { case TRUE: { - ModelVector *vec=new ModelVector(); - 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;jnumoperandsorvar;j++) { if (j!=i) - array[index++]=operands[j]; + array[index++]=this->operands[j]; } - Constraint *cn=new Constraint(OR, index, array); - ModelVector *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;jnumoperandsorvar;j++) if (j!=i) - array[index++]=operands[j]; + array[index++]=this->operands[j]; for(uint j=0;jnumoperandsorvar;j++) array[index++]=c->operands[j]; - Constraint *cn=new Constraint(OR, nsize, array); - ModelVector *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;jnumoperandsorvar;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 *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 *vec=new ModelVector(); + VectorConstraint *vec=allocDefVectorConstraint(); for(uint j=0;jnumoperandsorvar;j++) { //copy other elements - for(uint k=0;knumoperandsorvar;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 * 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: @@ -372,19 +368,19 @@ ModelVector * Constraint::simplify() { } //continue on to next item } - ModelVector *vec=new ModelVector(); - 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 *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: @@ -393,8 +389,8 @@ ModelVector * Constraint::simplify() { } } -Constraint * Constraint::negate() { - switch(type) { +Constraint * negateConstraint(Constraint * this) { + switch(this->type) { case TRUE: return &cfalse; case FALSE: @@ -403,18 +399,18 @@ Constraint * Constraint::negate() { 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;inegate(); + for(uint i=0;inumoperandsorvar;i++) { + this->operands[i]=negateConstraint(this->operands[i]); } - type=(type==AND) ? OR : AND; + this->type=(this->type==AND) ? OR : AND; return this; } default: diff --git a/src/constraint.h b/src/constraint.h index f6b1695..9f555d4 100644 --- a/src/constraint.h +++ b/src/constraint.h @@ -10,7 +10,7 @@ #ifndef CONSTRAINT_H #define CONSTRAINT_H #include "classlist.h" -#include "stl-model.h" +#include "structs.h" enum ConstraintType { TRUE, FALSE, IMPLIES, AND, OR, VAR, NOTVAR, BOGUS @@ -18,41 +18,37 @@ enum ConstraintType { typedef enum ConstraintType CType; -class Constraint { -public: - Constraint(CType t, Constraint *l, Constraint *r); - Constraint(CType t, Constraint *l); - Constraint(CType t, uint num, Constraint ** array); - Constraint(CType t, uint var); - Constraint(CType t); - ~Constraint(); - void print(); - void dumpConstraint(IncrementalSolver *solver); - uint getVar() {ASSERT(type==VAR); return numoperandsorvar;} - ModelVector * simplify(); - CType getType() {return type;} - bool isFalse() {return type==FALSE;} - bool isTrue() {return type==TRUE;} - void free(); - void freerec(); - Constraint * clone(); - void setNeg(Constraint *c) {neg=c;} - Constraint *negate(); - - MEMALLOC; -private: +struct Constraint { CType type; uint numoperandsorvar; Constraint ** operands; Constraint *neg; - friend bool mergeandfree(ModelVector * to, ModelVector * from); }; +Constraint * allocConstraint(CType t, Constraint *l, Constraint *r); +Constraint * allocUnaryConstraint(CType t, Constraint *l); +Constraint * allocArrayConstraint(CType t, uint num, Constraint ** array); +Constraint * allocVarConstraint(CType t, uint var); + +void freeConstraint(Constraint *); +void printConstraint(Constraint * c); +void dumpConstraint(Constraint * c, IncrementalSolver *solver); +uint getVarConstraint(Constraint * c) {ASSERT(c->type==VAR); return c->numoperandsorvar;} +VectorConstraint * simplify(Constraint * c); +CType getType(Constraint * c) {return c->type;} +bool isFalse(Constraint * c) {return c->type==FALSE;} +bool isTrue(Constraint * c) {return c->type==TRUE;} +void freeConstraint(Constraint * c); +void freerecConstraint(Constraint * c); +Constraint * cloneConstraint(Constraint * c); +void setNegConstraint(Constraint * this, Constraint *c) {this->neg=c;} +Constraint *negateConstraint(Constraint * c); + extern Constraint ctrue; extern Constraint cfalse; Constraint * generateConstraint(uint numvars, Constraint ** vars, uint value); Constraint * generateLTConstraint(uint numvars, Constraint ** vars, uint value); -Constraint * generateEquivConstraint(uint numvars, Constraint **var1, Constraint **var2); +Constraint * generateEquivNVConstraint(uint numvars, Constraint **var1, Constraint **var2); Constraint * generateEquivConstraint(Constraint *var1, Constraint *var2); #endif diff --git a/src/structs.c b/src/structs.c index 058f628..4cfb51a 100644 --- a/src/structs.c +++ b/src/structs.c @@ -4,5 +4,6 @@ VectorImpl(Int, uint64_t, 4); VectorImpl(Boolean, Boolean *, 4); VectorImpl(Void, void *, 4); +VectorImpl(Constraint, Constraint *, 4); HashTableImpl(Void, void *, void *, Ptr_hash_function, Ptr_equals); HashSetImpl(Void, void *, Ptr_hash_function, Ptr_equals); diff --git a/src/structs.h b/src/structs.h index da5f863..83ce58c 100644 --- a/src/structs.h +++ b/src/structs.h @@ -7,6 +7,7 @@ VectorDef(Int, uint64_t, 4); VectorDef(Boolean, Boolean *, 4); +VectorDef(Constraint, Constraint *, 4); VectorDef(Void, void *, 4); inline unsigned int Ptr_hash_function(void * hash) { diff --git a/src/vector.h b/src/vector.h index 9beccb3..a867db6 100644 --- a/src/vector.h +++ b/src/vector.h @@ -16,7 +16,8 @@ type getVector ## name(Vector ## name *vector, uint index); \ void setVector ## name(Vector ## name *vector, uint index, type item); \ uint getSizeVector ##name(Vector ##name *vector); \ - void freeVector ##name(Vector ##name *vector); + void freeVector ##name(Vector ##name *vector); \ + void clearVector ##name(Vector ## name *vector); #define VectorImpl(name, type, defcap) \ Vector ## name * allocDefVector ## name() { \ @@ -53,5 +54,8 @@ void freeVector ##name(Vector ##name *vector) { \ ourfree(vector->array); \ ourfree(vector); \ + } \ + void clearVector ##name(Vector ## name *vector) { \ + vector->size=0; \ } #endif