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
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
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)
debug: all
PHONY += docs
-docs: *.cc *.h
+docs: *.c *.cc *.h
doxygen
$(LIB_SO): $(OBJECTS)
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)
#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;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);
+ 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:
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;
+ deleteConstraint(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());
+ 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<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);
+ deleteVectorConstraint(from);
return true;
}
- to->push_back(c);
+ pushVectorConstraint(to, c);
}
- delete from;
+ deleteVectorConstraint(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:
#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
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<Constraint *> * 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<Constraint *> * to, ModelVector<Constraint *> * 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
#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;i<size;i++) {
+ deleteSet(getVectorSet(this->sets, i));
+ }
+
+ deleteVectorSet(this->sets);
+
+ size=getSizeVectorElement(this->elements);
+ for(uint i=0;i<size;i++) {
+ deleteElement(getVectorElement(this->elements, 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) {
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) {
#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
tmp->set=s;
return tmp;
}
+
+void deleteElement(Element *this) {
+ ourfree(this);
+}
};
Element * allocElement(Set *s);
+void deleteElement(Element *this);
#endif
#define HASH_SET_H
#include "hashtable.h"
-template<typename _Key>
-struct LinkNode {
- _Key key;
- LinkNode<_Key> *prev;
- LinkNode<_Key> *next;
-};
-
-template<typename _Key, typename _KeyInt, int _Shift, void *
- (* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *), unsigned int (*hash_function
- )(_Key), bool (*equals)(_Key, _Key)>
-class HashSet;
-
-template<typename _Key, typename _KeyInt, int _Shift, void * (* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *), unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, 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<typename _Key, typename _KeyInt, int _Shift = 0, void * (* _malloc)(size_t) = model_malloc, void * (* _calloc)(size_t, size_t) = model_calloc, void (*_free)(void *) = model_free, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, 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
#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<typename _Key, typename _Val>
-struct hashlistnode {
- _Key key;
- _Val val;
-};
-
-template<typename _Key, int _Shift, typename _KeyInt>
-inline unsigned int default_hash_function(_Key hash) {
- return (unsigned int)(((_KeyInt)hash) >> _Shift);
-}
-
-template<typename _Key>
-inline bool default_equals(_Key key1, _Key key2) {
- return key1 == key2;
-}
-
/**
* @brief A simple, custom hash table
*
*
* @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<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, void * (* _malloc)(size_t) = model_malloc, void * (* _calloc)(size_t, size_t) = model_calloc, void (*_free)(void *) = model_free, unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, 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<capacity;i++) {
- struct hashlistnode<_Key, _Val> *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<capacity;i++) {
- struct hashlistnode<_Key, _Val> *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;i<tab->capacity;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__ */
#include "inc_solver.h"
#define SATSOLVER "sat_solver"
#include <fcntl.h>
-
-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);
} 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]);
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;
}
#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;
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
#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);
+}
#define MUTABLESET_H
#include "set.h"
-MutableSet* allocMutableSet(VarType type);
+MutableSet * allocMutableSet(VarType t);
void addElementMSet(MutableSet * set, uint64_t element);
#endif
#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 */
#include <stddef.h>
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;
return tmp;
}
-void freeSet(Set * set) {
- if (set->isRange)
- freeVectorInt(set->members);
+void deleteSet(Set * set) {
+ if (!set->isRange)
+ deleteVectorInt(set->members);
ourfree(set);
}
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 */
#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);
#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
#include "mymemory.h"
struct Table {
-
+
};
Table * allocTable();
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() { \
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
projects / satune.git / commitdiff