From: Hamed Date: Thu, 15 Jun 2017 19:56:05 +0000 (-0700) Subject: commit after resolving conflicts X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=70b6717f45d3d104316e652522f4e7b0c02186b2;hp=c901d86ec2dca856e679c77eb52310791048887a;p=satune.git commit after resolving conflicts --- diff --git a/src/C.cfg b/src/C.cfg index a464e72..9831cf2 100644 --- a/src/C.cfg +++ b/src/C.cfg @@ -3,6 +3,7 @@ indent_cmt_with_tabs = True indent_columns = 2 indent_class = True output_tab_size = 2 +input_tab_size = 2 nl_func_leave_one_liners = True sp_after_semi = Ignore sp_after_semi_for = Remove @@ -11,3 +12,4 @@ sp_special_semi = ignore sp_before_semi = ignore sp_before_semi_for_empty = ignore sp_after_semi_for_empty = ignore +sp_before_nl_cont = ignore \ No newline at end of file diff --git a/src/Makefile b/src/Makefile index dae27b7..a5408be 100644 --- a/src/Makefile +++ b/src/Makefile @@ -4,7 +4,9 @@ PHONY += directories MKDIR_P = mkdir -p OBJ_DIR = bin -CPP_SOURCES := set.cc mutableset.cc element.cc function.cc order.cc table.cc predicate.cc boolean.cc csolver.cc 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 inc_solver.c + +TABBING_H := boolean.h classlist.h common.h config.h constraint.h csolver.h element.h function.h inc_solver.h mutableset.h mymemory.h ops.h order.h predicate.h set.h solver_interface.h structs.h table.h OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o) @@ -31,7 +33,7 @@ debug: CPPFLAGS += -DCONFIG_DEBUG debug: all PHONY += docs -docs: *.cc *.h +docs: *.c *.cc *.h doxygen $(LIB_SO): $(OBJECTS) @@ -62,8 +64,8 @@ tags: ctags -R tabbing: - uncrustify -c C.cfg --no-backup *.cc - uncrustify -c C.cfg --no-backup *.h + uncrustify -c C.cfg --no-backup *.c + uncrustify -c C.cfg --no-backup $(TABBING_H) .PHONY: $(PHONY) diff --git a/src/constraint.c b/src/constraint.c index c8a622a..8b38540 100644 --- a/src/constraint.c +++ b/src/constraint.c @@ -11,87 +11,83 @@ #include "mymemory.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 deleteConstraint(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); - solver->addClauseLiteral(0); - } else if (type==NOTVAR) { - solver->addClauseLiteral(-numoperandsorvar); - solver->addClauseLiteral(0); +void dumpConstraint(Constraint * this, IncrementalSolver *solver) { + if (this->type==VAR) { + addClauseLiteral(solver, this->numoperandsorvar); + addClauseLiteral(solver, 0); + } else if (this->type==NOTVAR) { + addClauseLiteral(solver, -this->numoperandsorvar); + addClauseLiteral(solver, 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); + addClauseLiteral(solver, c->numoperandsorvar); } else if (c->type==NOTVAR) { - solver->addClauseLiteral(-c->numoperandsorvar); + addClauseLiteral(solver, -c->numoperandsorvar); } else ASSERT(0); } - solver->addClauseLiteral(0); + addClauseLiteral(solver, 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; + deleteConstraint(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()); + Constraint * imp1=allocConstraint(OR, negateConstraint(cloneConstraint(var1)), var2); + Constraint * imp2=allocConstraint(OR, var1, negateConstraint(cloneConstraint(var2))); - return new Constraint(AND, imp1, imp2); + 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; + deleteVectorConstraint(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..06bb1d1 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 deleteConstraint(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 internalfreeConstraint(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/csolver.c b/src/csolver.c index 2e4f316..d1b0f58 100644 --- a/src/csolver.c +++ b/src/csolver.c @@ -2,44 +2,71 @@ #include "set.h" #include "mutableset.h" #include "element.h" + CSolver * allocCSolver() { CSolver * tmp=(CSolver *) ourmalloc(sizeof(CSolver)); - tmp->constraint=allocDefVectorBoolean(); - tmp->uniqSec=1; + tmp->constraints=allocDefVectorBoolean(); + tmp->sets=allocDefVectorSet(); + tmp->elements=allocDefVectorElement(); return tmp; } -Set * createSet(CSolver * solver, VarType type, uint64_t * elements, uint num) { - Set* set = allocSet(type, elements,num ); - return set; +/** This function tears down the solver and the entire AST */ + +void deleteSolver(CSolver *this) { + deleteVectorBoolean(this->constraints); + uint size=getSizeVectorSet(this->sets); + for(uint i=0;isets, i)); + } + + deleteVectorSet(this->sets); + + size=getSizeVectorElement(this->elements); + for(uint i=0;ielements, i)); + } + + deleteVectorElement(this->elements); + ourfree(this); +} + +Set * createSet(CSolver * this, VarType type, uint64_t * elements, uint numelements) { + Set * set=allocSet(type, elements, numelements); + pushVectorSet(this->sets, set); + return set; } -Set * createRangeSet(CSolver * solver, VarType type, uint64_t lowrange, uint64_t highrange) { - Set* rset = allocSetRange(type, lowrange, highrange); - return rset; +Set * createRangeSet(CSolver * this, VarType type, uint64_t lowrange, uint64_t highrange) { + Set * set=allocSetRange(type, lowrange, highrange); + pushVectorSet(this->sets, set); + return set; } -MutableSet * createMutableSet(CSolver * solver, VarType type) { - MutableSet* mset = allocMutableSet(type); - return mset; +MutableSet * createMutableSet(CSolver * this, VarType type) { + MutableSet * set=allocMutableSet(type); + pushVectorSet(this->sets, set); + return set; } void addItem(CSolver *solver, MutableSet * set, uint64_t element) { - addElementMSet(set, element); + addElementMSet(set, element); } -int64_t createUniqueItem(CSolver *solver, MutableSet * set) { - uint64_t uSec= solver->uniqSec++; - addElementMSet(set, uSec); - return uSec; +uint64_t createUniqueItem(CSolver *solver, MutableSet * set) { + uint64_t element=set->low++; + addElementMSet(set, element); + return element; } -Element * getElementVar(CSolver *solver, Set * set) { - return allocElement(set); +Element * getElementVar(CSolver *this, Set * set) { + Element * element=allocElement(set); + pushVectorElement(this->elements, element); + return element; } -Boolean * getBooleanVar(CSolver *solver) { - return NULL; +Boolean * getBooleanVar(CSolver *solver, VarType type) { + return NULL; } Function * createFunctionOperator(CSolver *solver, enum ArithOp op, Set ** domain, Set * range, enum OverFlowBehavior overflowbehavior, Boolean * overflowstatus) { @@ -77,8 +104,8 @@ Boolean * applyLogicalOperation(CSolver *solver, enum LogicOp op, Boolean ** arr return NULL; } -void addBoolean(CSolver *solver, Boolean * constraint) { - solver-> +void addBoolean(CSolver *this, Boolean * constraint) { + pushVectorBoolean(this->constraints, constraint); } Order * createOrder(CSolver *solver, enum OrderType type, Set * set) { diff --git a/src/csolver.h b/src/csolver.h index f2db838..63ba766 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -5,20 +5,21 @@ #include "structs.h" struct CSolver { - VectorBoolean * constraint; - uint64_t uniqSec; + VectorBoolean * constraints; + VectorSet * sets; + VectorElement * elements; }; - + CSolver * allocCSolver(); Set * createSet(CSolver *, VarType type, uint64_t * elements, uint num); Set * createRangeSet(CSolver *, VarType type, uint64_t lowrange, uint64_t highrange); MutableSet * createMutableSet(CSolver *, VarType type); void addItem(CSolver *, MutableSet * set, uint64_t element); -int64_t createUniqueItem(CSolver *, MutableSet * set); +uint64_t createUniqueItem(CSolver *, MutableSet * set); Element * getElementVar(CSolver *, Set * set); -Boolean * getBooleanVar(CSolver *); +Boolean * getBooleanVar(CSolver *, VarType type); Function * createFunctionOperator(CSolver *, enum ArithOp op, Set ** domain, Set * range, enum OverFlowBehavior overflowbehavior, Boolean * overflowstatus); //Does Not Overflow diff --git a/src/element.c b/src/element.c index 2513fe5..191686c 100644 --- a/src/element.c +++ b/src/element.c @@ -5,3 +5,7 @@ Element *allocElement(Set * s) { tmp->set=s; return tmp; } + +void deleteElement(Element *this) { + ourfree(this); +} diff --git a/src/element.h b/src/element.h index 06c33a0..8f0f082 100644 --- a/src/element.h +++ b/src/element.h @@ -8,4 +8,5 @@ struct Element { }; Element * allocElement(Set *s); +void deleteElement(Element *this); #endif diff --git a/src/hashset.h b/src/hashset.h index c9d3b9d..6d87078 100644 --- a/src/hashset.h +++ b/src/hashset.h @@ -11,211 +11,184 @@ #define HASH_SET_H #include "hashtable.h" -template -struct LinkNode { - _Key key; - LinkNode<_Key> *prev; - LinkNode<_Key> *next; -}; - -template -class HashSet; - -template, bool (*equals)(_Key, _Key) = default_equals<_Key> > -class HSIterator { -public: - HSIterator(LinkNode<_Key> *_curr, HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * _set) : - curr(_curr), - set(_set) - { - } - - /** Override: new operator */ - void * operator new(size_t size) { - return _malloc(size); - } - - /** Override: delete operator */ - void operator delete(void *p, size_t size) { - _free(p); - } - - /** Override: new[] operator */ - void * operator new[](size_t size) { - return _malloc(size); - } - - /** Override: delete[] operator */ - void operator delete[](void *p, size_t size) { - _free(p); - } - - bool hasNext() { - return curr!=NULL; - } - - _Key next() { - _Key k=curr->key; - last=curr; - curr=curr->next; - return k; - } - - _Key currKey() { - return last->key; - } - - void remove() { - _Key k=last->key; - set->remove(k); - } - -private: - LinkNode<_Key> *curr; - LinkNode<_Key> *last; - HashSet <_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * set; -}; - -template, bool (*equals)(_Key, _Key) = default_equals<_Key> > -class HashSet { -public: - HashSet(unsigned int initialcapacity = 16, double factor = 0.5) : - table(new HashTable<_Key, LinkNode<_Key> *, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(initialcapacity, factor)), - list(NULL), - tail(NULL) - { - } - - /** @brief Hashset destructor */ - ~HashSet() { - LinkNode<_Key> *tmp=list; - while(tmp!=NULL) { - LinkNode<_Key> *tmpnext=tmp->next; - _free(tmp); - tmp=tmpnext; - } - delete table; - } - - HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * copy() { - HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> *copy=new HashSet<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(table->getCapacity(), table->getLoadFactor()); - HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * it=iterator(); - while(it->hasNext()) - copy->add(it->next()); - delete it; - return copy; - } - - void reset() { - LinkNode<_Key> *tmp=list; - while(tmp!=NULL) { - LinkNode<_Key> *tmpnext=tmp->next; - _free(tmp); - tmp=tmpnext; - } - list=tail=NULL; - table->reset(); - } - - /** @brief Adds a new key to the hashset. Returns false if the key - * is already present. */ - - bool add(_Key key) { - LinkNode<_Key> * val=table->get(key); - if (val==NULL) { - LinkNode<_Key> * newnode=(LinkNode<_Key> *)_malloc(sizeof(struct LinkNode<_Key>)); - newnode->prev=tail; - newnode->next=NULL; - newnode->key=key; - if (tail!=NULL) - tail->next=newnode; - else - list=newnode; - tail=newnode; - table->put(key, newnode); - return true; - } else - return false; - } - - /** @brief Gets the original key corresponding to this one from the - * hashset. Returns NULL if not present. */ - - _Key get(_Key key) { - LinkNode<_Key> * val=table->get(key); - if (val!=NULL) - return val->key; - else - return NULL; - } - - _Key getFirstKey() { - return list->key; - } - - bool contains(_Key key) { - return table->get(key)!=NULL; - } - - bool remove(_Key key) { - LinkNode<_Key> * oldlinknode; - oldlinknode=table->get(key); - if (oldlinknode==NULL) { - return false; - } - table->remove(key); - - //remove link node from the list - if (oldlinknode->prev==NULL) - list=oldlinknode->next; - else - oldlinknode->prev->next=oldlinknode->next; - if (oldlinknode->next!=NULL) - oldlinknode->next->prev=oldlinknode->prev; - else - tail=oldlinknode->prev; - _free(oldlinknode); - return true; - } - - unsigned int getSize() { - return table->getSize(); - } - - bool isEmpty() { - return getSize()==0; - } - - - - HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * iterator() { - return new HSIterator<_Key, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals>(list, this); - } - - /** Override: new operator */ - void * operator new(size_t size) { - return _malloc(size); - } - - /** Override: delete operator */ - void operator delete(void *p, size_t size) { - _free(p); - } - - /** Override: new[] operator */ - void * operator new[](size_t size) { - return _malloc(size); - } - - /** Override: delete[] operator */ - void operator delete[](void *p, size_t size) { - _free(p); - } -private: - HashTable<_Key, LinkNode<_Key>*, _KeyInt, _Shift, _malloc, _calloc, _free, hash_function, equals> * table; - LinkNode<_Key> *list; - LinkNode<_Key> *tail; -}; +#define HashSetDef(Name, _Key, hash_function, equals) \ + struct LinkNode ## Name { \ + _Key key; \ + struct LinkNode ## Name *prev; \ + struct LinkNode ## Name *next; \ + }; \ + typedef struct LinkNode ## Name LinkNode ## Name; \ + struct HashSet ## Name; \ + typedef struct HashSet ## Name HashSet ## Name; \ + struct HSIterator ## Name { \ + LinkNode ## Name *curr; \ + LinkNode ## Name *last; \ + HashSet ## Name * set; \ + }; \ + typedef struct HSIterator ## Name HSIterator ## Name; \ + HashTableDef(Name ## Set, _Key, LinkNode ## Name *, hash_function, equals); \ + HSIterator ## Name * allocHSIterator ## Name(LinkNode ## Name *_curr, HashSet ## Name * _set); \ + void deleteIter ## Name(HSIterator ## Name *hsit); \ + bool hasNext ## Name(HSIterator ## Name *hsit); \ + _Key next ## Name(HSIterator ## Name *hsit); \ + _Key currKey ## Name(HSIterator ## Name *hsit); \ + void removeIter ## Name(HSIterator ## Name *hsit); \ + struct HashSet ## Name { \ + HashTable ## Name ## Set * table; \ + LinkNode ## Name *list; \ + LinkNode ## Name *tail; \ + }; \ + typedef struct HashSet ## Name HashSet ## Name; \ + \ + HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor); \ + void deleteHashSet ## Name(struct HashSet ## Name * set); \ + HashSet ## Name * copy ## Name(HashSet ## Name * set); \ + void resetSet ## Name(HashSet ## Name * set); \ + bool add ## Name(HashSet ## Name * set,_Key key); \ + _Key getSet ## Name(HashSet ## Name * set,_Key key); \ + _Key getFirstKey ## Name(HashSet ## Name * set); \ + bool containsSet ## Name(HashSet ## Name * set,_Key key); \ + bool removeSet ## Name(HashSet ## Name * set,_Key key); \ + unsigned int getSizeSet ## Name(HashSet ## Name * set); \ + bool isEmpty ## Name(HashSet ## Name * set); \ + HSIterator ## Name * iterator ## Name(HashSet ## Name * set); + + +#define HashSetImpl(Name, _Key, hash_function, equals) \ + HashTableImpl(Name ## Set, _Key, LinkNode ## Name *, hash_function, equals); \ + HSIterator ## Name * allocHSIterator ## Name(LinkNode ## Name *_curr, HashSet ## Name * _set) { \ + HSIterator ## Name * hsit = (HSIterator ## Name *) ourmalloc(sizeof(HSIterator ## Name)); \ + hsit->curr=_curr; \ + hsit->set=_set; \ + return hsit; \ + } \ + \ + void deleteIter ## Name(HSIterator ## Name *hsit) { \ + ourfree(hsit); \ + } \ + \ + bool hasNext ## Name(HSIterator ## Name *hsit) { \ + return hsit->curr!=NULL; \ + } \ + \ + _Key next ## Name(HSIterator ## Name *hsit) { \ + _Key k=hsit->curr->key; \ + hsit->last=hsit->curr; \ + hsit->curr=hsit->curr->next; \ + return k; \ + } \ + \ + _Key currKey ## Name(HSIterator ## Name *hsit) { \ + return hsit->last->key; \ + } \ + \ + void removeIter ## Name(HSIterator ## Name *hsit) { \ + _Key k=hsit->last->key; \ + removeSet ## Name(hsit->set, k); \ + } \ + \ + HashSet ## Name * allocHashSet ## Name (unsigned int initialcapacity, double factor) { \ + HashSet ## Name * set = (HashSet ## Name *) ourmalloc(sizeof(struct HashSet ## Name)); \ + set->table=allocHashTable ## Name ## Set(initialcapacity, factor); \ + set->list=NULL; \ + set->tail=NULL; \ + return set; \ +} \ + \ + void deleteHashSet ## Name(struct HashSet ## Name * set) { \ + LinkNode ## Name *tmp=set->list; \ + while(tmp!=NULL) { \ + LinkNode ## Name *tmpnext=tmp->next; \ + ourfree(tmp); \ + tmp=tmpnext; \ + } \ + deleteHashTable ## Name ## Set(set->table); \ + ourfree(set); \ + } \ + \ + HashSet ## Name * copy ## Name(HashSet ## Name * set) { \ + HashSet ## Name *copy=allocHashSet ## Name(getCapacity ## Name ## Set(set->table), getLoadFactor ## Name ## Set(set->table)); \ + HSIterator ## Name * it=iterator ## Name(set); \ + while(hasNext ## Name(it)) \ + add ## Name(copy, next ## Name(it)); \ + deleteIter ## Name(it); \ + return copy; \ + } \ + \ + void resetSet ## Name(HashSet ## Name * set) { \ + LinkNode ## Name *tmp=set->list; \ + while(tmp!=NULL) { \ + LinkNode ## Name *tmpnext=tmp->next; \ + ourfree(tmp); \ + tmp=tmpnext; \ + } \ + set->list=set->tail=NULL; \ + reset ## Name ## Set(set->table); \ + } \ + \ + bool add ## Name(HashSet ## Name * set,_Key key) { \ + LinkNode ## Name * val=get ## Name ## Set(set->table, key); \ + if (val==NULL) { \ + LinkNode ## Name * newnode=(LinkNode ## Name *)ourmalloc(sizeof(struct LinkNode ## Name)); \ + newnode->prev=set->tail; \ + newnode->next=NULL; \ + newnode->key=key; \ + if (set->tail!=NULL) \ + set->tail->next=newnode; \ + else \ + set->list=newnode; \ + set->tail=newnode; \ + put ## Name ## Set(set->table, key, newnode); \ + return true; \ + } else \ + return false; \ + } \ + \ + _Key getSet ## Name(HashSet ## Name * set,_Key key) { \ + LinkNode ## Name * val=get ## Name ## Set(set->table, key); \ + if (val!=NULL) \ + return val->key; \ + else \ + return NULL; \ + } \ + \ + _Key getFirstKey ## Name(HashSet ## Name * set) { \ + return set->list->key; \ + } \ + \ + bool containsSet ## Name(HashSet ## Name * set,_Key key) { \ + return get ## Name ## Set(set->table, key)!=NULL; \ + } \ + \ + bool removeSet ## Name(HashSet ## Name * set,_Key key) { \ + LinkNode ## Name * oldlinknode; \ + oldlinknode=get ## Name ## Set(set->table, key); \ + if (oldlinknode==NULL) { \ + return false; \ + } \ + remove ## Name ## Set(set->table, key); \ + \ + if (oldlinknode->prev==NULL) \ + set->list=oldlinknode->next; \ + else \ + oldlinknode->prev->next=oldlinknode->next; \ + if (oldlinknode->next!=NULL) \ + oldlinknode->next->prev=oldlinknode->prev; \ + else \ + set->tail=oldlinknode->prev; \ + ourfree(oldlinknode); \ + return true; \ + } \ + \ + unsigned int getSizeSet ## Name(HashSet ## Name * set) { \ + return getSizeTable ## Name ## Set(set->table); \ + } \ + \ + bool isEmpty ## Name(HashSet ## Name * set) { \ + return getSizeSet ## Name(set)==0; \ + } \ + \ + HSIterator ## Name * iterator ## Name(HashSet ## Name * set) { \ + return allocHSIterator ## Name(set->list, set); \ + } #endif diff --git a/src/hashtable.h b/src/hashtable.h index f007b59..e0db665 100644 --- a/src/hashtable.h +++ b/src/hashtable.h @@ -20,28 +20,6 @@ #include "mymemory.h" #include "common.h" -/** - * @brief HashTable node - * - * @tparam _Key Type name for the key - * @tparam _Val Type name for the values to be stored - */ -template -struct hashlistnode { - _Key key; - _Val val; -}; - -template -inline unsigned int default_hash_function(_Key hash) { - return (unsigned int)(((_KeyInt)hash) >> _Shift); -} - -template -inline bool default_equals(_Key key1, _Key key2) { - return key1 == key2; -} - /** * @brief A simple, custom hash table * @@ -52,322 +30,252 @@ inline bool default_equals(_Key key1, _Key key2) { * * @tparam _Key Type name for the key * @tparam _Val Type name for the values to be stored - * @tparam _KeyInt Integer type that is at least as large as _Key. Used for key - * manipulation and storage. - * @tparam _Shift Logical shift to apply to all keys. Default 0. - * @tparam _malloc Provide your own 'malloc' for the table, or default to - * model_malloc. - * @tparam _calloc Provide your own 'calloc' for the table, or default to - * model_malloc. - * @tparam _free Provide your own 'free' for the table, or default to - * model_malloc. */ -template, bool (*equals)(_Key, _Key) = default_equals<_Key> > -class HashTable { -public: - /** - * @brief Hash table constructor - * @param initialcapacity Sets the initial capacity of the hash table. - * Default size 1024. - * @param factor Sets the percentage full before the hashtable is - * resized. Default ratio 0.5. - */ - HashTable(unsigned int initialcapacity = 1024, double factor = 0.5) { - // Allocate space for the hash table - table = (struct hashlistnode<_Key, _Val> *)_calloc(initialcapacity, sizeof(struct hashlistnode<_Key, _Val>)); - zero = NULL; - loadfactor = factor; - capacity = initialcapacity; - capacitymask = initialcapacity - 1; - - threshold = (unsigned int)(initialcapacity * loadfactor); - // Initial number of elements in the hash - size = 0; - } - - /** @brief Hash table destructor */ - ~HashTable() { - _free(table); - if (zero) - _free(zero); - } - - /** Override: new operator */ - void * operator new(size_t size) { - return _malloc(size); - } - - /** Override: delete operator */ - void operator delete(void *p, size_t size) { - _free(p); - } - - /** Override: new[] operator */ - void * operator new[](size_t size) { - return _malloc(size); - } - - /** Override: delete[] operator */ - void operator delete[](void *p, size_t size) { - _free(p); - } - - /** @brief Reset the table to its initial state. */ - void reset() { - memset(table, 0, capacity * sizeof(struct hashlistnode<_Key, _Val>)); - if (zero) { - _free(zero); - zero = NULL; - } - size = 0; - } - - void resetanddelete() { - for(unsigned int i=0;i *bin = &table[i]; - if (bin->key != NULL) { - bin->key = NULL; - if (bin->val != NULL) { - delete bin->val; - bin->val = NULL; - } - } - } - if (zero) { - if (zero->val != NULL) - delete zero->val; - _free(zero); - zero = NULL; - } - size = 0; - } - - void resetandfree() { - for(unsigned int i=0;i *bin = &table[i]; - if (bin->key != NULL) { - bin->key = NULL; - if (bin->val != NULL) { - _free(bin->val); - bin->val = NULL; - } - } - } - if (zero) { - if (zero->val != NULL) - _free(zero->val); - _free(zero); - zero = NULL; - } - size = 0; - } - - /** - * @brief Put a key/value pair into the table - * @param key The key for the new value; must not be 0 or NULL - * @param val The value to store in the table - */ - void put(_Key key, _Val val) { - /* HashTable cannot handle 0 as a key */ - if (!key) { - if (!zero) { - zero=(struct hashlistnode<_Key, _Val> *)_malloc(sizeof(struct hashlistnode<_Key, _Val>)); - size++; - } - zero->key=key; - zero->val=val; - return; - } - - if (size > threshold) - resize(capacity << 1); - - struct hashlistnode<_Key, _Val> *search; - - unsigned int index = hash_function(key); - do { - index &= capacitymask; - search = &table[index]; - if (!search->key) { - //key is null, probably done - break; - } - if (equals(search->key, key)) { - search->val = val; - return; - } - index++; - } while (true); - - search->key = key; - search->val = val; - size++; - } - - /** - * @brief Lookup the corresponding value for the given key - * @param key The key for finding the value; must not be 0 or NULL - * @return The value in the table, if the key is found; otherwise 0 - */ - _Val get(_Key key) const { - struct hashlistnode<_Key, _Val> *search; - - /* HashTable cannot handle 0 as a key */ - if (!key) { - if (zero) - return zero->val; - else - return (_Val) 0; - } - - unsigned int oindex = hash_function(key) & capacitymask; - unsigned int index=oindex; - do { - search = &table[index]; - if (!search->key) { - if (!search->val) - break; - } else - if (equals(search->key, key)) - return search->val; - index++; - index &= capacitymask; - if (index==oindex) - break; - } while (true); - return (_Val)0; - } - - /** - * @brief Remove the given key and return the corresponding value - * @param key The key for finding the value; must not be 0 or NULL - * @return The value in the table, if the key is found; otherwise 0 - */ - _Val remove(_Key key) { - struct hashlistnode<_Key, _Val> *search; - - /* HashTable cannot handle 0 as a key */ - if (!key) { - if (!zero) { - return (_Val)0; - } else { - _Val v=zero->val; - _free(zero); - zero=NULL; - size--; - return v; - } - } - - - unsigned int index = hash_function(key); - do { - index &= capacitymask; - search = &table[index]; - if (!search->key) { - if (!search->val) - break; - } else - if (equals(search->key, key)) { - _Val v=search->val; - //empty out this bin - search->val=(_Val) 1; - search->key=0; - size--; - return v; - } - index++; - } while (true); - return (_Val)0; - } - - unsigned int getSize() const { - return size; - } - - - /** - * @brief Check whether the table contains a value for the given key - * @param key The key for finding the value; must not be 0 or NULL - * @return True, if the key is found; false otherwise - */ - bool contains(_Key key) const { - struct hashlistnode<_Key, _Val> *search; - - /* HashTable cannot handle 0 as a key */ - if (!key) { - return zero!=NULL; - } - - unsigned int index = hash_function(key); - do { - index &= capacitymask; - search = &table[index]; - if (!search->key) { - if (!search->val) - break; - } else - if (equals(search->key, key)) - return true; - index++; - } while (true); - return false; - } - - /** - * @brief Resize the table - * @param newsize The new size of the table - */ - void resize(unsigned int newsize) { - struct hashlistnode<_Key, _Val> *oldtable = table; - struct hashlistnode<_Key, _Val> *newtable; - unsigned int oldcapacity = capacity; - - if ((newtable = (struct hashlistnode<_Key, _Val> *)_calloc(newsize, sizeof(struct hashlistnode<_Key, _Val>))) == NULL) { - model_print("calloc error %s %d\n", __FILE__, __LINE__); - exit(EXIT_FAILURE); - } - - table = newtable; - // Update the global hashtable upon resize() - capacity = newsize; - capacitymask = newsize - 1; - - threshold = (unsigned int)(newsize * loadfactor); - - struct hashlistnode<_Key, _Val> *bin = &oldtable[0]; - struct hashlistnode<_Key, _Val> *lastbin = &oldtable[oldcapacity]; - for (;bin < lastbin;bin++) { - _Key key = bin->key; - - struct hashlistnode<_Key, _Val> *search; - if (!key) - continue; +#define HashTableDef(Name, _Key, _Val, hash_function, equals)\ + struct hashlistnode ## Name { \ + _Key key; \ + _Val val; \ + }; \ + \ + struct HashTable ## Name { \ + struct hashlistnode ## Name *table; \ + struct hashlistnode ## Name *zero; \ + unsigned int capacity; \ + unsigned int size; \ + unsigned int capacitymask; \ + unsigned int threshold; \ + double loadfactor; \ + }; \ + \ + typedef struct HashTable ## Name HashTable ## Name; \ + HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor); \ + void deleteHashTable ## Name(HashTable ## Name * tab); \ + void reset ## Name(HashTable ## Name * tab); \ + void resetandfree ## Name(HashTable ## Name * tab); \ + void put ## Name(HashTable ## Name * tab, _Key key, _Val val); \ + _Val get ## Name(const HashTable ## Name * tab, _Key key); \ + _Val remove ## Name(HashTable ## Name * tab, _Key key); \ + unsigned int getSizeTable ## Name(const HashTable ## Name * tab); \ + bool contains ## Name(const HashTable ## Name * tab, _Key key); \ + void resize ## Name(HashTable ## Name * tab, unsigned int newsize); \ + double getLoadFactor ## Name(HashTable ## Name * tab); \ + unsigned int getCapacity ## Name(HashTable ## Name * tab); + +#define HashTableImpl(Name, _Key, _Val, hash_function, equals) \ + HashTable ## Name * allocHashTable ## Name(unsigned int initialcapacity, double factor) { \ + HashTable ## Name * tab = (HashTable ## Name *) ourmalloc(sizeof(HashTable ## Name)); \ + tab -> table = (struct hashlistnode ## Name *) ourcalloc(initialcapacity, sizeof(struct hashlistnode ## Name)); \ + tab->zero = NULL; \ + tab->loadfactor = factor; \ + tab->capacity = initialcapacity; \ + tab->capacitymask = initialcapacity - 1; \ + \ + tab->threshold = (unsigned int)(initialcapacity * factor); \ + tab->size = 0; \ + return tab; \ + } \ + \ + void deleteHashTable ## Name(HashTable ## Name * tab) { \ + ourfree(tab->table); \ + if (tab->zero) \ + ourfree(tab->zero); \ + ourfree(tab); \ + } \ + \ + void reset ## Name(HashTable ## Name * tab) { \ + memset(tab->table, 0, tab->capacity * sizeof(struct hashlistnode ## Name)); \ + if (tab->zero) { \ + ourfree(tab->zero); \ + tab->zero = NULL; \ + } \ + tab->size = 0; \ + } \ + \ + void resetandfree ## Name(HashTable ## Name * tab) { \ + for(unsigned int i=0;icapacity;i++) { \ + struct hashlistnode ## Name *bin = &tab->table[i]; \ + if (bin->key != NULL) { \ + bin->key = NULL; \ + if (bin->val != NULL) { \ + ourfree(bin->val); \ + bin->val = NULL; \ + } \ + } \ + } \ + if (tab->zero) { \ + if (tab->zero->val != NULL) \ + ourfree(tab->zero->val); \ + ourfree(tab->zero); \ + tab->zero = NULL; \ + } \ + tab->size = 0; \ + } \ + \ + void put ## Name(HashTable ## Name * tab, _Key key, _Val val) { \ + if (!key) { \ + if (!tab->zero) { \ + tab->zero=(struct hashlistnode ## Name *)ourmalloc(sizeof(struct hashlistnode ## Name)); \ + tab->size++; \ + } \ + tab->zero->key=key; \ + tab->zero->val=val; \ + return; \ + } \ + \ + if (tab->size > tab->threshold) \ + resize ## Name (tab, tab->capacity << 1); \ + \ + struct hashlistnode ## Name *search; \ + \ + unsigned int index = hash_function(key); \ + do { \ + index &= tab->capacitymask; \ + search = &tab->table[index]; \ + if (!search->key) { \ + break; \ + } \ + if (equals(search->key, key)) { \ + search->val = val; \ + return; \ + } \ + index++; \ + } while (true); \ + \ + search->key = key; \ + search->val = val; \ + tab->size++; \ + } \ + \ + _Val get ## Name(const HashTable ## Name * tab, _Key key) { \ + struct hashlistnode ## Name *search; \ + \ + if (!key) { \ + if (tab->zero) \ + return tab->zero->val; \ + else \ + return (_Val) 0; \ + } \ + \ + unsigned int oindex = hash_function(key) & tab->capacitymask; \ + unsigned int index=oindex; \ + do { \ + search = &tab->table[index]; \ + if (!search->key) { \ + if (!search->val) \ + break; \ + } else \ + if (equals(search->key, key)) \ + return search->val; \ + index++; \ + index &= tab->capacitymask; \ + if (index==oindex) \ + break; \ + } while (true); \ + return (_Val)0; \ + } \ + \ + _Val remove ## Name(HashTable ## Name * tab, _Key key) { \ + struct hashlistnode ## Name *search; \ + \ + if (!key) { \ + if (!tab->zero) { \ + return (_Val)0; \ + } else { \ + _Val v=tab->zero->val; \ + ourfree(tab->zero); \ + tab->zero=NULL; \ + tab->size--; \ + return v; \ + } \ + } \ + \ + unsigned int index = hash_function(key); \ + do { \ + index &= tab->capacitymask; \ + search = &tab->table[index]; \ + if (!search->key) { \ + if (!search->val) \ + break; \ + } else \ + if (equals(search->key, key)) { \ + _Val v=search->val; \ + search->val=(_Val) 1; \ + search->key=0; \ + tab->size--; \ + return v; \ + } \ + index++; \ + } while (true); \ + return (_Val)0; \ + } \ + \ + unsigned int getSizeTable ## Name(const HashTable ## Name * tab) { \ + return tab->size; \ + } \ + \ + \ + bool contains ## Name(const HashTable ## Name * tab, _Key key) { \ + struct hashlistnode ## Name *search; \ + if (!key) { \ + return tab->zero!=NULL; \ + } \ + unsigned int index = hash_function(key); \ + do { \ + index &= tab->capacitymask; \ + search = &tab->table[index]; \ + if (!search->key) { \ + if (!search->val) \ + break; \ + } else \ + if (equals(search->key, key)) \ + return true; \ + index++; \ + } while (true); \ + return false; \ + } \ + \ + void resize ## Name(HashTable ## Name * tab, unsigned int newsize) { \ + struct hashlistnode ## Name *oldtable = tab->table; \ + struct hashlistnode ## Name *newtable; \ + unsigned int oldcapacity = tab->capacity; \ + \ + if ((newtable = (struct hashlistnode ## Name *)ourcalloc(newsize, sizeof(struct hashlistnode ## Name))) == NULL) { \ + model_print("calloc error %s %d\n", __FILE__, __LINE__); \ + exit(EXIT_FAILURE); \ + } \ + \ + tab->table = newtable; \ + tab->capacity = newsize; \ + tab->capacitymask = newsize - 1; \ + \ + tab->threshold = (unsigned int)(newsize * tab->loadfactor); \ + \ + struct hashlistnode ## Name *bin = &oldtable[0]; \ + struct hashlistnode ## Name *lastbin = &oldtable[oldcapacity]; \ + for (;bin < lastbin;bin++) { \ + _Key key = bin->key; \ + \ + struct hashlistnode ## Name *search; \ + if (!key) \ + continue; \ + \ + unsigned int index = hash_function(key); \ + do { \ + index &= tab->capacitymask; \ + search = &tab->table[index]; \ + index++; \ + } while (search->key); \ + \ + search->key = key; \ + search->val = bin->val; \ + } \ + \ + ourfree(oldtable); \ + } \ + double getLoadFactor ## Name(HashTable ## Name * tab) {return tab->loadfactor;} \ + unsigned int getCapacity ## Name(HashTable ## Name * tab) {return tab->capacity;} - unsigned int index = hash_function(key); - do { - index &= capacitymask; - search = &table[index]; - index++; - } while (search->key); - search->key = key; - search->val = bin->val; - } - _free(oldtable); - // Free the memory of the old hash table - } - double getLoadFactor() {return loadfactor;} - unsigned int getCapacity() {return capacity;} - struct hashlistnode<_Key, _Val> *table; - struct hashlistnode<_Key, _Val> *zero; - unsigned int capacity; - unsigned int size; -private: - unsigned int capacitymask; - unsigned int threshold; - double loadfactor; -}; #endif/* __HASHTABLE_H__ */ diff --git a/src/inc_solver.c b/src/inc_solver.c index 97f050c..c25cfba 100644 --- a/src/inc_solver.c +++ b/src/inc_solver.c @@ -10,84 +10,86 @@ #include "inc_solver.h" #define SATSOLVER "sat_solver" #include - -IncrementalSolver::IncrementalSolver() : - buffer((int *)model_malloc(sizeof(int)*IS_BUFFERSIZE)), - solution(NULL), - solutionsize(0), - offset(0) -{ - createSolver(); +#include "common.h" + +IncrementalSolver * allocIncrementalSolver() { + IncrementalSolver *this=(IncrementalSolver *)ourmalloc(sizeof(IncrementalSolver)); + this->buffer=((int *)ourmalloc(sizeof(int)*IS_BUFFERSIZE)); + this->solution=NULL; + this->solutionsize=0; + this->offset=0; + createSolver(this); + return this; } -IncrementalSolver::~IncrementalSolver() { - killSolver(); - model_free(buffer); - if (solution != NULL) - model_free(solution); +void deleteIncrementalSolver(IncrementalSolver * this) { + killSolver(this); + ourfree(this->buffer); + if (this->solution != NULL) + ourfree(this->solution); } -void IncrementalSolver::reset() { - killSolver(); - offset = 0; - createSolver(); +void resetSolver(IncrementalSolver * this) { + killSolver(this); + this->offset = 0; + createSolver(this); } -void IncrementalSolver::addClauseLiteral(int literal) { - buffer[offset++]=literal; - if (offset==IS_BUFFERSIZE) { - flushBuffer(); +void addClauseLiteral(IncrementalSolver * this, int literal) { + this->buffer[this->offset++]=literal; + if (this->offset==IS_BUFFERSIZE) { + flushBufferSolver(this); } } -void IncrementalSolver::finishedClauses() { - addClauseLiteral(0); +void finishedClauses(IncrementalSolver * this) { + addClauseLiteral(this, 0); } -void IncrementalSolver::freeze(int variable) { - addClauseLiteral(IS_FREEZE); - addClauseLiteral(variable); +void freeze(IncrementalSolver * this, int variable) { + addClauseLiteral(this, IS_FREEZE); + addClauseLiteral(this, variable); } -int IncrementalSolver::solve() { +int solve(IncrementalSolver * this) { //add an empty clause - startSolve(); - return getSolution(); + startSolve(this); + return getSolution(this); } -void IncrementalSolver::startSolve() { - addClauseLiteral(IS_RUNSOLVER); - flushBuffer(); +void startSolve(IncrementalSolver *this) { + addClauseLiteral(this, IS_RUNSOLVER); + flushBufferSolver(this); } -int IncrementalSolver::getSolution() { - int result=readIntSolver(); +int getSolution(IncrementalSolver * this) { + int result=readIntSolver(this); if (result == IS_SAT) { - int numVars=readIntSolver(); - if (numVars > solutionsize) { - if (solution != NULL) - model_free(solution); - solution = (int *) model_malloc((numVars+1)*sizeof(int)); - solution[0] = 0; + int numVars=readIntSolver(this); + if (numVars > this->solutionsize) { + if (this->solution != NULL) + ourfree(this->solution); + this->solution = (int *) ourmalloc((numVars+1)*sizeof(int)); + this->solution[0] = 0; } - readSolver(&solution[1], numVars * sizeof(int)); + readSolver(this, &this->solution[1], numVars * sizeof(int)); } return result; } -int IncrementalSolver::readIntSolver() { +int readIntSolver(IncrementalSolver * this) { int value; - readSolver(&value, 4); + readSolver(this, &value, 4); return value; } -void IncrementalSolver::readSolver(void * tmp, ssize_t size) { +void readSolver(IncrementalSolver * this, void * tmp, ssize_t size) { char *result = (char *) tmp; ssize_t bytestoread=size; ssize_t bytesread=0; do { - ssize_t n=read(from_solver_fd, &((char *)result)[bytesread], bytestoread); + ssize_t n=read(this->from_solver_fd, &((char *)result)[bytesread], bytestoread); if (n == -1) { model_print("Read failure\n"); exit(-1); @@ -97,22 +99,22 @@ void IncrementalSolver::readSolver(void * tmp, ssize_t size) { } while(bytestoread != 0); } -bool IncrementalSolver::getValue(int variable) { - return solution[variable]; +bool getValueSolver(IncrementalSolver * this, int variable) { + return this->solution[variable]; } -void IncrementalSolver::createSolver() { +void createSolver(IncrementalSolver * this) { int to_pipe[2]; int from_pipe[2]; if (pipe(to_pipe) || pipe(from_pipe)) { model_print("Error creating pipe.\n"); exit(-1); } - if ((solver_pid = fork()) == -1) { + if ((this->solver_pid = fork()) == -1) { model_print("Error forking.\n"); exit(-1); } - if (solver_pid == 0) { + if (this->solver_pid == 0) { //Solver process close(to_pipe[1]); close(from_pipe[0]); @@ -129,36 +131,36 @@ void IncrementalSolver::createSolver() { close(fd); } else { //Our process - to_solver_fd = to_pipe[1]; - from_solver_fd = from_pipe[0]; + this->to_solver_fd = to_pipe[1]; + this->from_solver_fd = from_pipe[0]; close(to_pipe[0]); close(from_pipe[1]); } } -void IncrementalSolver::killSolver() { - close(to_solver_fd); - close(from_solver_fd); +void killSolver(IncrementalSolver * this) { + close(this->to_solver_fd); + close(this->from_solver_fd); //Stop the solver - if (solver_pid > 0) { + if (this->solver_pid > 0) { int status; - kill(solver_pid, SIGKILL); - waitpid(solver_pid, &status, 0); + kill(this->solver_pid, SIGKILL); + waitpid(this->solver_pid, &status, 0); } } -void IncrementalSolver::flushBuffer() { - ssize_t bytestowrite=sizeof(int)*offset; +void flushBufferSolver(IncrementalSolver * this) { + ssize_t bytestowrite=sizeof(int)*this->offset; ssize_t byteswritten=0; do { - ssize_t n=write(to_solver_fd, &((char *)buffer)[byteswritten], bytestowrite); + ssize_t n=write(this->to_solver_fd, &((char *)this->buffer)[byteswritten], bytestowrite); if (n == -1) { perror("Write failure\n"); - model_print("to_solver_fd=%d\n",to_solver_fd); + model_print("to_solver_fd=%d\n",this->to_solver_fd); exit(-1); } bytestowrite -= n; byteswritten += n; } while(bytestowrite != 0); - offset = 0; + this->offset = 0; } diff --git a/src/inc_solver.h b/src/inc_solver.h index 415dc8d..ead727f 100644 --- a/src/inc_solver.h +++ b/src/inc_solver.h @@ -18,27 +18,7 @@ #include "solver_interface.h" #include "classlist.h" -class IncrementalSolver { -public: - IncrementalSolver(); - ~IncrementalSolver(); - void addClauseLiteral(int literal); - void finishedClauses(); - void freeze(int variable); - int solve(); - void startSolve(); - int getSolution(); - - bool getValue(int variable); - void reset(); - MEMALLOC; - -private: - void createSolver(); - void killSolver(); - void flushBuffer(); - int readIntSolver(); - void readSolver(void * buffer, ssize_t size); +struct IncrementalSolver { int * buffer; int * solution; int solutionsize; @@ -47,4 +27,20 @@ private: int to_solver_fd; int from_solver_fd; }; + +IncrementalSolver * allocIncrementalSolver(); +void deleteIncrementalSolver(IncrementalSolver * this); +void addClauseLiteral(IncrementalSolver * this, int literal); +void finishedClauses(IncrementalSolver * this); +void freeze(IncrementalSolver * this, int variable); +int solve(IncrementalSolver * this); +void startSolve(IncrementalSolver * this); +int getSolution(IncrementalSolver * this); +bool getValueSolver(IncrementalSolver * this, int variable); +void resetSolver(IncrementalSolver * this); +void createSolver(IncrementalSolver * this); +void killSolver(IncrementalSolver * this); +void flushBufferSolver(IncrementalSolver * this); +int readIntSolver(IncrementalSolver * this); +void readSolver(IncrementalSolver * this, void * buffer, ssize_t size); #endif diff --git a/src/mutableset.c b/src/mutableset.c index b3fef7c..18f038b 100644 --- a/src/mutableset.c +++ b/src/mutableset.c @@ -1,12 +1,15 @@ #include "mutableset.h" -MutableSet* allocMutableSet(VarType type){ - MutableSet* set = (MutableSet*)ourmalloc(sizeof(struct Set)); - set->type = type; - set->members = allocDefVectorInt(); - set->isRange = false; - return set; +MutableSet * allocMutableSet(VarType t) { + MutableSet * tmp=(MutableSet *)ourmalloc(sizeof(MutableSet)); + tmp->type=t; + tmp->isRange=false; + tmp->low=0; + tmp->high=0; + tmp->members=allocDefVectorInt(); + return tmp; } - -void addElementMSet(MutableSet * set, uint64_t element) { pushVectorInt(set->members, element); } +void addElementMSet(MutableSet * set, uint64_t element) { + pushVectorInt(set->members, element); +} diff --git a/src/mutableset.h b/src/mutableset.h index 955d1ec..fe089f4 100644 --- a/src/mutableset.h +++ b/src/mutableset.h @@ -2,6 +2,6 @@ #define MUTABLESET_H #include "set.h" -MutableSet* allocMutableSet(VarType type); +MutableSet * allocMutableSet(VarType t); void addElementMSet(MutableSet * set, uint64_t element); #endif diff --git a/src/mymemory.h b/src/mymemory.h index 5267ce2..2fa964e 100644 --- a/src/mymemory.h +++ b/src/mymemory.h @@ -19,35 +19,9 @@ #include "config.h" -/** MEMALLOC declares the allocators for a class to allocate - * memory in the non-snapshotting heap. */ -/* -#define MEMALLOC \ - void * operator new(size_t size) { \ - return model_malloc(size); \ - } \ - void operator delete(void *p, size_t size) { \ - model_free(p); \ - } \ - void * operator new[](size_t size) { \ - return model_malloc(size); \ - } \ - void operator delete[](void *p, size_t size) { \ - model_free(p); \ - } \ - void * operator new(size_t size, void *p) { \ - return p; \ - } -*/ - void * ourmalloc(size_t size); void ourfree(void *ptr); void * ourcalloc(size_t count, size_t size); void * ourrealloc(void *ptr, size_t size); -void *model_malloc(size_t size); -void *model_calloc(size_t count, size_t size); -void * model_realloc(void *ptr, size_t size); -void model_free(void *ptr); - #endif/* _MY_MEMORY_H */ diff --git a/src/set.c b/src/set.c index c92de33..fc056a2 100644 --- a/src/set.c +++ b/src/set.c @@ -2,17 +2,17 @@ #include Set * allocSet(VarType t, uint64_t* elements, uint num) { - Set * tmp=(Set *)ourmalloc(sizeof(struct Set)); + Set * tmp=(Set *)ourmalloc(sizeof(Set)); tmp->type=t; tmp->isRange=false; tmp->low=0; tmp->high=0; - tmp->members=allocVectorArrayInt(elements, num); + tmp->members=allocVectorArrayInt(num, elements); return tmp; } Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange) { - Set * tmp=(Set *)ourmalloc(sizeof(struct Set)); + Set * tmp=(Set *)ourmalloc(sizeof(Set)); tmp->type=t; tmp->isRange=true; tmp->low=lowrange; @@ -21,8 +21,8 @@ Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange) { return tmp; } -void freeSet(Set * set) { - if (set->isRange) - freeVectorInt(set->members); +void deleteSet(Set * set) { + if (!set->isRange) + deleteVectorInt(set->members); ourfree(set); } diff --git a/src/set.h b/src/set.h index ee3f940..92315e2 100644 --- a/src/set.h +++ b/src/set.h @@ -15,14 +15,14 @@ struct Set { VarType type; bool isRange; - uint64_t low, high; + uint64_t low;//also used to count unique items + uint64_t high; VectorInt * members; }; Set *allocSet(VarType t, uint64_t * elements, uint num); -Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange); -void freeSet(Set *set); - +Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange); +void deleteSet(Set *set); #endif/* SET_H */ diff --git a/src/structs.c b/src/structs.c index 7eea923..30bca42 100644 --- a/src/structs.c +++ b/src/structs.c @@ -2,4 +2,10 @@ #include "mymemory.h" VectorImpl(Int, uint64_t, 4); +VectorImpl(Void, void *, 4); VectorImpl(Boolean, Boolean *, 4); +VectorImpl(Constraint, Constraint *, 4); +VectorImpl(Set, Set *, 4); +VectorImpl(Element, Element *, 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 4229f71..888f359 100644 --- a/src/structs.h +++ b/src/structs.h @@ -1,8 +1,25 @@ #ifndef STRUCTS_H #define STRUCTS_H #include "vector.h" +#include "hashtable.h" +#include "hashset.h" #include "classlist.h" VectorDef(Int, uint64_t, 4); +VectorDef(Void, void *, 4); VectorDef(Boolean, Boolean *, 4); +VectorDef(Constraint, Constraint *, 4); +VectorDef(Set, Set *, 4); +VectorDef(Element, Element *, 4); + +inline unsigned int Ptr_hash_function(void * hash) { + return (unsigned int)((uint64_t)hash >> 4); +} + +inline bool Ptr_equals(void * key1, void * key2) { + return key1 == key2; +} + +HashTableDef(Void, void *, void *, Ptr_hash_function, Ptr_equals); +HashSetDef(Void, void *, Ptr_hash_function, Ptr_equals); #endif diff --git a/src/table.h b/src/table.h index 6e886b7..2bb9805 100644 --- a/src/table.h +++ b/src/table.h @@ -4,7 +4,7 @@ #include "mymemory.h" struct Table { - + }; Table * allocTable(); diff --git a/src/vector.h b/src/vector.h index e9a3361..d131a27 100644 --- a/src/vector.h +++ b/src/vector.h @@ -11,12 +11,13 @@ typedef struct Vector ## name Vector ## name; \ Vector ## name * allocVector ## name(uint capacity); \ Vector ## name * allocDefVector ## name(); \ - Vector ## name * allocVectorArray ## name(type * array, uint capacity); \ + Vector ## name * allocVectorArray ## name(uint capacity, type * array); \ void pushVector ## name(Vector ## name *vector, type item); \ type getVector ## name(Vector ## name *vector, uint index); \ void setVector ## name(Vector ## name *vector, uint index, type item); \ - uint getSize ##name(Vector ##name *vector); \ - void freeVector ##name(Vector ##name *vector); + uint getSizeVector ##name(Vector ##name *vector); \ + void deleteVector ##name(Vector ##name *vector); \ + void clearVector ##name(Vector ## name *vector); #define VectorImpl(name, type, defcap) \ Vector ## name * allocDefVector ## name() { \ @@ -47,11 +48,14 @@ void setVector ## name(Vector ## name * vector, uint index, type item) { \ vector->array[index]=item; \ } \ - uint getSize ## name(Vector ## name *vector) { \ + uint getSizeVector ## name(Vector ## name *vector) { \ return vector->size; \ } \ - void freeVector ##name(Vector ##name *vector) { \ + void deleteVector ##name(Vector ##name *vector) { \ ourfree(vector->array); \ ourfree(vector); \ + } \ + void clearVector ##name(Vector ## name *vector) { \ + vector->size=0; \ } #endif