Fix some things that C++ doesn't like so we don't lose the possibility to use the...

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index d452b1a27e981a6c19627a15a8dd6b9bab237c83..7d9aec39f8bac6e042b0bb76b415ee189e2bd5c2 100644 (file)
--- 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 065ba4ac2590696b7a107e1214019aff795c5c91..d00a82cf123fa325eb1d2eadef911272df66302d 100644 (file)
--- 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 191686cec460d17e1eb8ce2d0136515ab5bcf3a5..45117e1dccf6abc9f05958eea6d12badd79610a1 100644 (file)
--- 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 8f0f0826548f314de74c2330fef547436677958a..6cbf94cef1cb6d9a75d3ce3bc4da737659c00110 100644 (file)
--- 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 61a6148fb9a568d380a42e1d073a4096401e5a48..459f0b55d3b3c8ee1c2195b7ef173f048d27cac0 100644 (file)
--- 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 7fdf2f300b41a0e42c7780aaf34f05a438b475ab..35418088be0ff31e624a3f72fbcf2acf650a42f4 100644 (file)
--- 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 dd233b644bd2964e2566d83019897b470f167dbc..c18e039f11347eb38a617b4c72e6d0ddae30d443 100644 (file)
--- 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 2bb13b248ee5898e87cea4cbb06da489f0ea6597..727098b6053373ec78d87a058c885ed4b2eadf3f 100644 (file)
--- 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 2beef617d2c5ec9a5b1dee7c7289ccd79c14d14a..09adb1b07b1f2ec769479dd4bc8716f09b4a4abf 100644 (file)
--- 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; i<numDomain; i++)
         pushVectorSet(predicate->domains,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 a4dd7ed12a145b483c812133b6b5fcd95d45a0c7..5d23764847a39361833e6126eb3e69251ff108ca 100644 (file)
--- 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 8b38540a59657bdca7b90bee60ed100a1aca9a3d..1aa3d3cc9b5f22d90498dcbd0ad915b0e8ab928d 100644 (file)
--- 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;i<this->numoperandsorvar;i++) {
-                       Constraint *c=this->operands[i];
+               ASSERT(This->type==OR);
+               for(uint i=0;i<This->numoperandsorvar;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;i<this->numoperandsorvar;i++)
-                               freerecConstraint(this->operands[i]);
+               if (This->operands!=NULL) {
+                       for(uint i=0;i<This->numoperandsorvar;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;i<this->numoperandsorvar;i++) {
+               for(uint i=0;i<This->numoperandsorvar;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;i<this->numoperandsorvar;i++) {
-                       array[i]=cloneConstraint(this->operands[i]);
+               Constraint *array[This->numoperandsorvar];
+               for(uint i=0;i<This->numoperandsorvar;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;i<this->numoperandsorvar;i++) {
-                       VectorConstraint * subvec=simplifyConstraint(this->operands[i]);
+               for(uint i=0;i<This->numoperandsorvar;i++) {
+                       VectorConstraint * subvec=simplifyConstraint(This->operands[i]);
                        if (mergeandfree(vec, subvec)) {
-                               for(uint j=i+1;j<this->numoperandsorvar;j++) {
-                                       freerecConstraint(this->operands[j]);
+                               for(uint j=i+1;j<This->numoperandsorvar;j++) {
+                                       freerecConstraint(This->operands[j]);
                                }
-                               internalfreeConstraint(this);
+                               internalfreeConstraint(This);
                                return vec;
                        }
                }
-               internalfreeConstraint(this);
+               internalfreeConstraint(This);
                return vec;
        }
        case OR: {
-               for(uint i=0;i<this->numoperandsorvar;i++) {
-                       Constraint *c=this->operands[i];
+               for(uint i=0;i<This->numoperandsorvar;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;j<this->numoperandsorvar;j++) {
+                               for(uint j=0;j<This->numoperandsorvar;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;j<this->numoperandsorvar;j++)
+                               for(uint j=0;j<This->numoperandsorvar;j++)
                                        if (j!=i)
-                                               array[index++]=this->operands[j];
+                                               array[index++]=This->operands[j];
                                for(uint j=0;j<c->numoperandsorvar;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;j<this->numoperandsorvar;j++)
+                               for(uint j=0;j<This->numoperandsorvar;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;j<c->numoperandsorvar;j++) {
                                        //copy other elements
-                                       for(uint k=0;k<this->numoperandsorvar;k++) {
+                                       for(uint k=0;k<This->numoperandsorvar;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;i<this->numoperandsorvar;i++) {
-                       this->operands[i]=negateConstraint(this->operands[i]);
+               for(uint i=0;i<This->numoperandsorvar;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 06bb1d18f74488a6e3da4b760d45120edad2faa2..4b59812d91fe1c5b0ea95e05bd1d58b63c9ae303 100644 (file)
--- 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 c25cfba9c870fa883e475112a48ba4edb3f396e2..5e1ed548ab31e487d958bc1fb293c840ffc0533b 100644 (file)
--- 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 ead727fba25395146b7ae64fa57e3d0d8d91bc9c..15e5def4ccd8c498f7bca94694bf3b01938205bb 100644 (file)
--- 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 c9ea34fee387295b614247267ad4de14574922ae..8bb5cc29e38f084af9aab49ade951030fb2718a7 100644 (file)
--- 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 095f99ded848dc8dc3d4316b951a0eef971de42e..a4e206762ef11b7bf8669a67e176feb7c451f71a 100644 (file)
--- 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 eb20f2b865853a948626f3033e861a092b667df0..08fb85e7dab28544d008d2c2e3238fca35ecff84 100644 (file)
--- 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 887972bc46d588fe5318c5b7d19912e871f4a603..282912d2d09e6df861fbea1e5468921babcfd589 100644 (file)
--- 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 4cd5c86b138636e475c30b16211cc0a577f047cc..63583b64cf2148620a453b43b68469b7fe53aa30 100644 (file)
--- 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 f722a6e2331218e81535f978bd61a5eacdbddac9..d232592fef332c3d58cbe6670569f3e03ce0cfe0 100644 (file)
--- 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 03a0473d15c5b51ea8ce8cdaddd5333fd3169604..7179222096c54ab17af4cb31b5f2ec50e74659b8 100644 (file)
--- 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;i<size;i++) {
-               deleteBoolean(getVectorBoolean(this->allBooleans, i));
+               deleteBoolean(getVectorBoolean(This->allBooleans, i));
        }
 
-       deleteVectorBoolean(this->allBooleans);
+       deleteVectorBoolean(This->allBooleans);
 
-       size=getSizeVectorSet(this->allSets);
+       size=getSizeVectorSet(This->allSets);
        for(uint i=0;i<size;i++) {
-               deleteSet(getVectorSet(this->allSets, i));
+               deleteSet(getVectorSet(This->allSets, i));
        }
 
-       deleteVectorSet(this->allSets);
+       deleteVectorSet(This->allSets);
 
-       size=getSizeVectorElement(this->allElements);
+       size=getSizeVectorElement(This->allElements);
        for(uint i=0;i<size;i++) {
-               deleteElement(getVectorElement(this->allElements, 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 aedef9391ea27c586b5b838e38c1cbf21611cb5a..d2e715c06f793e18a10b5181df19c15b92b8b18e 100644 (file)
--- 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);