From 561b93dec85db0c90426345c0dc669fe3de2d4f7 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sat, 17 Jun 2017 00:11:57 -0700 Subject: [PATCH] Fix some things that C++ doesn't like so we don't lose the possibility to use the C++ compiler in the future --- src/AST/boolean.c | 8 +- src/AST/boolean.h | 4 +- src/AST/element.c | 4 +- src/AST/element.h | 2 +- src/AST/function.h | 4 +- src/AST/ops.h | 10 +- src/AST/order.c | 2 +- src/AST/order.h | 4 +- src/AST/predicate.c | 4 +- src/AST/predicate.h | 4 +- src/Backend/constraint.c | 230 ++++++++++++++++---------------- src/Backend/constraint.h | 2 +- src/Backend/inc_solver.c | 124 ++++++++--------- src/Backend/inc_solver.h | 28 ++-- src/Collections/hashtable.h | 2 +- src/Encoders/elementencoding.c | 26 ++-- src/Encoders/elementencoding.h | 2 +- src/Encoders/functionencoding.c | 20 +-- src/Encoders/functionencoding.h | 2 +- src/classlist.h | 8 -- src/csolver.c | 46 +++---- src/csolver.h | 6 +- 22 files changed, 272 insertions(+), 270 deletions(-) diff --git a/src/AST/boolean.c b/src/AST/boolean.c index d452b1a..7d9aec3 100644 --- a/src/AST/boolean.c +++ b/src/AST/boolean.c @@ -2,20 +2,20 @@ Boolean* allocBoolean(VarType t) { BooleanVar* tmp=(BooleanVar *) ourmalloc(sizeof (BooleanVar)); - tmp->base.btype=BOOLEANVAR; + GETBOOLEANTYPE(tmp)=BOOLEANVAR; tmp->vtype=t; return & tmp->base; } Boolean* allocBooleanOrder(Order* order, uint64_t first, uint64_t second) { BooleanOrder* tmp=(BooleanOrder *) ourmalloc(sizeof (BooleanOrder)); - tmp->base.btype=ORDERCONST; + GETBOOLEANTYPE(tmp)=ORDERCONST; tmp->order=order; tmp->first=first; tmp->second=second; return & tmp -> base; } -void deleteBoolean(Boolean * this) { - ourfree(this); +void deleteBoolean(Boolean * This) { + ourfree(This); } diff --git a/src/AST/boolean.h b/src/AST/boolean.h index 065ba4a..d00a82c 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -8,6 +8,8 @@ This is a little sketchy, but apparently legit. https://www.python.org/dev/peps/pep-3123/ */ +#define GETBOOLEANTYPE(o) (((Boolean *)(o))->btype) + struct Boolean { BooleanType btype; }; @@ -42,6 +44,6 @@ struct BooleanComp { Boolean * allocBoolean(VarType t); Boolean * allocBooleanOrder(Order * order, uint64_t first, uint64_t second); -void deleteBoolean(Boolean * this); +void deleteBoolean(Boolean * This); #endif diff --git a/src/AST/element.c b/src/AST/element.c index 191686c..45117e1 100644 --- a/src/AST/element.c +++ b/src/AST/element.c @@ -6,6 +6,6 @@ Element *allocElement(Set * s) { return tmp; } -void deleteElement(Element *this) { - ourfree(this); +void deleteElement(Element *This) { + ourfree(This); } diff --git a/src/AST/element.h b/src/AST/element.h index 8f0f082..6cbf94c 100644 --- a/src/AST/element.h +++ b/src/AST/element.h @@ -8,5 +8,5 @@ struct Element { }; Element * allocElement(Set *s); -void deleteElement(Element *this); +void deleteElement(Element *This); #endif diff --git a/src/AST/function.h b/src/AST/function.h index 61a6148..459f0b5 100644 --- a/src/AST/function.h +++ b/src/AST/function.h @@ -5,10 +5,10 @@ #include "ops.h" #include "structs.h" struct Function { - enum ArithOp op; + ArithOp op; VectorSet* domains; Set * range; - enum OverFlowBehavior overflowbehavior; + OverFlowBehavior overflowbehavior; Table* table; }; #endif diff --git a/src/AST/ops.h b/src/AST/ops.h index 7fdf2f3..3541808 100644 --- a/src/AST/ops.h +++ b/src/AST/ops.h @@ -1,9 +1,16 @@ #ifndef OPS_H #define OPS_H enum LogicOp {AND, OR, NOT, XOR, IMPLIES}; +typedef enum LogicOp LogicOp; + enum ArithOp {ADD, SUB}; +typedef enum ArithOp ArithOp; + enum CompOp {EQUALS}; +typedef enum CompOp CompOp; + enum OrderType {PARTIAL, TOTAL}; +typedef enum OrderType OrderType; /** * FLAGFORCESOVERFLOW forces the operation to overflow if the boolean flag is true @@ -14,7 +21,8 @@ enum OrderType {PARTIAL, TOTAL}; * NOOVERFLOW -- client has ensured that overflow is impossible */ enum OverFlowBehavior {IGNORE, WRAPAROUND, FLAGFORCESOVERFLOW, OVERFLOWSETSFLAG, FLAGIFFOVERFLOW, NOOVERFLOW}; +typedef enum OverFlowBehavior OverFlowBehavior; enum BooleanType {ORDERCONST, BOOLEANVAR, LOGICOP, COMPARE}; - +typedef enum BooleanType BooleanType; #endif diff --git a/src/AST/order.c b/src/AST/order.c index dd233b6..c18e039 100644 --- a/src/AST/order.c +++ b/src/AST/order.c @@ -3,7 +3,7 @@ #include "set.h" -Order* allocOrder(enum OrderType type, Set * set){ +Order* allocOrder(OrderType type, Set * set){ Order* order = (Order*)ourmalloc(sizeof(Order)); order->set=set; order->constraints = allocDefVectorBoolean(); diff --git a/src/AST/order.h b/src/AST/order.h index 2bb13b2..727098b 100644 --- a/src/AST/order.h +++ b/src/AST/order.h @@ -5,11 +5,11 @@ #include "structs.h" #include "ops.h" struct Order { - enum OrderType type; + OrderType type; Set * set; VectorBoolean* constraints; }; -Order* allocOrder(enum OrderType type, Set * set); +Order* allocOrder(OrderType type, Set * set); Boolean* getOrderConstraint(Order* order,uint64_t first, uint64_t second); #endif diff --git a/src/AST/predicate.c b/src/AST/predicate.c index 2beef61..09adb1b 100644 --- a/src/AST/predicate.c +++ b/src/AST/predicate.c @@ -2,11 +2,11 @@ #include "structs.h" -Predicate* allocPredicate(enum CompOp op, Set ** domain, uint numDomain){ +Predicate* allocPredicate(CompOp op, Set ** domain, uint numDomain){ Predicate* predicate = (Predicate*) ourmalloc(sizeof(Predicate)); predicate->domains = allocDefVectorSet(); for(uint i=0; idomains,domain[i]); predicate->op=op; return predicate; -} \ No newline at end of file +} diff --git a/src/AST/predicate.h b/src/AST/predicate.h index a4dd7ed..5d23764 100644 --- a/src/AST/predicate.h +++ b/src/AST/predicate.h @@ -6,10 +6,10 @@ #include "structs.h" struct Predicate { - enum CompOp op; + CompOp op; VectorSet* domains; }; -Predicate* allocPredicate(enum CompOp op, Set ** domain, uint numDomain); +Predicate* allocPredicate(CompOp op, Set ** domain, uint numDomain); #endif diff --git a/src/Backend/constraint.c b/src/Backend/constraint.c index 8b38540..1aa3d3c 100644 --- a/src/Backend/constraint.c +++ b/src/Backend/constraint.c @@ -15,67 +15,67 @@ Constraint ctrue={TRUE, 0xffffffff, NULL, NULL}; Constraint cfalse={FALSE, 0xffffffff, NULL, 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; + 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 { - this->operands[0]=l; + This->operands[0]=l; // } - this->operands[1]=r; - return this; + This->operands[1]=r; + return This; } 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 *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 * 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 *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 * 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 *This=(Constraint *) ourmalloc(sizeof(Constraint)); + This->type=t; + This->numoperandsorvar=v; + This->operands=NULL; + This->neg=NULL; + return This; } -void deleteConstraint(Constraint *this) { - if (this->operands!=NULL) - ourfree(this->operands); +void deleteConstraint(Constraint *This) { + if (This->operands!=NULL) + ourfree(This->operands); } -void dumpConstraint(Constraint * this, IncrementalSolver *solver) { - if (this->type==VAR) { - addClauseLiteral(solver, this->numoperandsorvar); +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); + } else if (This->type==NOTVAR) { + addClauseLiteral(solver, -This->numoperandsorvar); addClauseLiteral(solver, 0); } else { - ASSERT(this->type==OR); - for(uint i=0;inumoperandsorvar;i++) { - Constraint *c=this->operands[i]; + ASSERT(This->type==OR); + for(uint i=0;inumoperandsorvar;i++) { + Constraint *c=This->operands[i]; if (c->type==VAR) { addClauseLiteral(solver, c->numoperandsorvar); } else if (c->type==NOTVAR) { @@ -86,8 +86,8 @@ void dumpConstraint(Constraint * this, IncrementalSolver *solver) { } } -void internalfreeConstraint(Constraint * this) { - switch(this->type) { +void internalfreeConstraint(Constraint * This) { + switch(This->type) { case TRUE: case FALSE: case NOTVAR: @@ -96,13 +96,13 @@ void internalfreeConstraint(Constraint * this) { case BOGUS: ASSERT(0); default: - this->type=BOGUS; - ourfree(this); + This->type=BOGUS; + ourfree(This); } } -void freerecConstraint(Constraint *this) { - switch(this->type) { +void freerecConstraint(Constraint *This) { + switch(This->type) { case TRUE: case FALSE: case NOTVAR: @@ -111,18 +111,18 @@ void freerecConstraint(Constraint *this) { case BOGUS: ASSERT(0); default: - if (this->operands!=NULL) { - for(uint i=0;inumoperandsorvar;i++) - freerecConstraint(this->operands[i]); + if (This->operands!=NULL) { + for(uint i=0;inumoperandsorvar;i++) + freerecConstraint(This->operands[i]); } - this->type=BOGUS; - deleteConstraint(this); + This->type=BOGUS; + deleteConstraint(This); } } -void printConstraint(Constraint * this) { - switch(this->type) { +void printConstraint(Constraint * This) { + switch(This->type) { case TRUE: model_print("true"); break; @@ -131,54 +131,54 @@ void printConstraint(Constraint * this) { break; case IMPLIES: model_print("("); - printConstraint(this->operands[0]); + printConstraint(This->operands[0]); model_print(")"); model_print("=>"); model_print("("); - printConstraint(this->operands[1]); + printConstraint(This->operands[1]); model_print(")"); break; case AND: case OR: model_print("("); - for(uint i=0;inumoperandsorvar;i++) { + for(uint i=0;inumoperandsorvar;i++) { if (i!=0) { - if (this->type==AND) + if (This->type==AND) model_print(" ^ "); else model_print(" v "); } - printConstraint(this->operands[i]); + printConstraint(This->operands[i]); } model_print(")"); break; case VAR: - model_print("t%u",this->numoperandsorvar); + model_print("t%u",This->numoperandsorvar); break; case NOTVAR: - model_print("!t%u",this->numoperandsorvar); + model_print("!t%u",This->numoperandsorvar); break; default: ASSERT(0); } } -Constraint * cloneConstraint(Constraint * this) { - switch(this->type) { +Constraint * cloneConstraint(Constraint * This) { + switch(This->type) { case TRUE: case FALSE: case VAR: case NOTVAR: - return this; + return This; case IMPLIES: - return allocConstraint(IMPLIES, cloneConstraint(this->operands[0]), cloneConstraint(this->operands[1])); + return allocConstraint(IMPLIES, cloneConstraint(This->operands[0]), cloneConstraint(This->operands[1])); case AND: case OR: { - Constraint *array[this->numoperandsorvar]; - for(uint i=0;inumoperandsorvar;i++) { - array[i]=cloneConstraint(this->operands[i]); + Constraint *array[This->numoperandsorvar]; + for(uint i=0;inumoperandsorvar;i++) { + array[i]=cloneConstraint(This->operands[i]); } - return allocArrayConstraint(this->type, this->numoperandsorvar, array); + return allocArrayConstraint(This->type, This->numoperandsorvar, array); } default: ASSERT(0); @@ -260,107 +260,107 @@ bool mergeandfree(VectorConstraint * to, VectorConstraint * from) { return false; } -VectorConstraint * simplifyConstraint(Constraint * this) { - switch(this->type) { +VectorConstraint * simplifyConstraint(Constraint * This) { + switch(This->type) { case TRUE: case VAR: case NOTVAR: case FALSE: { VectorConstraint * vec=allocDefVectorConstraint(); - pushVectorConstraint(vec, this); + pushVectorConstraint(vec, This); return vec; } case AND: { VectorConstraint *vec=allocDefVectorConstraint(); - for(uint i=0;inumoperandsorvar;i++) { - VectorConstraint * subvec=simplifyConstraint(this->operands[i]); + for(uint i=0;inumoperandsorvar;i++) { + VectorConstraint * subvec=simplifyConstraint(This->operands[i]); if (mergeandfree(vec, subvec)) { - for(uint j=i+1;jnumoperandsorvar;j++) { - freerecConstraint(this->operands[j]); + for(uint j=i+1;jnumoperandsorvar;j++) { + freerecConstraint(This->operands[j]); } - internalfreeConstraint(this); + internalfreeConstraint(This); return vec; } } - internalfreeConstraint(this); + internalfreeConstraint(This); return vec; } case OR: { - for(uint i=0;inumoperandsorvar;i++) { - Constraint *c=this->operands[i]; + for(uint i=0;inumoperandsorvar;i++) { + Constraint *c=This->operands[i]; switch(c->type) { case TRUE: { VectorConstraint * vec=allocDefVectorConstraint(); pushVectorConstraint(vec, c); - freerecConstraint(this); + freerecConstraint(This); return vec; } case FALSE: { - Constraint *array[this->numoperandsorvar-1]; + Constraint *array[This->numoperandsorvar-1]; uint index=0; - for(uint j=0;jnumoperandsorvar;j++) { + for(uint j=0;jnumoperandsorvar;j++) { if (j!=i) - array[index++]=this->operands[j]; + array[index++]=This->operands[j]; } Constraint *cn=allocArrayConstraint(OR, index, array); VectorConstraint *vec=simplifyConstraint(cn); - internalfreeConstraint(this); + internalfreeConstraint(This); return vec; } case VAR: case NOTVAR: break; case OR: { - uint nsize=this->numoperandsorvar+c->numoperandsorvar-1; + uint nsize=This->numoperandsorvar+c->numoperandsorvar-1; Constraint *array[nsize]; uint index=0; - for(uint j=0;jnumoperandsorvar;j++) + for(uint j=0;jnumoperandsorvar;j++) if (j!=i) - array[index++]=this->operands[j]; + array[index++]=This->operands[j]; for(uint j=0;jnumoperandsorvar;j++) array[index++]=c->operands[j]; Constraint *cn=allocArrayConstraint(OR, nsize, array); VectorConstraint *vec=simplifyConstraint(cn); - internalfreeConstraint(this); + internalfreeConstraint(This); internalfreeConstraint(c); return vec; } case IMPLIES: { - uint nsize=this->numoperandsorvar+1; + uint nsize=This->numoperandsorvar+1; Constraint *array[nsize]; uint index=0; - for(uint j=0;jnumoperandsorvar;j++) + for(uint j=0;jnumoperandsorvar;j++) if (j!=i) - array[index++]=this->operands[j]; + array[index++]=This->operands[j]; array[index++]=negateConstraint(c->operands[0]); array[index++]=c->operands[1]; Constraint *cn=allocArrayConstraint(OR, nsize, array); VectorConstraint *vec=simplifyConstraint(cn); - internalfreeConstraint(this); + internalfreeConstraint(This); internalfreeConstraint(c); return vec; } case AND: { - Constraint *array[this->numoperandsorvar]; + Constraint *array[This->numoperandsorvar]; VectorConstraint *vec=allocDefVectorConstraint(); for(uint j=0;jnumoperandsorvar;j++) { //copy other elements - for(uint k=0;knumoperandsorvar;k++) { + for(uint k=0;knumoperandsorvar;k++) { if (k!=i) { - array[k]=cloneConstraint(this->operands[k]); + array[k]=cloneConstraint(This->operands[k]); } } array[i]=cloneConstraint(c->operands[j]); - Constraint *cn=allocArrayConstraint(OR, this->numoperandsorvar, array); + Constraint *cn=allocArrayConstraint(OR, This->numoperandsorvar, array); VectorConstraint * newvec=simplifyConstraint(cn); if (mergeandfree(vec, newvec)) { - freerecConstraint(this); + freerecConstraint(This); return vec; } } - freerecConstraint(this); + freerecConstraint(This); return vec; } default: @@ -369,18 +369,18 @@ VectorConstraint * simplifyConstraint(Constraint * this) { //continue on to next item } VectorConstraint * vec=allocDefVectorConstraint(); - if (this->numoperandsorvar==1) { - Constraint *c=this->operands[0]; - freerecConstraint(this); + if (This->numoperandsorvar==1) { + Constraint *c=This->operands[0]; + freerecConstraint(This); pushVectorConstraint(vec, c); } else - pushVectorConstraint(vec, this); + pushVectorConstraint(vec, This); return vec; } case IMPLIES: { - Constraint *cn=allocConstraint(OR, negateConstraint(this->operands[0]), this->operands[1]); + Constraint *cn=allocConstraint(OR, negateConstraint(This->operands[0]), This->operands[1]); VectorConstraint * vec=simplifyConstraint(cn); - internalfreeConstraint(this); + internalfreeConstraint(This); return vec; } default: @@ -389,29 +389,29 @@ VectorConstraint * simplifyConstraint(Constraint * this) { } } -Constraint * negateConstraint(Constraint * this) { - switch(this->type) { +Constraint * negateConstraint(Constraint * This) { + switch(This->type) { case TRUE: return &cfalse; case FALSE: return &ctrue; case NOTVAR: case VAR: - return this->neg; + return This->neg; case IMPLIES: { - Constraint *l=this->operands[0]; - Constraint *r=this->operands[1]; - this->operands[0]=r; - this->operands[1]=l; - return this; + 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;inumoperandsorvar;i++) { - this->operands[i]=negateConstraint(this->operands[i]); + for(uint i=0;inumoperandsorvar;i++) { + This->operands[i]=negateConstraint(This->operands[i]); } - this->type=(this->type==AND) ? OR : AND; - return this; + This->type=(This->type==AND) ? OR : AND; + return This; } default: ASSERT(0); diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h index 06bb1d1..4b59812 100644 --- a/src/Backend/constraint.h +++ b/src/Backend/constraint.h @@ -41,7 +41,7 @@ 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;} +void setNegConstraint(Constraint * This, Constraint *c) {This->neg=c;} Constraint *negateConstraint(Constraint * c); extern Constraint ctrue; diff --git a/src/Backend/inc_solver.c b/src/Backend/inc_solver.c index c25cfba..5e1ed54 100644 --- a/src/Backend/inc_solver.c +++ b/src/Backend/inc_solver.c @@ -13,83 +13,83 @@ #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 *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; } -void deleteIncrementalSolver(IncrementalSolver * this) { - killSolver(this); - ourfree(this->buffer); - if (this->solution != NULL) - ourfree(this->solution); +void deleteIncrementalSolver(IncrementalSolver * This) { + killSolver(This); + ourfree(This->buffer); + if (This->solution != NULL) + ourfree(This->solution); } -void resetSolver(IncrementalSolver * this) { - killSolver(this); - this->offset = 0; - createSolver(this); +void resetSolver(IncrementalSolver * This) { + killSolver(This); + This->offset = 0; + createSolver(This); } -void addClauseLiteral(IncrementalSolver * this, int literal) { - this->buffer[this->offset++]=literal; - if (this->offset==IS_BUFFERSIZE) { - flushBufferSolver(this); +void addClauseLiteral(IncrementalSolver * This, int literal) { + This->buffer[This->offset++]=literal; + if (This->offset==IS_BUFFERSIZE) { + flushBufferSolver(This); } } -void finishedClauses(IncrementalSolver * this) { - addClauseLiteral(this, 0); +void finishedClauses(IncrementalSolver * This) { + addClauseLiteral(This, 0); } -void freeze(IncrementalSolver * this, int variable) { - addClauseLiteral(this, IS_FREEZE); - addClauseLiteral(this, variable); +void freeze(IncrementalSolver * This, int variable) { + addClauseLiteral(This, IS_FREEZE); + addClauseLiteral(This, variable); } -int solve(IncrementalSolver * this) { +int solve(IncrementalSolver * This) { //add an empty clause - startSolve(this); - return getSolution(this); + startSolve(This); + return getSolution(This); } -void startSolve(IncrementalSolver *this) { - addClauseLiteral(this, IS_RUNSOLVER); - flushBufferSolver(this); +void startSolve(IncrementalSolver *This) { + addClauseLiteral(This, IS_RUNSOLVER); + flushBufferSolver(This); } -int getSolution(IncrementalSolver * this) { - int result=readIntSolver(this); +int getSolution(IncrementalSolver * This) { + int result=readIntSolver(This); if (result == IS_SAT) { - 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; + 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(this, &this->solution[1], numVars * sizeof(int)); + readSolver(This, &This->solution[1], numVars * sizeof(int)); } return result; } -int readIntSolver(IncrementalSolver * this) { +int readIntSolver(IncrementalSolver * This) { int value; - readSolver(this, &value, 4); + readSolver(This, &value, 4); return value; } -void readSolver(IncrementalSolver * this, 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(this->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); @@ -99,22 +99,22 @@ void readSolver(IncrementalSolver * this, void * tmp, ssize_t size) { } while(bytestoread != 0); } -bool getValueSolver(IncrementalSolver * this, int variable) { - return this->solution[variable]; +bool getValueSolver(IncrementalSolver * This, int variable) { + return This->solution[variable]; } -void createSolver(IncrementalSolver * this) { +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 ((this->solver_pid = fork()) == -1) { + if ((This->solver_pid = fork()) == -1) { model_print("Error forking.\n"); exit(-1); } - if (this->solver_pid == 0) { + if (This->solver_pid == 0) { //Solver process close(to_pipe[1]); close(from_pipe[0]); @@ -131,36 +131,36 @@ void createSolver(IncrementalSolver * this) { close(fd); } else { //Our process - this->to_solver_fd = to_pipe[1]; - this->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 killSolver(IncrementalSolver * this) { - close(this->to_solver_fd); - close(this->from_solver_fd); +void killSolver(IncrementalSolver * This) { + close(This->to_solver_fd); + close(This->from_solver_fd); //Stop the solver - if (this->solver_pid > 0) { + if (This->solver_pid > 0) { int status; - kill(this->solver_pid, SIGKILL); - waitpid(this->solver_pid, &status, 0); + kill(This->solver_pid, SIGKILL); + waitpid(This->solver_pid, &status, 0); } } -void flushBufferSolver(IncrementalSolver * this) { - ssize_t bytestowrite=sizeof(int)*this->offset; +void flushBufferSolver(IncrementalSolver * This) { + ssize_t bytestowrite=sizeof(int)*This->offset; ssize_t byteswritten=0; do { - ssize_t n=write(this->to_solver_fd, &((char *)this->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",this->to_solver_fd); + model_print("to_solver_fd=%d\n",This->to_solver_fd); exit(-1); } bytestowrite -= n; byteswritten += n; } while(bytestowrite != 0); - this->offset = 0; + This->offset = 0; } diff --git a/src/Backend/inc_solver.h b/src/Backend/inc_solver.h index ead727f..15e5def 100644 --- a/src/Backend/inc_solver.h +++ b/src/Backend/inc_solver.h @@ -29,18 +29,18 @@ struct IncrementalSolver { }; 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); +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/Collections/hashtable.h b/src/Collections/hashtable.h index c9ea34f..8bb5cc2 100644 --- a/src/Collections/hashtable.h +++ b/src/Collections/hashtable.h @@ -24,7 +24,7 @@ * @brief A simple, custom hash table * * By default it is model_malloc, but you can pass in your own allocation - * functions. Note that this table does not support the value 0 (NULL) used as + * functions. Note that This table does not support the value 0 (NULL) used as * a key and is designed primarily with pointer-based keys in mind. Other * primitive key types are supported only for non-zero values. * diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c index 095f99d..a4e2067 100644 --- a/src/Encoders/elementencoding.c +++ b/src/Encoders/elementencoding.c @@ -1,19 +1,19 @@ #include "elementencoding.h" ElementEncoding * allocElementEncoding(ElementEncodingType type, Element *element) { - ElementEncoding * this=(ElementEncoding *)ourmalloc(sizeof(ElementEncoding)); - this->element=element; - this->type=type; - this->variables=NULL; - this->encodingArray=NULL; - this->numVars=0; - return this; + ElementEncoding * This=(ElementEncoding *)ourmalloc(sizeof(ElementEncoding)); + This->element=element; + This->type=type; + This->variables=NULL; + This->encodingArray=NULL; + This->numVars=0; + return This; } -void deleteElementEncoding(ElementEncoding *this) { - if (this->variables!=NULL) - ourfree(this->variables); - if (this->encodingArray!=NULL) - ourfree(this->encodingArray); - ourfree(this); +void deleteElementEncoding(ElementEncoding *This) { + if (This->variables!=NULL) + ourfree(This->variables); + if (This->encodingArray!=NULL) + ourfree(This->encodingArray); + ourfree(This); } diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h index eb20f2b..08fb85e 100644 --- a/src/Encoders/elementencoding.h +++ b/src/Encoders/elementencoding.h @@ -17,5 +17,5 @@ struct ElementEncoding { }; ElementEncoding * allocElementEncoding(ElementEncodingType type, Element *element); -void deleteElementEncoding(ElementEncoding *this); +void deleteElementEncoding(ElementEncoding *This); #endif diff --git a/src/Encoders/functionencoding.c b/src/Encoders/functionencoding.c index 887972b..282912d 100644 --- a/src/Encoders/functionencoding.c +++ b/src/Encoders/functionencoding.c @@ -1,19 +1,19 @@ #include "functionencoding.h" FunctionEncoding * allocFunctionEncoding(FunctionEncodingType type, Element *function) { - FunctionEncoding * this=(FunctionEncoding *)ourmalloc(sizeof(FunctionEncoding)); - this->op.function=function; - this->type=type; - return this; + FunctionEncoding * This=(FunctionEncoding *)ourmalloc(sizeof(FunctionEncoding)); + This->op.function=function; + This->type=type; + return This; } FunctionEncoding * allocPredicateEncoding(FunctionEncodingType type, Boolean *predicate) { - FunctionEncoding * this=(FunctionEncoding *)ourmalloc(sizeof(FunctionEncoding)); - this->op.predicate=predicate; - this->type=type; - return this; + FunctionEncoding * This=(FunctionEncoding *)ourmalloc(sizeof(FunctionEncoding)); + This->op.predicate=predicate; + This->type=type; + return This; } -void deleteFunctionEncoding(FunctionEncoding *this) { - ourfree(this); +void deleteFunctionEncoding(FunctionEncoding *This) { + ourfree(This); } diff --git a/src/Encoders/functionencoding.h b/src/Encoders/functionencoding.h index 4cd5c86..63583b6 100644 --- a/src/Encoders/functionencoding.h +++ b/src/Encoders/functionencoding.h @@ -23,5 +23,5 @@ struct FunctionEncoding { FunctionEncoding * allocFunctionEncoding(FunctionEncodingType type, Element *function); FunctionEncoding * allocPredicateEncoding(FunctionEncodingType type, Boolean *predicate); -void deleteFunctionEncoding(FunctionEncoding *this); +void deleteFunctionEncoding(FunctionEncoding *This); #endif diff --git a/src/classlist.h b/src/classlist.h index f722a6e..d232592 100644 --- a/src/classlist.h +++ b/src/classlist.h @@ -62,14 +62,6 @@ typedef struct FunctionEncoding FunctionEncoding; struct TableEntry; typedef struct TableEntry TableEntry; - -typedef enum ArithOp ArithOp; -typedef enum LogicOp LogicOp; -typedef enum CompOp CompOp; -typedef enum OrderType OrderType; -typedef enum BooleanType BooleanType; -typedef enum OverFlowBehavior OverFlowBehavior; - typedef unsigned int uint; typedef uint64_t VarType; #endif diff --git a/src/csolver.c b/src/csolver.c index 03a0473..7179222 100644 --- a/src/csolver.c +++ b/src/csolver.c @@ -20,47 +20,47 @@ CSolver * allocCSolver() { /** This function tears down the solver and the entire AST */ -void deleteSolver(CSolver *this) { - deleteVectorBoolean(this->constraints); +void deleteSolver(CSolver *This) { + deleteVectorBoolean(This->constraints); - uint size=getSizeVectorBoolean(this->allBooleans); + uint size=getSizeVectorBoolean(This->allBooleans); for(uint i=0;iallBooleans, i)); + deleteBoolean(getVectorBoolean(This->allBooleans, i)); } - deleteVectorBoolean(this->allBooleans); + deleteVectorBoolean(This->allBooleans); - size=getSizeVectorSet(this->allSets); + size=getSizeVectorSet(This->allSets); for(uint i=0;iallSets, i)); + deleteSet(getVectorSet(This->allSets, i)); } - deleteVectorSet(this->allSets); + deleteVectorSet(This->allSets); - size=getSizeVectorElement(this->allElements); + size=getSizeVectorElement(This->allElements); for(uint i=0;iallElements, i)); + deleteElement(getVectorElement(This->allElements, i)); } //FIXME: Freeing alltables and allpredicates - deleteVectorElement(this->allElements); - ourfree(this); + deleteVectorElement(This->allElements); + ourfree(This); } -Set * createSet(CSolver * this, VarType type, uint64_t * elements, uint numelements) { +Set * createSet(CSolver * This, VarType type, uint64_t * elements, uint numelements) { Set * set=allocSet(type, elements, numelements); - pushVectorSet(this->allSets, set); + pushVectorSet(This->allSets, set); return set; } -Set * createRangeSet(CSolver * this, VarType type, uint64_t lowrange, uint64_t highrange) { +Set * createRangeSet(CSolver * This, VarType type, uint64_t lowrange, uint64_t highrange) { Set * set=allocSetRange(type, lowrange, highrange); - pushVectorSet(this->allSets, set); + pushVectorSet(This->allSets, set); return set; } -MutableSet * createMutableSet(CSolver * this, VarType type) { +MutableSet * createMutableSet(CSolver * This, VarType type) { MutableSet * set=allocMutableSet(type); - pushVectorSet(this->allSets, set); + pushVectorSet(This->allSets, set); return set; } @@ -74,9 +74,9 @@ uint64_t createUniqueItem(CSolver *solver, MutableSet * set) { return element; } -Element * getElementVar(CSolver *this, Set * set) { +Element * getElementVar(CSolver *This, Set * set) { Element * element=allocElement(set); - pushVectorElement(this->allElements, element); + pushVectorElement(This->allElements, element); return element; } @@ -91,7 +91,7 @@ Function * createFunctionOperator(CSolver *solver, ArithOp op, Set ** domain, ui return NULL; } -Predicate * createPredicateOperator(CSolver *solver, enum CompOp op, Set ** domain, uint numDomain) { +Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, uint numDomain) { Predicate* predicate= allocPredicate(op, domain,numDomain); pushVectorPredicate(solver->allPredicates, predicate); return predicate; @@ -123,8 +123,8 @@ Boolean * applyLogicalOperation(CSolver *solver, LogicOp op, Boolean ** array) { return NULL; } -void addBoolean(CSolver *this, Boolean * constraint) { - pushVectorBoolean(this->constraints, constraint); +void addBoolean(CSolver *This, Boolean * constraint) { + pushVectorBoolean(This->constraints, constraint); } Order * createOrder(CSolver *solver, OrderType type, Set * set) { diff --git a/src/csolver.h b/src/csolver.h index aedef93..d2e715c 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -61,7 +61,7 @@ Function * createFunctionOperator(CSolver *solver, ArithOp op, Set ** domain, ui /** This function creates a predicate operator. */ -Predicate * createPredicateOperator(CSolver *solver, enum CompOp op, Set ** domain, uint numDomain); +Predicate * createPredicateOperator(CSolver *solver, CompOp op, Set ** domain, uint numDomain); /** This function creates an empty instance table.*/ @@ -85,7 +85,7 @@ Boolean * applyPredicate(CSolver *, Predicate * predicate, Element ** inputs); /** This function applies a logical operation to the Booleans in its input. */ -Boolean * applyLogicalOperation(CSolver *, enum LogicOp op, Boolean ** array); +Boolean * applyLogicalOperation(CSolver *, LogicOp op, Boolean ** array); /** This function adds a boolean constraint to the set of constraints to be satisfied */ @@ -93,7 +93,7 @@ Boolean * applyLogicalOperation(CSolver *, enum LogicOp op, Boolean ** array); void addBoolean(CSolver *, Boolean * constraint); /** This function instantiates an order of type type over the set set. */ -Order * createOrder(CSolver *, enum OrderType type, Set * set); +Order * createOrder(CSolver *, OrderType type, Set * set); /** This function instantiates a boolean on two items in an order. */ Boolean * orderConstraint(CSolver *, Order * order, uint64_t first, uint64_t second); -- 2.34.1