From: bdemsky <bdemsky@uci.edu>
Date: Wed, 18 Oct 2017 23:54:43 +0000 (-0700)
Subject: Fix tabbing
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=d8a822b4166c0e1da167d756bc10cffbaded8972

Fix tabbing
---

diff --git a/src/AST/astops.h b/src/AST/astops.h
index ebe9fc0..d4e185d 100644
--- a/src/AST/astops.h
+++ b/src/AST/astops.h
@@ -8,7 +8,7 @@ enum PredicateType {TABLEPRED, OPERATORPRED};
 typedef enum PredicateType PredicateType;
 
 enum ASTNodeType {ORDERCONST, BOOLEANVAR, LOGICOP, PREDICATEOP, BOOLCONST, ELEMSET, ELEMFUNCRETURN, ELEMCONST,
-	BOOLEANEDGE, ORDERTYPE, SETTYPE, PREDTABLETYPE, PREDOPERTYPE, TABLETYPE, FUNCTABLETYPE, FUNCOPTYPE};
+									BOOLEANEDGE, ORDERTYPE, SETTYPE, PREDTABLETYPE, PREDOPERTYPE, TABLETYPE, FUNCTABLETYPE, FUNCOPTYPE};
 typedef enum ASTNodeType ASTNodeType;
 
 enum Polarity {P_UNDEFINED=0, P_TRUE=1, P_FALSE=2, P_BOTHTRUEFALSE=3};
diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index fff3658..f7d3e88 100644
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -47,9 +47,9 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uin
 }
 
 BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e) {
-	bool isnegated=e.isNegated();
-	Boolean *b=e->clone(solver, map);
-	BooleanEdge be=BooleanEdge(b);
+	bool isnegated = e.isNegated();
+	Boolean *b = e->clone(solver, map);
+	BooleanEdge be = BooleanEdge(b);
 	return isnegated ? be.negate() : be;
 }
 
@@ -62,7 +62,7 @@ Boolean *BooleanVar::clone(CSolver *solver, CloneMap *map) {
 	if (b != NULL)
 		return b;
 	BooleanEdge bvar = solver->getBooleanVar(type);
-	Boolean * base=bvar.getRaw();
+	Boolean *base = bvar.getRaw();
 	map->put(this, base);
 	return base;
 }
@@ -92,117 +92,117 @@ Boolean *BooleanPredicate::clone(CSolver *solver, CloneMap *map) {
 }
 
 void BooleanPredicate::updateParents() {
-	for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+	for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
 }
 
 void BooleanLogic::updateParents() {
-	for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+	for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
 }
 
-void BooleanVar::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void BooleanVar::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
 	serializer->mywrite(&type, sizeof(ASTNodeType));
-	BooleanVar* This = this;
-	serializer->mywrite(&This, sizeof(BooleanVar*));
+	BooleanVar *This = this;
+	serializer->mywrite(&This, sizeof(BooleanVar *));
 	serializer->mywrite(&vtype, sizeof(VarType));
 }
 
-void BooleanVar::print(){
+void BooleanVar::print() {
 	model_print("BooleanVar:%lu\n", (uintptr_t)this);
 }
 
-void BooleanConst::print(){
-	model_print("BooleanConst:%s\n", istrue?"TRUE" :"FALSE");
+void BooleanConst::print() {
+	model_print("BooleanConst:%s\n", istrue ? "TRUE" : "FALSE");
 }
 
-void BooleanOrder::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void BooleanOrder::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
 	order->serialize(serializer);
-	
+
 	serializer->mywrite(&type, sizeof(ASTNodeType));
-	BooleanOrder* This = this;
-	serializer->mywrite(&This, sizeof(BooleanOrder*));
-	serializer->mywrite(&order, sizeof(Order*));
+	BooleanOrder *This = this;
+	serializer->mywrite(&This, sizeof(BooleanOrder *));
+	serializer->mywrite(&order, sizeof(Order *));
 	serializer->mywrite(&first, sizeof(uint64_t));
 	serializer->mywrite(&second, sizeof(uint64_t));
 }
 
-void BooleanOrder::print(){
+void BooleanOrder::print() {
 	model_print("{BooleanOrder: First= %lu, Second = %lu on Order:\n", first, second);
 	order->print();
 	model_print("}\n");
 }
 
-void BooleanPredicate::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void BooleanPredicate::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
-	
+
 	predicate->serialize(serializer);
 	uint size = inputs.getSize();
-	for(uint i=0; i<size; i++){
-		Element* input = inputs.get(i);
+	for (uint i = 0; i < size; i++) {
+		Element *input = inputs.get(i);
 		input->serialize(serializer);
 	}
 	serializeBooleanEdge(serializer, undefStatus);
-	
+
 	serializer->mywrite(&type, sizeof(ASTNodeType));
-	BooleanPredicate* This = this;
-	serializer->mywrite(&This, sizeof(BooleanPredicate*));
+	BooleanPredicate *This = this;
+	serializer->mywrite(&This, sizeof(BooleanPredicate *));
 	serializer->mywrite(&predicate, sizeof(Predicate *));
 	serializer->mywrite(&size, sizeof(uint));
-	for(uint i=0; i<size; i++){
+	for (uint i = 0; i < size; i++) {
 		Element *input = inputs.get(i);
 		serializer->mywrite(&input, sizeof(Element *));
 	}
-	Boolean* undefStat = undefStatus!= BooleanEdge(NULL)?undefStatus.getRaw() : NULL;
-	serializer->mywrite(&undefStat, sizeof(Boolean*));
+	Boolean *undefStat = undefStatus != BooleanEdge(NULL) ? undefStatus.getRaw() : NULL;
+	serializer->mywrite(&undefStat, sizeof(Boolean *));
 }
 
-void BooleanPredicate::print(){
+void BooleanPredicate::print() {
 	model_print("{BooleanPredicate:\n");
 	predicate->print();
 	model_print("elements:\n");
 	uint size = inputs.getSize();
-	for(uint i=0; i<size; i++){
+	for (uint i = 0; i < size; i++) {
 		Element *input = inputs.get(i);
 		input->print();
 	}
 	model_print("}\n");
 }
 
-void BooleanLogic::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void BooleanLogic::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
 	uint size = inputs.getSize();
-	for(uint i=0; i<size; i++){
+	for (uint i = 0; i < size; i++) {
 		BooleanEdge input = inputs.get(i);
 		serializeBooleanEdge(serializer, input);
 	}
 	serializer->mywrite(&type, sizeof(ASTNodeType));
-	BooleanLogic* This = this;
-	serializer->mywrite(&This, sizeof(BooleanLogic*));
+	BooleanLogic *This = this;
+	serializer->mywrite(&This, sizeof(BooleanLogic *));
 	serializer->mywrite(&op, sizeof(LogicOp));
 	serializer->mywrite(&size, sizeof(uint));
-	for(uint i=0; i<size; i++){
-		Boolean* input = inputs.get(i).getRaw();
-		serializer->mywrite(&input, sizeof(Boolean*));
+	for (uint i = 0; i < size; i++) {
+		Boolean *input = inputs.get(i).getRaw();
+		serializer->mywrite(&input, sizeof(Boolean *));
 	}
 }
 
-void BooleanLogic::print(){
-	model_print("{BooleanLogic: %s\n", 
-							op ==SATC_AND? "AND": op == SATC_OR? "OR": op==SATC_NOT? "NOT":
-							op == SATC_XOR? "XOR" : op==SATC_IFF? "IFF" : "IMPLIES");
+void BooleanLogic::print() {
+	model_print("{BooleanLogic: %s\n",
+							op == SATC_AND ? "AND" : op == SATC_OR ? "OR" : op == SATC_NOT ? "NOT" :
+							op == SATC_XOR ? "XOR" : op == SATC_IFF ? "IFF" : "IMPLIES");
 	uint size = inputs.getSize();
-	for(uint i=0; i<size; i++){
+	for (uint i = 0; i < size; i++) {
 		BooleanEdge input = inputs.get(i);
-		if(input.isNegated())
+		if (input.isNegated())
 			model_print("!");
 		input.getBoolean()->print();
 	}
diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 3674d9f..9864d9b 100644
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -15,15 +15,15 @@ public:
 	Boolean(ASTNodeType _type);
 	virtual ~Boolean() {}
 	virtual Boolean *clone(CSolver *solver, CloneMap *map) = 0;
-	virtual void serialize(Serializer* ) = 0;
-        virtual void print() =0;
+	virtual void serialize(Serializer * ) = 0;
+	virtual void print() = 0;
 	virtual bool isTrue() {return boolVal == BV_MUSTBETRUE;}
 	virtual bool isFalse() {return boolVal == BV_MUSTBEFALSE;}
 	Polarity polarity;
 	BooleanValue boolVal;
 	Vector<Boolean *> parents;
 	virtual void updateParents() {}
-	
+
 	CMEMALLOC;
 };
 
@@ -33,8 +33,8 @@ public:
 	Boolean *clone(CSolver *solver, CloneMap *map);
 	bool isTrue() {return istrue;}
 	bool isFalse() {return !istrue;}
-	void serialize(Serializer *serializer ){};
-        virtual void print();
+	void serialize(Serializer *serializer ) {};
+	virtual void print();
 	bool istrue;
 	CMEMALLOC;
 };
@@ -44,7 +44,7 @@ public:
 	BooleanVar(VarType t);
 	Boolean *clone(CSolver *solver, CloneMap *map);
 	void serialize(Serializer *serializer );
-        virtual void print();
+	virtual void print();
 	VarType vtype;
 	Edge var;
 	CMEMALLOC;
@@ -55,7 +55,7 @@ public:
 	BooleanOrder(Order *_order, uint64_t _first, uint64_t _second);
 	Boolean *clone(CSolver *solver, CloneMap *map);
 	void serialize(Serializer *serializer );
-        virtual void print();
+	virtual void print();
 
 	Order *order;
 	uint64_t first;
@@ -71,7 +71,7 @@ public:
 	FunctionEncoding *getFunctionEncoding() {return &encoding;}
 	void updateParents();
 	void serialize(Serializer *serializer );
-        virtual void print();
+	virtual void print();
 	CMEMALLOC;
 
 	Predicate *predicate;
@@ -85,12 +85,12 @@ public:
 	BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uint asize);
 	Boolean *clone(CSolver *solver, CloneMap *map);
 	void serialize(Serializer *serializer );
-        virtual void print();
+	virtual void print();
 	LogicOp op;
 	bool replaced;
 	Array<BooleanEdge> inputs;
 	void updateParents();
-	
+
 	CMEMALLOC;
 };
 BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e);
diff --git a/src/AST/element.cc b/src/AST/element.cc
index 205d31f..87c0ef8 100644
--- a/src/AST/element.cc
+++ b/src/AST/element.cc
@@ -57,83 +57,83 @@ Element *ElementFunction::clone(CSolver *solver, CloneMap *map) {
 }
 
 void ElementFunction::updateParents() {
-	for(uint i=0;i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
+	for (uint i = 0; i < inputs.getSize(); i++) inputs.get(i)->parents.push(this);
 }
 
-Set * ElementFunction::getRange() {
+Set *ElementFunction::getRange() {
 	return function->getRange();
 }
 
-void ElementSet::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void ElementSet::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
-	
+
 	set->serialize(serializer);
-	
+
 	serializer->mywrite(&type, sizeof(ASTNodeType));
 	ElementSet *This = this;
-	serializer->mywrite(&This, sizeof(ElementSet*));
-	serializer->mywrite(&set, sizeof(Set*));
+	serializer->mywrite(&This, sizeof(ElementSet *));
+	serializer->mywrite(&set, sizeof(Set *));
 }
 
-void ElementSet::print(){
+void ElementSet::print() {
 	model_print("{ElementSet:\n");
 	set->print();
 	model_print("}\n");
 }
 
-void ElementConst::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void ElementConst::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
-	
+
 	set->serialize(serializer);
-	
+
 	serializer->mywrite(&type, sizeof(ASTNodeType));
 	ElementSet *This = this;
-	serializer->mywrite(&This, sizeof(ElementSet*));
+	serializer->mywrite(&This, sizeof(ElementSet *));
 	VarType type = set->getType();
 	serializer->mywrite(&type, sizeof(VarType));
 	serializer->mywrite(&value, sizeof(uint64_t));
 }
 
-void ElementConst::print(){
-	model_print("{ElementConst: %lu}\n", value);	
+void ElementConst::print() {
+	model_print("{ElementConst: %lu}\n", value);
 }
 
-void ElementFunction::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void ElementFunction::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
 
 	function->serialize(serializer);
 	uint size = inputs.getSize();
-	for(uint i=0; i<size; i++){
+	for (uint i = 0; i < size; i++) {
 		Element *input = inputs.get(i);
 		input->serialize(serializer);
 	}
 	serializeBooleanEdge(serializer, overflowstatus);
-	
+
 	serializer->mywrite(&type, sizeof(ASTNodeType));
 	ElementFunction *This = this;
 	serializer->mywrite(&This, sizeof(ElementFunction *));
 	serializer->mywrite(&function, sizeof(Function *));
 	serializer->mywrite(&size, sizeof(uint));
-	for(uint i=0; i<size; i++){
-		Element* input = inputs.get(i);
-		serializer->mywrite(&input, sizeof(Element*));
+	for (uint i = 0; i < size; i++) {
+		Element *input = inputs.get(i);
+		serializer->mywrite(&input, sizeof(Element *));
 	}
-	Boolean* overflowstat = overflowstatus.getRaw();
-	serializer->mywrite(&overflowstat, sizeof(Boolean*));
+	Boolean *overflowstat = overflowstatus.getRaw();
+	serializer->mywrite(&overflowstat, sizeof(Boolean *));
 }
 
-void ElementFunction::print(){
+void ElementFunction::print() {
 	model_print("{ElementFunction:\n");
 	function->print();
 	model_print("Elements:\n");
 	uint size = inputs.getSize();
-	for(uint i=0; i<size; i++){
+	for (uint i = 0; i < size; i++) {
 		Element *input = inputs.get(i);
 		input->print();
 	}
diff --git a/src/AST/element.h b/src/AST/element.h
index c643603..b74e582 100644
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -14,12 +14,12 @@ public:
 	virtual ~Element() {}
 	Vector<ASTNode *> parents;
 	ElementEncoding encoding;
-	inline ElementEncoding *getElementEncoding(){ return &encoding; }
+	inline ElementEncoding *getElementEncoding() { return &encoding; }
 	virtual Element *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;};
-	virtual void serialize(Serializer* serializer) =0;
-        virtual void print() = 0;
+	virtual void serialize(Serializer *serializer) = 0;
+	virtual void print() = 0;
 	virtual void updateParents() {}
-	virtual Set * getRange() = 0;
+	virtual Set *getRange() = 0;
 	CMEMALLOC;
 };
 
@@ -28,11 +28,11 @@ public:
 	ElementSet(ASTNodeType type, Set *s);
 	ElementSet(Set *s);
 	virtual Element *clone(CSolver *solver, CloneMap *map);
-	virtual void serialize(Serializer* serializer);
-        virtual void print();
+	virtual void serialize(Serializer *serializer);
+	virtual void print();
 	CMEMALLOC;
 	Set *getRange() {return set;}
- protected:
+protected:
 	Set *set;
 
 };
@@ -41,8 +41,8 @@ class ElementConst : public ElementSet {
 public:
 	ElementConst(uint64_t value, Set *_set);
 	uint64_t value;
-	virtual void serialize(Serializer* serializer);
-        virtual void print();
+	virtual void serialize(Serializer *serializer);
+	virtual void print();
 	Element *clone(CSolver *solver, CloneMap *map);
 	CMEMALLOC;
 };
@@ -54,14 +54,14 @@ public:
 	BooleanEdge overflowstatus;
 	FunctionEncoding functionencoding;
 	Element *clone(CSolver *solver, CloneMap *map);
-	virtual void serialize(Serializer* serializer);
-        virtual void print();
-	Set * getRange();
+	virtual void serialize(Serializer *serializer);
+	virtual void print();
+	Set *getRange();
 	void updateParents();
-	Function * getFunction() {return function;}
+	Function *getFunction() {return function;}
 	inline FunctionEncoding *getElementFunctionEncoding() {return &functionencoding;}
 	CMEMALLOC;
- private:
+private:
 	Function *function;
 };
 
diff --git a/src/AST/function.cc b/src/AST/function.cc
index f17fb62..c385512 100644
--- a/src/AST/function.cc
+++ b/src/AST/function.cc
@@ -62,51 +62,51 @@ Function *FunctionTable::clone(CSolver *solver, CloneMap *map) {
 	return f;
 }
 
-Set * FunctionTable::getRange() {
+Set *FunctionTable::getRange() {
 	return table->getRange();
 }
 
-void FunctionTable::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void FunctionTable::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
-	
+
 	table->serialize(serializer);
-	
-	ASTNodeType type = FUNCTABLETYPE;	
+
+	ASTNodeType type = FUNCTABLETYPE;
 	serializer->mywrite(&type, sizeof(ASTNodeType));
-	FunctionTable* This = this;
-	serializer->mywrite(&This, sizeof(FunctionTable*));
+	FunctionTable *This = this;
+	serializer->mywrite(&This, sizeof(FunctionTable *));
 	serializer->mywrite(&table, sizeof(Table *));
 	serializer->mywrite(&undefBehavior, sizeof(UndefinedBehavior));
-	
+
 }
 
-void FunctionTable::print(){
+void FunctionTable::print() {
 	model_print("{FunctionTable:\n");
 	table->print();
 	model_print("}\n");
 }
 
-void FunctionOperator::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void FunctionOperator::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
-	
+
 	uint size = domains.getSize();
-	for(uint i=0; i<size; i++){
-		Set* domain = domains.get(i);
+	for (uint i = 0; i < size; i++) {
+		Set *domain = domains.get(i);
 		domain->serialize(serializer);
 	}
 	range->serialize(serializer);
-	
-	ASTNodeType nodeType = FUNCOPTYPE; 
+
+	ASTNodeType nodeType = FUNCOPTYPE;
 	serializer->mywrite(&nodeType, sizeof(ASTNodeType));
-	FunctionOperator* This = this;
-	serializer->mywrite(&This, sizeof(FunctionOperator*));
+	FunctionOperator *This = this;
+	serializer->mywrite(&This, sizeof(FunctionOperator *));
 	serializer->mywrite(&op, sizeof(ArithOp));
 	serializer->mywrite(&size, sizeof(uint));
-	for(uint i=0; i<size; i++){
+	for (uint i = 0; i < size; i++) {
 		Set *domain = domains.get(i);
 		serializer->mywrite(&domain, sizeof(Set *));
 	}
@@ -115,5 +115,5 @@ void FunctionOperator::serialize(Serializer* serializer){
 }
 
 void FunctionOperator::print() {
-	model_print("{FunctionOperator: %s}\n", op == SATC_ADD? "ADD": "SUB" );
+	model_print("{FunctionOperator: %s}\n", op == SATC_ADD ? "ADD" : "SUB" );
 }
diff --git a/src/AST/function.h b/src/AST/function.h
index b8d0c78..5cfbb7d 100644
--- a/src/AST/function.h
+++ b/src/AST/function.h
@@ -12,9 +12,9 @@ public:
 	FunctionType type;
 	virtual ~Function() {}
 	virtual Function *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
-	virtual void serialize(Serializer* serialiezr) =0;
-        virtual void print() = 0;
-	virtual Set * getRange() = 0;
+	virtual void serialize(Serializer *serialiezr) = 0;
+	virtual void print() = 0;
+	virtual Set *getRange() = 0;
 	CMEMALLOC;
 };
 
@@ -28,9 +28,9 @@ public:
 	uint64_t applyFunctionOperator(uint numVals, uint64_t *values);
 	bool isInRangeFunction(uint64_t val);
 	Function *clone(CSolver *solver, CloneMap *map);
-	virtual void serialize(Serializer* serialiezr);
-        virtual void print();
-	Set * getRange() {return range;}
+	virtual void serialize(Serializer *serialiezr);
+	virtual void print();
+	Set *getRange() {return range;}
 	CMEMALLOC;
 };
 
@@ -40,9 +40,9 @@ public:
 	UndefinedBehavior undefBehavior;
 	FunctionTable (Table *table, UndefinedBehavior behavior);
 	Function *clone(CSolver *solver, CloneMap *map);
-	virtual void serialize(Serializer* serialiezr);
-        virtual void print();
-	Set * getRange();
+	virtual void serialize(Serializer *serialiezr);
+	virtual void print();
+	Set *getRange();
 	CMEMALLOC;
 };
 
diff --git a/src/AST/iterator.cc b/src/AST/iterator.cc
index 2b0dea4..03b368f 100644
--- a/src/AST/iterator.cc
+++ b/src/AST/iterator.cc
@@ -3,7 +3,7 @@
 #include "element.h"
 #include "csolver.h"
 
-BooleanIterator::BooleanIterator(CSolver * _solver) :
+BooleanIterator::BooleanIterator(CSolver *_solver) :
 	solverit(_solver->getConstraints()) {
 	updateNext();
 }
@@ -21,11 +21,11 @@ void BooleanIterator::updateNext() {
 		boolean.pop();
 		index.pop();
 	}
-	
-	while(true) {
+
+	while (true) {
 		if (boolean.getSize() == 0) {
 			if (solverit->hasNext()) {
-				Boolean *b=solverit->next().getBoolean();
+				Boolean *b = solverit->next().getBoolean();
 				if (discovered.add(b)) {
 					boolean.push(b);
 					index.push(0);
@@ -34,22 +34,22 @@ void BooleanIterator::updateNext() {
 			} else
 				return;
 		}
-		Boolean *topboolean=boolean.last();
-		uint topindex=index.last();
-		switch(topboolean->type) {
+		Boolean *topboolean = boolean.last();
+		uint topindex = index.last();
+		switch (topboolean->type) {
 		case ORDERCONST:
 		case BOOLEANVAR:
 		case PREDICATEOP:
 		case BOOLCONST:
 			return;
 		case LOGICOP: {
-			BooleanLogic * logicop=(BooleanLogic*) topboolean;
-			uint size=logicop->inputs.getSize();
+			BooleanLogic *logicop = (BooleanLogic *) topboolean;
+			uint size = logicop->inputs.getSize();
 			if (topindex == size)
 				return;
 			index.pop();
-			index.push(topindex+1);
-			Boolean *newchild=logicop->inputs.get(topindex).getBoolean();
+			index.push(topindex + 1);
+			Boolean *newchild = logicop->inputs.get(topindex).getBoolean();
 			if (discovered.add(newchild)) {
 				boolean.push(newchild);
 				index.push(0);
@@ -62,8 +62,8 @@ void BooleanIterator::updateNext() {
 	}
 }
 
-Boolean * BooleanIterator::next() {
-	Boolean * b = boolean.last();
+Boolean *BooleanIterator::next() {
+	Boolean *b = boolean.last();
 	updateNext();
 	return b;
 }
@@ -87,15 +87,15 @@ void ElementIterator::updateNext() {
 		element.pop();
 		index.pop();
 	}
-	
-	while(true) {
+
+	while (true) {
 		if (element.getSize() == 0) {
 			if (base != NULL) {
 				if (baseindex == base->inputs.getSize()) {
 					base = NULL;
 					continue;
 				} else {
-					Element * e = base->inputs.get(baseindex);
+					Element *e = base->inputs.get(baseindex);
 					baseindex++;
 					if (discovered.add(e)) {
 						element.push(e);
@@ -105,30 +105,30 @@ void ElementIterator::updateNext() {
 				}
 			} else {
 				if (bit.hasNext()) {
-					Boolean *b=bit.next();
+					Boolean *b = bit.next();
 					if (b->type == PREDICATEOP) {
 						base = (BooleanPredicate *)b;
-						baseindex=0;
+						baseindex = 0;
 					}
 					continue;
 				} else
 					return;
 			}
 		}
-		Element *topelement=element.last();
-		uint topindex=index.last();
-		switch(topelement->type) {
+		Element *topelement = element.last();
+		uint topindex = index.last();
+		switch (topelement->type) {
 		case ELEMSET:
 		case ELEMCONST:
 			return;
 		case ELEMFUNCRETURN: {
-			ElementFunction * func=(ElementFunction*) topelement;
-			uint size=func->inputs.getSize();
+			ElementFunction *func = (ElementFunction *) topelement;
+			uint size = func->inputs.getSize();
 			if (topindex == size)
 				return;
 			index.pop();
-			index.push(topindex+1);
-			Element *newchild=func->inputs.get(topindex);
+			index.push(topindex + 1);
+			Element *newchild = func->inputs.get(topindex);
 			if (discovered.add(newchild)) {
 				element.push(newchild);
 				index.push(0);
@@ -141,8 +141,8 @@ void ElementIterator::updateNext() {
 	}
 }
 
-Element * ElementIterator::next() {
-	Element * e = element.last();
+Element *ElementIterator::next() {
+	Element *e = element.last();
 	updateNext();
 	return e;
 }
diff --git a/src/AST/iterator.h b/src/AST/iterator.h
index 0e7303f..5309934 100644
--- a/src/AST/iterator.h
+++ b/src/AST/iterator.h
@@ -4,15 +4,15 @@
 #include "structs.h"
 
 class BooleanIterator {
- public:
-	BooleanIterator(CSolver * _solver);
+public:
+	BooleanIterator(CSolver *_solver);
 	~BooleanIterator();
 	bool hasNext();
-	Boolean * next();
+	Boolean *next();
 	CMEMALLOC;
 
- private:
-	SetIteratorBooleanEdge * solverit;
+private:
+	SetIteratorBooleanEdge *solverit;
 	HashsetBoolean discovered;
 	Vector<Boolean *> boolean;
 	Vector<uint> index;
@@ -20,14 +20,14 @@ class BooleanIterator {
 };
 
 class ElementIterator {
- public:
+public:
 	ElementIterator(CSolver *_solver);
 	~ElementIterator();
 	bool hasNext();
-	Element * next();
+	Element *next();
 	CMEMALLOC;
 
- private:
+private:
 	BooleanIterator bit;
 	BooleanPredicate *base;
 	uint baseindex;
diff --git a/src/AST/mutableset.cc b/src/AST/mutableset.cc
index 3d9db49..31ce431 100644
--- a/src/AST/mutableset.cc
+++ b/src/AST/mutableset.cc
@@ -16,13 +16,13 @@ Set *MutableSet::clone(CSolver *solver, CloneMap *map) {
 	s = solver->createMutableSet(type);
 	for (uint i = 0; i < members->getSize(); i++) {
 		((MutableSet *)s)->addElementMSet(members->get(i));
-				solver->addItem((MutableSet *) s, members->get(i));
+		solver->addItem((MutableSet *) s, members->get(i));
 	}
-	((MutableSet*)s)->finalize();
+	((MutableSet *)s)->finalize();
 	map->put(this, s);
 	return s;
 }
 
-void MutableSet::finalize(){
+void MutableSet::finalize() {
 	bsdqsort(members->expose(), members->getSize(), sizeof(uint64_t), intcompare);
 }
\ No newline at end of file
diff --git a/src/AST/order.cc b/src/AST/order.cc
index a28d6c0..f3ccde4 100644
--- a/src/AST/order.cc
+++ b/src/AST/order.cc
@@ -31,9 +31,9 @@ Order *Order::clone(CSolver *solver, CloneMap *map) {
 	return o;
 }
 
-HashtableOrderPair* Order::getOrderPairTable(){
+HashtableOrderPair *Order::getOrderPairTable() {
 	ASSERT( encoding.resolver != NULL);
-	if (OrderPairResolver* t = dynamic_cast<OrderPairResolver*>(encoding.resolver)){
+	if (OrderPairResolver *t = dynamic_cast<OrderPairResolver *>(encoding.resolver)) {
 		return t->getOrderPairTable();
 	} else {
 		ASSERT(0);
@@ -46,20 +46,20 @@ Order::~Order() {
 	}
 }
 
-void Order::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void Order::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
 	set->serialize(serializer);
 	ASTNodeType asttype = ORDERTYPE;
 	serializer->mywrite(&asttype, sizeof(ASTNodeType));
-	Order* This = this;
-	serializer->mywrite(&This, sizeof(Order*));
+	Order *This = this;
+	serializer->mywrite(&This, sizeof(Order *));
 	serializer->mywrite(&type, sizeof(OrderType));
 	serializer->mywrite(&set, sizeof(Set *));
 }
 
-void Order::print(){
+void Order::print() {
 	model_print("{Order on Set:\n");
 	set->print();
 	model_print("}\n");
diff --git a/src/AST/order.h b/src/AST/order.h
index e2e0b43..866b1ab 100644
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -8,7 +8,7 @@
 #include "boolean.h"
 #include "orderpair.h"
 
-class Order{
+class Order {
 public:
 	Order(OrderType type, Set *set);
 	virtual ~Order();
@@ -24,7 +24,7 @@ public:
 	void initializeOrderElementsHashtable();
 	void addOrderConstraint(BooleanOrder *constraint);
 	void setOrderEncodingType(OrderEncodingType type);
-	HashtableOrderPair* getOrderPairTable();
+	HashtableOrderPair *getOrderPairTable();
 	CMEMALLOC;
 };
 
diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc
index 1e0bb21..ac3b617 100644
--- a/src/AST/predicate.cc
+++ b/src/AST/predicate.cc
@@ -51,52 +51,52 @@ Predicate *PredicateTable::clone(CSolver *solver, CloneMap *map) {
 	return p;
 }
 
-void PredicateTable::serialize(Serializer* serializer){	
-	if(serializer->isSerialized(this))
+void PredicateTable::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
-	
+
 	table->serialize(serializer);
-	
-	ASTNodeType type = PREDTABLETYPE;	
+
+	ASTNodeType type = PREDTABLETYPE;
 	serializer->mywrite(&type, sizeof(ASTNodeType));
-	PredicateTable* This = this;
-	serializer->mywrite(&This, sizeof(PredicateTable*));
+	PredicateTable *This = this;
+	serializer->mywrite(&This, sizeof(PredicateTable *));
 	serializer->mywrite(&table, sizeof(Table *));
 	serializer->mywrite(&undefinedbehavior, sizeof(UndefinedBehavior));
 }
 
-void PredicateTable::print(){	
+void PredicateTable::print() {
 	model_print("{PredicateTable:\n");
 	table->print();
 	model_print("}\n");
 }
 
-void PredicateOperator::serialize(Serializer* serializer){	
-	if(serializer->isSerialized(this))
+void PredicateOperator::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
-	
+
 	uint size = domains.getSize();
-	for(uint i=0; i<size; i++){
-		Set* domain = domains.get(i);
+	for (uint i = 0; i < size; i++) {
+		Set *domain = domains.get(i);
 		domain->serialize(serializer);
 	}
-		
-	ASTNodeType type = PREDOPERTYPE;	
+
+	ASTNodeType type = PREDOPERTYPE;
 	serializer->mywrite(&type, sizeof(ASTNodeType));
-	PredicateOperator* This = this;
-	serializer->mywrite(&This, sizeof(PredicateOperator*));
+	PredicateOperator *This = this;
+	serializer->mywrite(&This, sizeof(PredicateOperator *));
 	serializer->mywrite(&op, sizeof(CompOp));
 	serializer->mywrite(&size, sizeof(uint));
-	for(uint i=0; i<size; i++){
-		Set* domain = domains.get(i);
-		serializer->mywrite(&domain, sizeof(Set*));
+	for (uint i = 0; i < size; i++) {
+		Set *domain = domains.get(i);
+		serializer->mywrite(&domain, sizeof(Set *));
 	}
 }
 
-void PredicateOperator::print(){	
-	model_print("{PredicateOperator: %s }\n", op ==SATC_EQUALS? "EQUAL": "NOT-EQUAL");
+void PredicateOperator::print() {
+	model_print("{PredicateOperator: %s }\n", op == SATC_EQUALS ? "EQUAL" : "NOT-EQUAL");
 }
 
 
diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index 94a7e2e..812d4bd 100644
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -12,8 +12,8 @@ public:
 	Predicate(PredicateType _type) : type(_type) {}
 	virtual ~Predicate() {}
 	virtual Predicate *clone(CSolver *solver, CloneMap *map) {ASSERT(0); return NULL;}
-	virtual void serialize(Serializer* serializer) = 0;
-        virtual void print() =0;
+	virtual void serialize(Serializer *serializer) = 0;
+	virtual void print() = 0;
 	PredicateType type;
 	CMEMALLOC;
 };
@@ -23,12 +23,12 @@ public:
 	PredicateOperator(CompOp op, Set **domain, uint numDomain);
 	bool evalPredicateOperator(uint64_t *inputs);
 	Predicate *clone(CSolver *solver, CloneMap *map);
-	virtual void serialize(Serializer* serializer);
-        virtual void print();
+	virtual void serialize(Serializer *serializer);
+	virtual void print();
 	Array<Set *> domains;
 	CompOp getOp() {return op;}
 	CMEMALLOC;
- private:
+private:
 	CompOp op;
 };
 
@@ -36,8 +36,8 @@ class PredicateTable : public Predicate {
 public:
 	PredicateTable(Table *table, UndefinedBehavior undefBehavior);
 	Predicate *clone(CSolver *solver, CloneMap *map);
-	virtual void serialize(Serializer* serializer);
-        virtual void print();
+	virtual void serialize(Serializer *serializer);
+	virtual void print();
 	Table *table;
 	UndefinedBehavior undefinedbehavior;
 	CMEMALLOC;
diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index b6908e1..2c946d5 100644
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -7,19 +7,19 @@ void CSolver::replaceBooleanWithTrue(BooleanEdge bexpr) {
 	if (constraints.contains(bexpr.negate())) {
 		constraints.remove(bexpr.negate());
 		setUnSAT();
-	}	
+	}
 	if (constraints.contains(bexpr)) {
 		constraints.remove(bexpr);
 	}
 
 	replaceBooleanWithTrueNoRemove(bexpr);
 }
-	
+
 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
 	updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
 
 	ASSERT(bexpr->boolVal != BV_UNSAT);
-	
+
 	uint size = bexpr->parents.getSize();
 	for (uint i = 0; i < size; i++) {
 		Boolean *parent = bexpr->parents.get(i);
@@ -44,8 +44,8 @@ void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
 void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
 	//Canonicalize
 	if (oldb.isNegated()) {
-		oldb=oldb.negate();
-		newb=newb.negate();
+		oldb = oldb.negate();
+		newb = newb.negate();
 
 	}
 	if (constraints.contains(oldb)) {
@@ -72,8 +72,8 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
 	for (uint i = 0; i < size; i++) {
 		Boolean *parent = oldb->parents.get(i);
 		BooleanLogic *logicop = (BooleanLogic *) parent;
-		boolMap.remove(parent); //could change parent's hash
-		
+		boolMap.remove(parent);	//could change parent's hash
+
 		uint parentsize = logicop->inputs.getSize();
 		for (uint j = 0; j < parentsize; j++) {
 			BooleanEdge b = logicop->inputs.get(j);
@@ -108,13 +108,13 @@ void CSolver::handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child) {
 }
 
 void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
-	BooleanEdge childNegate=child.negate();
-	
+	BooleanEdge childNegate = child.negate();
+
 	boolMap.remove(bexpr);
-	
+
 	for (uint i = 0; i < bexpr->inputs.getSize(); i++) {
 		BooleanEdge b = bexpr->inputs.get(i);
-		
+
 		if (b == child) {
 			bexpr->inputs.remove(i);
 			i--;
@@ -124,7 +124,7 @@ void CSolver::handleANDTrue(BooleanLogic *bexpr, BooleanEdge child) {
 		}
 	}
 
-	uint size=bexpr->inputs.getSize();
+	uint size = bexpr->inputs.getSize();
 	if (size == 0) {
 		bexpr->replaced = true;
 		replaceBooleanWithTrue(bexpr);
@@ -142,8 +142,8 @@ void CSolver::replaceBooleanWithFalse(BooleanEdge bexpr) {
 }
 
 BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
-	bool isNegated=bexpr.isNegated();
-	BooleanLogic * b = (BooleanLogic *) bexpr.getBoolean();
+	bool isNegated = bexpr.isNegated();
+	BooleanLogic *b = (BooleanLogic *) bexpr.getBoolean();
 	BooleanEdge result;
 	if (b->op == SATC_IFF) {
 		if (isTrue(b->inputs.get(0))) {
@@ -155,7 +155,7 @@ BooleanEdge CSolver::doRewrite(BooleanEdge bexpr) {
 		} else if (isFalse(b->inputs.get(1))) {
 			result = b->inputs.get(0).negate();
 		} else ASSERT(0);
-	} else if (b->op==SATC_AND) {
+	} else if (b->op == SATC_AND) {
 		uint size = b->inputs.getSize();
 		if (size == 0)
 			result = boolTrue;
diff --git a/src/AST/set.cc b/src/AST/set.cc
index 8fa9eda..ac4d088 100644
--- a/src/AST/set.cc
+++ b/src/AST/set.cc
@@ -5,11 +5,11 @@
 #include "qsort.h"
 
 int intcompare(const void *p1, const void *p2) {
-	uint64_t a=*(uint64_t const *) p1;
-	uint64_t b=*(uint64_t const *) p2;
+	uint64_t a = *(uint64_t const *) p1;
+	uint64_t b = *(uint64_t const *) p2;
 	if (a < b)
 		return -1;
-	else if (a==b)
+	else if (a == b)
 		return 0;
 	else
 		return 1;
@@ -34,18 +34,18 @@ bool Set::exists(uint64_t element) {
 		return element >= low && element <= high;
 	} else {
 		//Use Binary Search
-		uint low=0;
-		uint high=members->getSize()-1;
-		while(true) {
-			uint middle=(low+high)/2;
-			uint64_t val=members->get(middle);
+		uint low = 0;
+		uint high = members->getSize() - 1;
+		while (true) {
+			uint middle = (low + high) / 2;
+			uint64_t val = members->get(middle);
 			if (element < val) {
-				high=middle-1;
-				if (middle<=low)
+				high = middle - 1;
+				if (middle <= low)
 					return false;
 			} else if (element > val) {
-				low=middle+1;
-				if (middle>=high)
+				low = middle + 1;
+				if (middle >= high)
 					return false;
 			} else {
 				return true;
@@ -103,7 +103,7 @@ uint Set::getUnionSize(Set *s) {
 	uint sum = 0;
 	uint64_t sValue = s->getElement(sIndex);
 	uint64_t thisValue = getElement(thisIndex);
-	while(thisIndex < thisSize && sIndex < sSize) {
+	while (thisIndex < thisSize && sIndex < sSize) {
 		if (sValue < thisValue) {
 			sValue = s->getElement(++sIndex);
 			sum++;
@@ -117,18 +117,18 @@ uint Set::getUnionSize(Set *s) {
 		}
 	}
 	sum += (thisSize - thisIndex) + (sSize - sIndex);
-	
+
 	return sum;
 }
 
-void Set::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void Set::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
 	ASTNodeType asttype = SETTYPE;
 	serializer->mywrite(&asttype, sizeof(ASTNodeType));
-	Set* This = this;
-	serializer->mywrite(&This, sizeof(Set*));
+	Set *This = this;
+	serializer->mywrite(&This, sizeof(Set *));
 	serializer->mywrite(&type, sizeof(VarType));
 	serializer->mywrite(&isRange, sizeof(bool));
 	serializer->mywrite(&low, sizeof(uint64_t));
@@ -137,20 +137,20 @@ void Set::serialize(Serializer* serializer){
 	serializer->mywrite(&isMutable, sizeof(bool));
 	uint size = members->getSize();
 	serializer->mywrite(&size, sizeof(uint));
-	for(uint i=0; i<size; i++){
+	for (uint i = 0; i < size; i++) {
 		uint64_t mem = members->get(i);
 		serializer->mywrite(&mem, sizeof(uint64_t));
 	}
 }
 
-void Set::print(){
+void Set::print() {
 	model_print("{Set:");
-	if(isRange){
+	if (isRange) {
 		model_print("Range: low=%lu, high=%lu}\n\n", low, high);
 	} else {
 		uint size = members->getSize();
 		model_print("Members: ");
-		for(uint i=0; i<size; i++){
+		for (uint i = 0; i < size; i++) {
 			uint64_t mem = members->get(i);
 			model_print("%lu, ", mem);
 		}
diff --git a/src/AST/set.h b/src/AST/set.h
index a0bd449..c647af5 100644
--- a/src/AST/set.h
+++ b/src/AST/set.h
@@ -27,7 +27,7 @@ public:
 	uint getUnionSize(Set *s);
 	virtual bool isMutableSet() {return false;}
 	virtual Set *clone(CSolver *solver, CloneMap *map);
-	virtual void serialize(Serializer* serializer);
+	virtual void serialize(Serializer *serializer);
 	virtual void print();
 	CMEMALLOC;
 protected:
diff --git a/src/AST/table.cc b/src/AST/table.cc
index 3778767..5786b17 100644
--- a/src/AST/table.cc
+++ b/src/AST/table.cc
@@ -61,34 +61,34 @@ Table::~Table() {
 
 
 
-void Table::serialize(Serializer* serializer){
-	if(serializer->isSerialized(this))
+void Table::serialize(Serializer *serializer) {
+	if (serializer->isSerialized(this))
 		return;
 	serializer->addObject(this);
-	
+
 	uint size = domains.getSize();
-	for(uint i=0; i<size; i++){
-		Set* domain = domains.get(i);
+	for (uint i = 0; i < size; i++) {
+		Set *domain = domains.get(i);
 		domain->serialize(serializer);
 	}
-	if(range!= NULL)
+	if (range != NULL)
 		range->serialize(serializer);
-	
-	ASTNodeType type = TABLETYPE;	
+
+	ASTNodeType type = TABLETYPE;
 	serializer->mywrite(&type, sizeof(ASTNodeType));
-	Table* This = this;
-	serializer->mywrite(&This, sizeof(Table*));
+	Table *This = this;
+	serializer->mywrite(&This, sizeof(Table *));
 	serializer->mywrite(&size, sizeof(uint));
-	for(uint i=0; i<size; i++){
-		Set* domain = domains.get(i);
-		serializer->mywrite(&domain, sizeof(Set*));
+	for (uint i = 0; i < size; i++) {
+		Set *domain = domains.get(i);
+		serializer->mywrite(&domain, sizeof(Set *));
 	}
-	serializer->mywrite(&range, sizeof(Set*));
+	serializer->mywrite(&range, sizeof(Set *));
 	size = entries->getSize();
 	serializer->mywrite(&size, sizeof(uint));
-	SetIteratorTableEntry* iterator = getEntries();
-	while(iterator->hasNext()){
-		TableEntry* entry = iterator->next();
+	SetIteratorTableEntry *iterator = getEntries();
+	while (iterator->hasNext()) {
+		TableEntry *entry = iterator->next();
 		serializer->mywrite(&entry->output, sizeof(uint64_t));
 		serializer->mywrite(&entry->inputSize, sizeof(uint));
 		serializer->mywrite(entry->inputs, sizeof(uint64_t) * entry->inputSize);
@@ -97,13 +97,13 @@ void Table::serialize(Serializer* serializer){
 }
 
 
-void Table::print(){
+void Table::print() {
 	model_print("{Table:\n");
-	SetIteratorTableEntry* iterator = getEntries();
-	while(iterator->hasNext()){
-		TableEntry* entry = iterator->next();
+	SetIteratorTableEntry *iterator = getEntries();
+	while (iterator->hasNext()) {
+		TableEntry *entry = iterator->next();
 		model_print("<");
-		for(uint i=0; i<entry->inputSize; i++){
+		for (uint i = 0; i < entry->inputSize; i++) {
 			model_print("%lu, ", entry->inputs[i]);
 		}
 		model_print(" == %lu>", entry->output);
diff --git a/src/AST/table.h b/src/AST/table.h
index d8c7829..c196d3c 100644
--- a/src/AST/table.h
+++ b/src/AST/table.h
@@ -11,19 +11,19 @@ public:
 	TableEntry *getTableEntry(uint64_t *inputs, uint inputSize);
 	Table *clone(CSolver *solver, CloneMap *map);
 	void serialize(Serializer *serializer);
-        void print();
+	void print();
 	~Table();
-	Set * getRange() {return range;}
-	
-	Set * getDomain(uint i) {return domains.get(i);}
+	Set *getRange() {return range;}
+
+	Set *getDomain(uint i) {return domains.get(i);}
 	uint numDomains() {return domains.getSize();}
- 
-	SetIteratorTableEntry * getEntries() {return entries->iterator();}
+
+	SetIteratorTableEntry *getEntries() {return entries->iterator();}
 	uint getSize() {return entries->getSize();}
 
 	CMEMALLOC;
-	
- private:
+
+private:
 	Array<Set *> domains;
 	Set *range;
 	HashsetTableEntry *entries;
diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index ebe6d7a..abbaf29 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -10,13 +10,13 @@
 #include "subgraph.h"
 #include "elementencoding.h"
 
-EncodingGraph::EncodingGraph(CSolver * _solver) :
+EncodingGraph::EncodingGraph(CSolver *_solver) :
 	solver(_solver) {
 }
 
-int sortEncodingEdge(const void * p1, const void *p2) {
-	const EncodingEdge * e1 = * (const EncodingEdge **) p1;
-	const EncodingEdge * e2 = * (const EncodingEdge **) p2;
+int sortEncodingEdge(const void *p1, const void *p2) {
+	const EncodingEdge *e1 = *(const EncodingEdge **) p1;
+	const EncodingEdge *e2 = *(const EncodingEdge **) p2;
 	uint64_t v1 = e1->getValue();
 	uint64_t v2 = e2->getValue();
 	if (v1 < v2)
@@ -29,9 +29,9 @@ int sortEncodingEdge(const void * p1, const void *p2) {
 
 void EncodingGraph::buildGraph() {
 	ElementIterator it(solver);
-	while(it.hasNext()) {
-		Element * e = it.next();
-		switch(e->type) {
+	while (it.hasNext()) {
+		Element *e = it.next();
+		switch (e->type) {
 		case ELEMSET:
 		case ELEMFUNCRETURN:
 			processElement(e);
@@ -47,40 +47,40 @@ void EncodingGraph::buildGraph() {
 }
 
 void EncodingGraph::encode() {
-	SetIteratorEncodingSubGraph * itesg=subgraphs.iterator();
-	while(itesg->hasNext()) {
-		EncodingSubGraph *sg=itesg->next();
+	SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
+	while (itesg->hasNext()) {
+		EncodingSubGraph *sg = itesg->next();
 		sg->encode();
 	}
 	delete itesg;
 
 	ElementIterator it(solver);
-	while(it.hasNext()) {
-		Element * e = it.next();
-		switch(e->type) {
+	while (it.hasNext()) {
+		Element *e = it.next();
+		switch (e->type) {
 		case ELEMSET:
 		case ELEMFUNCRETURN: {
-			ElementEncoding *encoding=e->getElementEncoding();
+			ElementEncoding *encoding = e->getElementEncoding();
 			if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
 				EncodingNode *n = getNode(e);
 				if (n == NULL)
 					continue;
-				ElementEncodingType encodetype=n->getEncoding();
+				ElementEncodingType encodetype = n->getEncoding();
 				encoding->setElementEncodingType(encodetype);
 				if (encodetype == UNARY || encodetype == ONEHOT) {
 					encoding->encodingArrayInitialization();
 				} else if (encodetype == BINARYINDEX) {
-					EncodingSubGraph * subgraph = graphMap.get(n);
+					EncodingSubGraph *subgraph = graphMap.get(n);
 					if (subgraph == NULL)
 						continue;
 					uint encodingSize = subgraph->getEncodingSize(n);
 					uint paddedSize = encoding->getSizeEncodingArray(encodingSize);
 					encoding->allocInUseArrayElement(paddedSize);
 					encoding->allocEncodingArrayElement(paddedSize);
-					Set * s=e->getRange();
-					for(uint i=0;i<s->getSize();i++) {
-						uint64_t value=s->getElement(i);
-						uint encodingIndex=subgraph->getEncoding(n, value);
+					Set *s = e->getRange();
+					for (uint i = 0; i < s->getSize(); i++) {
+						uint64_t value = s->getElement(i);
+						uint encodingIndex = subgraph->getEncoding(n, value);
 						encoding->setInUseElement(encodingIndex);
 						encoding->encodingArray[encodingIndex] = value;
 					}
@@ -96,23 +96,23 @@ void EncodingGraph::encode() {
 }
 
 void EncodingGraph::encodeParent(Element *e) {
-	uint size=e->parents.getSize();
-	for(uint i=0;i<size;i++) {
-		ASTNode * n = e->parents.get(i);
-		if (n->type==PREDICATEOP) {
-			BooleanPredicate *b=(BooleanPredicate *)n;
-			FunctionEncoding *fenc=b->getFunctionEncoding();
+	uint size = e->parents.getSize();
+	for (uint i = 0; i < size; i++) {
+		ASTNode *n = e->parents.get(i);
+		if (n->type == PREDICATEOP) {
+			BooleanPredicate *b = (BooleanPredicate *)n;
+			FunctionEncoding *fenc = b->getFunctionEncoding();
 			if (fenc->getFunctionEncodingType() != FUNC_UNASSIGNED)
 				continue;
-			Predicate *p=b->getPredicate();
-			if (p->type==OPERATORPRED) {
-				PredicateOperator *po=(PredicateOperator *)p;
-				ASSERT(b->inputs.getSize()==2);
-				EncodingNode *left=createNode(b->inputs.get(0));
-				EncodingNode *right=createNode(b->inputs.get(1));
+			Predicate *p = b->getPredicate();
+			if (p->type == OPERATORPRED) {
+				PredicateOperator *po = (PredicateOperator *)p;
+				ASSERT(b->inputs.getSize() == 2);
+				EncodingNode *left = createNode(b->inputs.get(0));
+				EncodingNode *right = createNode(b->inputs.get(1));
 				if (left == NULL || right == NULL)
 					return;
-				EncodingEdge *edge=getEdge(left, right, NULL);
+				EncodingEdge *edge = getEdge(left, right, NULL);
 				if (edge != NULL && edge->getEncoding() == EDGE_MATCH) {
 					fenc->setFunctionEncodingType(CIRCUIT);
 				}
@@ -122,8 +122,8 @@ void EncodingGraph::encodeParent(Element *e) {
 }
 
 void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
-	EncodingSubGraph *graph1=graphMap.get(first);
-	EncodingSubGraph *graph2=graphMap.get(second);
+	EncodingSubGraph *graph1 = graphMap.get(first);
+	EncodingSubGraph *graph2 = graphMap.get(second);
 	if (graph1 == NULL)
 		first->setEncoding(BINARYINDEX);
 	if (graph2 == NULL)
@@ -143,9 +143,9 @@ void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
 		first = tmp;
 	}
 	if (graph1 != NULL && graph2 != NULL) {
-		SetIteratorEncodingNode * nodeit=graph2->nodeIterator();
-		while(nodeit->hasNext()) {
-			EncodingNode *node=nodeit->next();
+		SetIteratorEncodingNode *nodeit = graph2->nodeIterator();
+		while (nodeit->hasNext()) {
+			EncodingNode *node = nodeit->next();
 			graph1->addNode(node);
 			graphMap.put(node, graph1);
 		}
@@ -160,10 +160,10 @@ void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
 }
 
 void EncodingGraph::processElement(Element *e) {
-	uint size=e->parents.getSize();
-	for(uint i=0;i<size;i++) {
-		ASTNode * n = e->parents.get(i);
-		switch(n->type) {
+	uint size = e->parents.getSize();
+	for (uint i = 0; i < size; i++) {
+		ASTNode *n = e->parents.get(i);
+		switch (n->type) {
 		case PREDICATEOP:
 			processPredicate((BooleanPredicate *)n);
 			break;
@@ -177,32 +177,32 @@ void EncodingGraph::processElement(Element *e) {
 }
 
 void EncodingGraph::processFunction(ElementFunction *ef) {
-	Function *f=ef->getFunction();
-	if (f->type==OPERATORFUNC) {
-		FunctionOperator *fo=(FunctionOperator*)f;
+	Function *f = ef->getFunction();
+	if (f->type == OPERATORFUNC) {
+		FunctionOperator *fo = (FunctionOperator *)f;
 		ASSERT(ef->inputs.getSize() == 2);
-		EncodingNode *left=createNode(ef->inputs.get(0));
-		EncodingNode *right=createNode(ef->inputs.get(1));
+		EncodingNode *left = createNode(ef->inputs.get(0));
+		EncodingNode *right = createNode(ef->inputs.get(1));
 		if (left == NULL && right == NULL)
 			return;
-		EncodingNode *dst=createNode(ef);
-		EncodingEdge *edge=createEdge(left, right, dst);
+		EncodingNode *dst = createNode(ef);
+		EncodingEdge *edge = createEdge(left, right, dst);
 		edge->numArithOps++;
 	}
 }
 
 void EncodingGraph::processPredicate(BooleanPredicate *b) {
-	Predicate *p=b->getPredicate();
-	if (p->type==OPERATORPRED) {
-		PredicateOperator *po=(PredicateOperator *)p;
-		ASSERT(b->inputs.getSize()==2);
-		EncodingNode *left=createNode(b->inputs.get(0));
-		EncodingNode *right=createNode(b->inputs.get(1));
+	Predicate *p = b->getPredicate();
+	if (p->type == OPERATORPRED) {
+		PredicateOperator *po = (PredicateOperator *)p;
+		ASSERT(b->inputs.getSize() == 2);
+		EncodingNode *left = createNode(b->inputs.get(0));
+		EncodingNode *right = createNode(b->inputs.get(1));
 		if (left == NULL || right == NULL)
 			return;
-		EncodingEdge *edge=createEdge(left, right, NULL);
-		CompOp op=po->getOp();
-		switch(op) {
+		EncodingEdge *edge = createEdge(left, right, NULL);
+		CompOp op = po->getOp();
+		switch (op) {
 		case SATC_EQUALS:
 			edge->numEquals++;
 			break;
@@ -219,60 +219,60 @@ void EncodingGraph::processPredicate(BooleanPredicate *b) {
 }
 
 uint convertSize(uint cost) {
-	cost = 1.2 * cost; // fudge factor
+	cost = 1.2 * cost;// fudge factor
 	return NEXTPOW2(cost);
 }
 
 void EncodingGraph::decideEdges() {
-	uint size=edgeVector.getSize();
-	for(uint i=0; i<size; i++) {
+	uint size = edgeVector.getSize();
+	for (uint i = 0; i < size; i++) {
 		EncodingEdge *ee = edgeVector.get(i);
 		EncodingNode *left = ee->left;
 		EncodingNode *right = ee->right;
-		
+
 		if (ee->encoding != EDGE_UNASSIGNED ||
 				!left->couldBeBinaryIndex() ||
 				!right->couldBeBinaryIndex())
 			continue;
-		
+
 		uint64_t eeValue = ee->getValue();
 		if (eeValue == 0)
 			return;
 
 		EncodingSubGraph *leftGraph = graphMap.get(left);
 		EncodingSubGraph *rightGraph = graphMap.get(right);
-		if (leftGraph == NULL && rightGraph !=NULL) {
-			EncodingNode *tmp = left; left=right; right=tmp;
+		if (leftGraph == NULL && rightGraph != NULL) {
+			EncodingNode *tmp = left; left = right; right = tmp;
 			EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
 		}
 
-		uint leftSize=0, rightSize=0, newSize=0;
-		uint64_t totalCost=0;
+		uint leftSize = 0, rightSize = 0, newSize = 0;
+		uint64_t totalCost = 0;
 		if (leftGraph == NULL && rightGraph == NULL) {
-			leftSize=convertSize(left->getSize());
-			rightSize=convertSize(right->getSize());
-			newSize=convertSize(left->s->getUnionSize(right->s));
-			newSize=(leftSize > newSize) ? leftSize: newSize;
-			newSize=(rightSize > newSize) ? rightSize: newSize;
+			leftSize = convertSize(left->getSize());
+			rightSize = convertSize(right->getSize());
+			newSize = convertSize(left->s->getUnionSize(right->s));
+			newSize = (leftSize > newSize) ? leftSize : newSize;
+			newSize = (rightSize > newSize) ? rightSize : newSize;
 			totalCost = (newSize - leftSize) * left->elements.getSize() +
-				(newSize - rightSize) * right->elements.getSize();
+									(newSize - rightSize) * right->elements.getSize();
 		} else if (leftGraph != NULL && rightGraph == NULL) {
-			leftSize=convertSize(leftGraph->encodingSize);
-			rightSize=convertSize(right->getSize());
-			newSize=convertSize(leftGraph->estimateNewSize(right));
-			newSize=(leftSize > newSize) ? leftSize: newSize;
-			newSize=(rightSize > newSize) ? rightSize: newSize;
+			leftSize = convertSize(leftGraph->encodingSize);
+			rightSize = convertSize(right->getSize());
+			newSize = convertSize(leftGraph->estimateNewSize(right));
+			newSize = (leftSize > newSize) ? leftSize : newSize;
+			newSize = (rightSize > newSize) ? rightSize : newSize;
 			totalCost = (newSize - leftSize) * leftGraph->numElements +
-				(newSize - rightSize) * right->elements.getSize();
+									(newSize - rightSize) * right->elements.getSize();
 		} else {
 			//Neither are null
-			leftSize=convertSize(leftGraph->encodingSize);
-			rightSize=convertSize(rightGraph->encodingSize);
-			newSize=convertSize(leftGraph->estimateNewSize(rightGraph));
-			newSize=(leftSize > newSize) ? leftSize: newSize;
-			newSize=(rightSize > newSize) ? rightSize: newSize;
+			leftSize = convertSize(leftGraph->encodingSize);
+			rightSize = convertSize(rightGraph->encodingSize);
+			newSize = convertSize(leftGraph->estimateNewSize(rightGraph));
+			newSize = (leftSize > newSize) ? leftSize : newSize;
+			newSize = (rightSize > newSize) ? rightSize : newSize;
 			totalCost = (newSize - leftSize) * leftGraph->numElements +
-				(newSize - rightSize) * rightGraph->numElements;
+									(newSize - rightSize) * rightGraph->numElements;
 		}
 		double conversionfactor = 0.5;
 		if ((totalCost * conversionfactor) < eeValue) {
@@ -284,28 +284,28 @@ void EncodingGraph::decideEdges() {
 
 static TunableDesc EdgeEncodingDesc(EDGE_UNASSIGNED, EDGE_MATCH, EDGE_UNASSIGNED);
 
-EncodingEdge * EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
+EncodingEdge *EncodingGraph::getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
 	EncodingEdge e(left, right, dst);
 	EncodingEdge *result = edgeMap.get(&e);
 	return result;
 }
 
-EncodingEdge * EncodingGraph::createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
+EncodingEdge *EncodingGraph::createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst) {
 	EncodingEdge e(left, right, dst);
 	EncodingEdge *result = edgeMap.get(&e);
 	if (result == NULL) {
-		result=new EncodingEdge(left, right, dst);
-		VarType v1=left->getType();
-		VarType v2=right->getType();
+		result = new EncodingEdge(left, right, dst);
+		VarType v1 = left->getType();
+		VarType v2 = right->getType();
 		if (v1 > v2) {
-			VarType tmp=v2;
-			v2=v1;
-			v1=tmp;
+			VarType tmp = v2;
+			v2 = v1;
+			v1 = tmp;
 		}
 
 		if ((left != NULL && left->couldBeBinaryIndex()) &&
 				(right != NULL) && right->couldBeBinaryIndex()) {
-			EdgeEncodingType type=(EdgeEncodingType)solver->getTuner()->getVarTunable(v1, v2, EDGEENCODING, &EdgeEncodingDesc);
+			EdgeEncodingType type = (EdgeEncodingType)solver->getTuner()->getVarTunable(v1, v2, EDGEENCODING, &EdgeEncodingDesc);
 			result->setEncoding(type);
 			if (type == EDGE_MATCH) {
 				mergeNodes(left, right);
@@ -337,7 +337,7 @@ VarType EncodingNode::getType() const {
 
 static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
 
-EncodingNode * EncodingGraph::createNode(Element *e) {
+EncodingNode *EncodingGraph::createNode(Element *e) {
 	if (e->type == ELEMCONST)
 		return NULL;
 	Set *s = e->getRange();
@@ -345,14 +345,14 @@ EncodingNode * EncodingGraph::createNode(Element *e) {
 	if (n == NULL) {
 		n = new EncodingNode(s);
 		n->setEncoding((ElementEncodingType)solver->getTuner()->getVarTunable(n->getType(), NODEENCODING, &NodeEncodingDesc));
-		
+
 		encodingMap.put(s, n);
 	}
 	n->addElement(e);
 	return n;
 }
 
-EncodingNode * EncodingGraph::getNode(Element *e) {
+EncodingNode *EncodingGraph::getNode(Element *e) {
 	if (e->type == ELEMCONST)
 		return NULL;
 	Set *s = e->getRange();
@@ -387,7 +387,7 @@ EncodingEdge::EncodingEdge(EncodingNode *_left, EncodingNode *_right, EncodingNo
 }
 
 uint hashEncodingEdge(EncodingEdge *edge) {
-	uintptr_t hash=(((uintptr_t) edge->left) >> 2) ^ (((uintptr_t)edge->right) >> 4) ^ (((uintptr_t)edge->dst) >> 6);
+	uintptr_t hash = (((uintptr_t) edge->left) >> 2) ^ (((uintptr_t)edge->right) >> 4) ^ (((uintptr_t)edge->dst) >> 6);
 	return (uint) hash;
 }
 
diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index 301a74a..0c27e0a 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -5,44 +5,44 @@
 #include "graphstructs.h"
 
 class EncodingGraph {
- public:
-	EncodingGraph(CSolver * solver);
+public:
+	EncodingGraph(CSolver *solver);
 	void buildGraph();
 	void encode();
-	
+
 	CMEMALLOC;
- private:
-	CSolver * solver;
+private:
+	CSolver *solver;
 	HashtableEncoding encodingMap;
 	HashtableEdge edgeMap;
 	Vector<EncodingEdge *> edgeVector;
 	HashsetElement discovered;
 	HashtableNodeToSubGraph graphMap;
 	HashsetEncodingSubGraph subgraphs;
-	
+
 	void encodeParent(Element *e);
 	void decideEdges();
 	void mergeNodes(EncodingNode *first, EncodingNode *second);
 	void processElement(Element *e);
 	void processFunction(ElementFunction *f);
 	void processPredicate(BooleanPredicate *b);
-	EncodingNode * createNode(Element *e);
-	EncodingNode * getNode(Element *e);
-	EncodingEdge * getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
-	EncodingEdge * createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
+	EncodingNode *createNode(Element *e);
+	EncodingNode *getNode(Element *e);
+	EncodingEdge *getEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
+	EncodingEdge *createEdge(EncodingNode *left, EncodingNode *right, EncodingNode *dst);
 };
 
 class EncodingNode {
- public:
+public:
 	EncodingNode(Set *_s);
 	void addElement(Element *e);
 	uint getSize() const;
 	VarType getType() const;
-	void setEncoding(ElementEncodingType e) {encoding=e;}
+	void setEncoding(ElementEncodingType e) {encoding = e;}
 	ElementEncodingType getEncoding() {return encoding;}
 	bool couldBeBinaryIndex() {return encoding == BINARYINDEX || encoding == ELEM_UNASSIGNED;}
 	CMEMALLOC;
- private:
+private:
 	Set *s;
 	HashsetElement elements;
 	HashsetEncodingEdge edges;
@@ -55,16 +55,16 @@ enum EdgeEncodingType { EDGE_UNASSIGNED, EDGE_BREAK, EDGE_MATCH};
 typedef enum EdgeEncodingType EdgeEncodingType;
 
 class EncodingEdge {
- public:
+public:
 	EncodingEdge(EncodingNode *_l, EncodingNode *_r);
 	EncodingEdge(EncodingNode *_l, EncodingNode *_r, EncodingNode *_d);
-	void setEncoding(EdgeEncodingType e) {encoding=e;}
+	void setEncoding(EdgeEncodingType e) {encoding = e;}
 	uint64_t getValue() const;
 	EdgeEncodingType getEncoding() {return encoding;}
 
 	CMEMALLOC;
-	
- private:
+
+private:
 	EncodingNode *left;
 	EncodingNode *right;
 	EncodingNode *dst;
diff --git a/src/ASTAnalyses/Encoding/subgraph.cc b/src/ASTAnalyses/Encoding/subgraph.cc
index afddea1..f2c0de2 100644
--- a/src/ASTAnalyses/Encoding/subgraph.cc
+++ b/src/ASTAnalyses/Encoding/subgraph.cc
@@ -18,10 +18,10 @@ bool equalsNodeValuePair(NodeValuePair *nvp1, NodeValuePair *nvp2) {
 }
 
 int sortEncodingValue(const void *p1, const void *p2) {
-	const EncodingValue * e1 = * (const EncodingValue **) p1;
-	const EncodingValue * e2 = * (const EncodingValue **) p2;
-	uint se1=e1->notequals.getSize();
-	uint se2=e2->notequals.getSize();
+	const EncodingValue *e1 = *(const EncodingValue **) p1;
+	const EncodingValue *e2 = *(const EncodingValue **) p2;
+	uint se1 = e1->notequals.getSize();
+	uint se2 = e2->notequals.getSize();
 	if (se1 > se2)
 		return -1;
 	else if (se2 == se1)
@@ -39,9 +39,9 @@ uint EncodingSubGraph::getEncoding(EncodingNode *n, uint64_t val) {
 void EncodingSubGraph::solveEquals() {
 	Vector<EncodingValue *> toEncode;
 	Vector<bool> encodingArray;
-	SetIteratorEncodingValue *valIt=values.iterator();
-	while(valIt->hasNext()) {
-		EncodingValue *ev=valIt->next();
+	SetIteratorEncodingValue *valIt = values.iterator();
+	while (valIt->hasNext()) {
+		EncodingValue *ev = valIt->next();
 		if (!ev->inComparison)
 			toEncode.push(ev);
 		else
@@ -49,20 +49,20 @@ void EncodingSubGraph::solveEquals() {
 	}
 	delete valIt;
 	bsdqsort(toEncode.expose(), toEncode.getSize(), sizeof(EncodingValue *), sortEncodingValue);
-	uint toEncodeSize=toEncode.getSize();
-	for(uint i=0; i<toEncodeSize; i++) {
-		EncodingValue * ev=toEncode.get(i);
+	uint toEncodeSize = toEncode.getSize();
+	for (uint i = 0; i < toEncodeSize; i++) {
+		EncodingValue *ev = toEncode.get(i);
 		encodingArray.clear();
-		SetIteratorEncodingValue *conflictIt=ev->notequals.iterator();
-		while(conflictIt->hasNext()) {
-			EncodingValue * conflict=conflictIt->next();
+		SetIteratorEncodingValue *conflictIt = ev->notequals.iterator();
+		while (conflictIt->hasNext()) {
+			EncodingValue *conflict = conflictIt->next();
 			if (conflict->assigned) {
 				encodingArray.setExpand(conflict->encoding, true);
 			}
 		}
 		delete conflictIt;
-		uint encoding=0;
-		for(;encoding<encodingArray.getSize();encoding++) {
+		uint encoding = 0;
+		for (; encoding < encodingArray.getSize(); encoding++) {
 			//See if this is unassigned
 			if (!encodingArray.get(encoding))
 				break;
@@ -77,17 +77,17 @@ void EncodingSubGraph::solveEquals() {
 void EncodingSubGraph::solveComparisons() {
 	HashsetEncodingValue discovered;
 	Vector<EncodingValue *> tovisit;
-	SetIteratorEncodingValue *valIt=values.iterator();
-	while(valIt->hasNext()) {
-		EncodingValue *ev=valIt->next();
+	SetIteratorEncodingValue *valIt = values.iterator();
+	while (valIt->hasNext()) {
+		EncodingValue *ev = valIt->next();
 		if (discovered.add(ev)) {
 			tovisit.push(ev);
-			while(tovisit.getSize()!=0) {
-				EncodingValue * val=tovisit.last(); tovisit.pop();
-				SetIteratorEncodingValue *nextIt=val->larger.iterator();
+			while (tovisit.getSize() != 0) {
+				EncodingValue *val = tovisit.last(); tovisit.pop();
+				SetIteratorEncodingValue *nextIt = val->larger.iterator();
 				uint minVal = val->encoding + 1;
-				while(nextIt->hasNext()) {
-					EncodingValue *nextVal=nextIt->next();
+				while (nextIt->hasNext()) {
+					EncodingValue *nextVal = nextIt->next();
 					if (nextVal->encoding < minVal) {
 						if (minVal > maxEncodingVal)
 							maxEncodingVal = minVal;
@@ -104,11 +104,11 @@ void EncodingSubGraph::solveComparisons() {
 }
 
 uint EncodingSubGraph::estimateNewSize(EncodingSubGraph *sg) {
-	uint newSize=0;
-	SetIteratorEncodingNode * nit = sg->nodes.iterator();
-	while(nit->hasNext()) {
+	uint newSize = 0;
+	SetIteratorEncodingNode *nit = sg->nodes.iterator();
+	while (nit->hasNext()) {
 		EncodingNode *en = nit->next();
-		uint size=estimateNewSize(en);
+		uint size = estimateNewSize(en);
 		if (size > newSize)
 			newSize = size;
 	}
@@ -117,10 +117,10 @@ uint EncodingSubGraph::estimateNewSize(EncodingSubGraph *sg) {
 }
 
 uint EncodingSubGraph::estimateNewSize(EncodingNode *n) {
-	SetIteratorEncodingEdge * eeit = n->edges.iterator();
-	uint newsize=n->getSize();
-	while(eeit->hasNext()) {
-		EncodingEdge * ee = eeit->next();
+	SetIteratorEncodingEdge *eeit = n->edges.iterator();
+	uint newsize = n->getSize();
+	while (eeit->hasNext()) {
+		EncodingEdge *ee = eeit->next();
 		if (ee->left != NULL && ee->left != n && nodes.contains(ee->left)) {
 			uint intersectSize = n->s->getUnionSize(ee->left->s);
 			if (intersectSize > newsize)
@@ -143,13 +143,13 @@ uint EncodingSubGraph::estimateNewSize(EncodingNode *n) {
 
 void EncodingSubGraph::addNode(EncodingNode *n) {
 	nodes.add(n);
-	uint newSize=estimateNewSize(n);
+	uint newSize = estimateNewSize(n);
 	numElements += n->elements.getSize();
 	if (newSize > encodingSize)
-		encodingSize=newSize;
+		encodingSize = newSize;
 }
 
-SetIteratorEncodingNode * EncodingSubGraph::nodeIterator() {
+SetIteratorEncodingNode *EncodingSubGraph::nodeIterator() {
 	return nodes.iterator();
 }
 
@@ -162,14 +162,14 @@ void EncodingSubGraph::encode() {
 }
 
 void EncodingSubGraph::computeEqualities() {
-	SetIteratorEncodingNode *nodeit=nodes.iterator();
-	while(nodeit->hasNext()) {
-		EncodingNode *node=nodeit->next();
+	SetIteratorEncodingNode *nodeit = nodes.iterator();
+	while (nodeit->hasNext()) {
+		EncodingNode *node = nodeit->next();
 		generateEquals(node, node);
-		
-		SetIteratorEncodingEdge *edgeit=node->edges.iterator();
-		while(edgeit->hasNext()) {
-			EncodingEdge *edge=edgeit->next();
+
+		SetIteratorEncodingEdge *edgeit = node->edges.iterator();
+		while (edgeit->hasNext()) {
+			EncodingEdge *edge = edgeit->next();
 			//skip over comparisons as we have already handled them
 			if (edge->numComparisons != 0)
 				continue;
@@ -194,12 +194,12 @@ void EncodingSubGraph::computeEqualities() {
 }
 
 void EncodingSubGraph::computeComparisons() {
-	SetIteratorEncodingNode *nodeit=nodes.iterator();
-	while(nodeit->hasNext()) {
-		EncodingNode *node=nodeit->next();
-		SetIteratorEncodingEdge *edgeit=node->edges.iterator();
-		while(edgeit->hasNext()) {
-			EncodingEdge *edge=edgeit->next();
+	SetIteratorEncodingNode *nodeit = nodes.iterator();
+	while (nodeit->hasNext()) {
+		EncodingNode *node = nodeit->next();
+		SetIteratorEncodingEdge *edgeit = node->edges.iterator();
+		while (edgeit->hasNext()) {
+			EncodingEdge *edge = edgeit->next();
 			if (edge->numComparisons == 0)
 				continue;
 			if (edge->left == NULL || !nodes.contains(edge->left))
@@ -222,15 +222,15 @@ void EncodingSubGraph::orderEV(EncodingValue *earlier, EncodingValue *later) {
 }
 
 void EncodingSubGraph::generateEquals(EncodingNode *left, EncodingNode *right) {
-	Set *lset=left->s;
-	Set *rset=right->s;
-	uint lSize=lset->getSize(), rSize=rset->getSize();
-	for(uint lindex=0; lindex < lSize; lindex++) {
-		for(uint rindex=0; rindex < rSize; rindex++) {
-			uint64_t lVal=lset->getElement(lindex);
+	Set *lset = left->s;
+	Set *rset = right->s;
+	uint lSize = lset->getSize(), rSize = rset->getSize();
+	for (uint lindex = 0; lindex < lSize; lindex++) {
+		for (uint rindex = 0; rindex < rSize; rindex++) {
+			uint64_t lVal = lset->getElement(lindex);
 			NodeValuePair nvp1(left, lVal);
 			EncodingValue *lev = map.get(&nvp1);
-			uint64_t rVal=rset->getElement(rindex);
+			uint64_t rVal = rset->getElement(rindex);
 			NodeValuePair nvp2(right, rVal);
 			EncodingValue *rev = map.get(&nvp2);
 			if (lev != rev) {
@@ -252,21 +252,21 @@ void EncodingSubGraph::generateEquals(EncodingNode *left, EncodingNode *right) {
 }
 
 void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *right) {
-	Set *lset=left->s;
-	Set *rset=right->s;
-	uint lindex=0, rindex=0;
-	uint lSize=lset->getSize(), rSize=rset->getSize();
-	uint64_t lVal=lset->getElement(lindex);
+	Set *lset = left->s;
+	Set *rset = right->s;
+	uint lindex = 0, rindex = 0;
+	uint lSize = lset->getSize(), rSize = rset->getSize();
+	uint64_t lVal = lset->getElement(lindex);
 	NodeValuePair nvp1(left, lVal);
 	EncodingValue *lev = map.get(&nvp1);
 	lev->inComparison = true;
-	uint64_t rVal=rset->getElement(rindex);
+	uint64_t rVal = rset->getElement(rindex);
 	NodeValuePair nvp2(right, rVal);
 	EncodingValue *rev = map.get(&nvp2);
 	rev->inComparison = true;
 	EncodingValue *last = NULL;
 
-	while(lindex < lSize || rindex < rSize) {
+	while (lindex < lSize || rindex < rSize) {
 		if (last != NULL) {
 			if (lev != NULL)
 				orderEV(last, lev);
@@ -280,7 +280,7 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
 					orderEV(lev, rev);
 				last = lev;
 				if (++lindex < lSize) {
-					lVal=lset->getElement(lindex);
+					lVal = lset->getElement(lindex);
 					NodeValuePair nvpl(left, lVal);
 					lev = map.get(&nvpl);
 					lev->inComparison = true;
@@ -291,7 +291,7 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
 					orderEV(rev, lev);
 				last = rev;
 				if (++rindex < rSize) {
-					rVal=rset->getElement(rindex);
+					rVal = rset->getElement(rindex);
 					NodeValuePair nvpr(right, rVal);
 					rev = map.get(&nvpr);
 					rev->inComparison = true;
@@ -301,7 +301,7 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
 		} else {
 			last = lev;
 			if (++lindex < lSize) {
-				lVal=lset->getElement(lindex);
+				lVal = lset->getElement(lindex);
 				NodeValuePair nvpl(left, lVal);
 				lev = map.get(&nvpl);
 				lev->inComparison = true;
@@ -309,7 +309,7 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
 				lev = NULL;
 
 			if (++rindex < rSize) {
-				rVal=rset->getElement(rindex);
+				rVal = rset->getElement(rindex);
 				NodeValuePair nvpr(right, rVal);
 				rev = map.get(&nvpr);
 				rev->inComparison = true;
@@ -320,12 +320,12 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
 }
 
 void EncodingSubGraph::computeEncodingValue() {
-	SetIteratorEncodingNode *nodeit=nodes.iterator();
-	while(nodeit->hasNext()) {
-		EncodingNode *node=nodeit->next();
-		Set * set = node->s;
+	SetIteratorEncodingNode *nodeit = nodes.iterator();
+	while (nodeit->hasNext()) {
+		EncodingNode *node = nodeit->next();
+		Set *set = node->s;
 		uint setSize = set->getSize();
-		for(uint i=0; i<setSize; i++) {
+		for (uint i = 0; i < setSize; i++) {
 			uint64_t val = set->getElement(i);
 			NodeValuePair nvp(node, val);
 			if (!map.contains(&nvp)) {
@@ -337,21 +337,21 @@ void EncodingSubGraph::computeEncodingValue() {
 }
 
 void EncodingSubGraph::traverseValue(EncodingNode *node, uint64_t value) {
-	EncodingValue *ecv=new EncodingValue(value);
+	EncodingValue *ecv = new EncodingValue(value);
 	values.add(ecv);
 	HashsetEncodingNode discovered;
 	Vector<EncodingNode *> tovisit;
 	tovisit.push(node);
 	discovered.add(node);
-	while(tovisit.getSize()!=0) {
-		EncodingNode *n=tovisit.last();tovisit.pop();
+	while (tovisit.getSize() != 0) {
+		EncodingNode *n = tovisit.last();tovisit.pop();
 		//Add encoding node to structures
 		ecv->nodes.add(n);
-		NodeValuePair *nvp=new NodeValuePair(n, value);
+		NodeValuePair *nvp = new NodeValuePair(n, value);
 		map.put(nvp, ecv);
-		SetIteratorEncodingEdge *edgeit=node->edges.iterator();
-		while(edgeit->hasNext()) {
-			EncodingEdge *ee=edgeit->next();
+		SetIteratorEncodingEdge *edgeit = node->edges.iterator();
+		while (edgeit->hasNext()) {
+			EncodingEdge *ee = edgeit->next();
 			if (!discovered.contains(ee->left) && nodes.contains(ee->left) && ee->left->s->exists(value)) {
 				tovisit.push(ee->left);
 				discovered.add(ee->left);
diff --git a/src/ASTAnalyses/Encoding/subgraph.h b/src/ASTAnalyses/Encoding/subgraph.h
index 1f90e91..36f1902 100644
--- a/src/ASTAnalyses/Encoding/subgraph.h
+++ b/src/ASTAnalyses/Encoding/subgraph.h
@@ -5,8 +5,8 @@
 #include "graphstructs.h"
 
 class NodeValuePair {
- public:
- NodeValuePair(EncodingNode *n, uint64_t val) : node(n), value(val) {}
+public:
+	NodeValuePair(EncodingNode *n, uint64_t val) : node(n), value(val) {}
 	EncodingNode *node;
 	uint64_t value;
 };
@@ -17,8 +17,8 @@ typedef Hashset<EncodingValue *, uintptr_t, PTRSHIFT> HashsetEncodingValue;
 typedef SetIterator<EncodingValue *, uintptr_t, PTRSHIFT> SetIteratorEncodingValue;
 
 class EncodingValue {
- public:
- EncodingValue(uint64_t _val) : value(_val), encoding(0), inComparison(false), assigned(false) {}
+public:
+	EncodingValue(uint64_t _val) : value(_val), encoding(0), inComparison(false), assigned(false) {}
 	void merge(EncodingValue *value);
 	uint64_t value;
 	uint encoding;
@@ -35,16 +35,16 @@ bool equalsNodeValuePair(NodeValuePair *nvp1, NodeValuePair *nvp2);
 typedef Hashtable<NodeValuePair *, EncodingValue *, uintptr_t, 0, hashNodeValuePair, equalsNodeValuePair> NVPMap;
 
 class EncodingSubGraph {
- public:
+public:
 	EncodingSubGraph();
 	void addNode(EncodingNode *n);
-	SetIteratorEncodingNode * nodeIterator();
+	SetIteratorEncodingNode *nodeIterator();
 	void encode();
 	uint getEncoding(EncodingNode *n, uint64_t val);
 	uint getEncodingSize(EncodingNode *n) { return maxEncodingVal;}
-	
+
 	CMEMALLOC;
- private:
+private:
 	uint estimateNewSize(EncodingNode *n);
 	uint estimateNewSize(EncodingSubGraph *sg);
 	void traverseValue(EncodingNode *node, uint64_t value);
@@ -63,7 +63,7 @@ class EncodingSubGraph {
 	uint encodingSize;
 	uint numElements;
 	uint maxEncodingVal;
-	
+
 	friend class EncodingGraph;
 };
 
diff --git a/src/ASTAnalyses/Order/orderanalysis.cc b/src/ASTAnalyses/Order/orderanalysis.cc
index ae3c752..701efde 100644
--- a/src/ASTAnalyses/Order/orderanalysis.cc
+++ b/src/ASTAnalyses/Order/orderanalysis.cc
@@ -115,7 +115,7 @@ void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
 			OrderNode *sinkNode = outEdge->sink;
 			sinkNode->inEdges.remove(outEdge);
 			//Adding new edge to new sink and src nodes ...
-			if(srcNode == sinkNode) {
+			if (srcNode == sinkNode) {
 				This->setUnSAT();
 				delete iterout;
 				delete iterin;
@@ -297,7 +297,7 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode
 				if (!edge->mustNeg && sources->contains(child)) {
 					edge->mustNeg = true;
 					edge->polNeg = true;
-					if (edge->mustPos){
+					if (edge->mustPos) {
 						solver->setUnSAT();
 					}
 				}
diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc
index 822af1f..07d7f7f 100644
--- a/src/ASTAnalyses/Order/ordergraph.cc
+++ b/src/ASTAnalyses/Order/ordergraph.cc
@@ -12,7 +12,7 @@ OrderGraph::OrderGraph(Order *_order) :
 }
 
 OrderGraph *buildOrderGraph(Order *order) {
-        ASSERT(order->graph == NULL);
+	ASSERT(order->graph == NULL);
 	OrderGraph *orderGraph = new OrderGraph(order);
 	order->graph = orderGraph;
 	uint constrSize = order->constraints.getSize();
@@ -24,7 +24,7 @@ OrderGraph *buildOrderGraph(Order *order) {
 
 //Builds only the subgraph for the must order graph.
 OrderGraph *buildMustOrderGraph(Order *order) {
-        ASSERT(order->graph == NULL);
+	ASSERT(order->graph == NULL);
 	OrderGraph *orderGraph = new OrderGraph(order);
 	uint constrSize = order->constraints.getSize();
 	for (uint j = 0; j < constrSize; j++) {
@@ -180,23 +180,23 @@ OrderGraph::~OrderGraph() {
 	delete edges;
 }
 
-bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
+bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) {
 	HashsetOrderNode visited;
 	visited.add(source);
 	SetIteratorOrderEdge *iterator = source->outEdges.iterator();
 	bool found = false;
-	while(iterator->hasNext()){
-		OrderEdge* edge = iterator->next();
-		if(edge->polPos){
-			OrderNode* node = edge->sink;
-			if(!visited.contains(node)){
-				if( node == destination ){
+	while (iterator->hasNext()) {
+		OrderEdge *edge = iterator->next();
+		if (edge->polPos) {
+			OrderNode *node = edge->sink;
+			if (!visited.contains(node)) {
+				if ( node == destination ) {
 					found = true;
 					break;
 				}
 				visited.add(node);
-				found =isTherePathVisit(visited, node, destination);
-				if(found){
+				found = isTherePathVisit(visited, node, destination);
+				if (found) {
 					break;
 				}
 			}
@@ -206,19 +206,19 @@ bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
 	return found;
 }
 
-bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination){
+bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination) {
 	SetIteratorOrderEdge *iterator = current->outEdges.iterator();
 	bool found = false;
-	while(iterator->hasNext()){
-		OrderEdge* edge = iterator->next();
-		if(edge->polPos){
-			OrderNode* node = edge->sink;
-			if(node == destination){
+	while (iterator->hasNext()) {
+		OrderEdge *edge = iterator->next();
+		if (edge->polPos) {
+			OrderNode *node = edge->sink;
+			if (node == destination) {
 				found = true;
 				break;
 			}
 			visited.add(node);
-			if(isTherePathVisit(visited, node, destination)){
+			if (isTherePathVisit(visited, node, destination)) {
 				found = true;
 				break;
 			}
diff --git a/src/ASTAnalyses/Order/ordergraph.h b/src/ASTAnalyses/Order/ordergraph.h
index a155c7f..2bb8812 100644
--- a/src/ASTAnalyses/Order/ordergraph.h
+++ b/src/ASTAnalyses/Order/ordergraph.h
@@ -24,9 +24,9 @@ public:
 	void addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
 	void addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr);
 	OrderEdge *getInverseOrderEdge(OrderEdge *edge);
-	Order *getOrder() {return order;} 
-	bool isTherePath(OrderNode* source, OrderNode* destination);
-	bool isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination);
+	Order *getOrder() {return order;}
+	bool isTherePath(OrderNode *source, OrderNode *destination);
+	bool isTherePathVisit(HashsetOrderNode &visited, OrderNode *current, OrderNode *destination);
 	SetIteratorOrderNode *getNodes() {return nodes->iterator();}
 	SetIteratorOrderEdge *getEdges() {return edges->iterator();}
 
diff --git a/src/ASTAnalyses/Polarity/polarityassignment.cc b/src/ASTAnalyses/Polarity/polarityassignment.cc
index 0be8066..6254832 100644
--- a/src/ASTAnalyses/Polarity/polarityassignment.cc
+++ b/src/ASTAnalyses/Polarity/polarityassignment.cc
@@ -46,10 +46,10 @@ void computePredicatePolarity(BooleanPredicate *This) {
 }
 
 void computeLogicOpPolarity(BooleanLogic *This) {
-	Polarity child=computeLogicOpPolarityChildren(This);
+	Polarity child = computeLogicOpPolarityChildren(This);
 	uint size = This->inputs.getSize();
 	for (uint i = 0; i < size; i++) {
-		BooleanEdge b=This->inputs.get(i);
+		BooleanEdge b = This->inputs.get(i);
 		computePolarity(b.getBoolean(), b.isNegated() ? negatePolarity(child) : child);
 	}
 }
diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 3791b10..3b8571d 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -28,8 +28,8 @@ DecomposeOrderTransform::~DecomposeOrderTransform() {
 
 void DecomposeOrderTransform::doTransform() {
 	HashsetOrder *orders = solver->getActiveOrders()->copy();
-	SetIteratorOrder * orderit=orders->iterator();
-	while(orderit->hasNext()) {
+	SetIteratorOrder *orderit = orders->iterator();
+	while (orderit->hasNext()) {
 		Order *order = orderit->next();
 
 		if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0) {
@@ -60,12 +60,12 @@ void DecomposeOrderTransform::doTransform() {
 			}
 		}
 
-		
+
 		bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff);
 
 		if (mustReachPrune)
 			removeMustBeTrueNodes(solver, graph);
-		
+
 		//This is needed for splitorder
 		computeStronglyConnectedComponentGraph(graph);
 		decomposeOrder(order, graph);
diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 25ef990..1b34bae 100644
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -17,8 +17,8 @@ IntegerEncodingTransform::~IntegerEncodingTransform() {
 
 void IntegerEncodingTransform::doTransform() {
 	HashsetOrder *orders = solver->getActiveOrders()->copy();
-	SetIteratorOrder * orderit=orders->iterator();
-	while(orderit->hasNext()) {
+	SetIteratorOrder *orderit = orders->iterator();
+	while (orderit->hasNext()) {
 		Order *order = orderit->next();
 		if (GETVARTUNABLE(solver->getTuner(), order->type, ORDERINTEGERENCODING, &onoff))
 			integerEncode(order);
diff --git a/src/ASTTransform/preprocess.cc b/src/ASTTransform/preprocess.cc
index 1e04fd0..1e60c19 100644
--- a/src/ASTTransform/preprocess.cc
+++ b/src/ASTTransform/preprocess.cc
@@ -15,10 +15,10 @@ Preprocess::~Preprocess() {
 void Preprocess::doTransform() {
 	if (solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
 		return;
-	
+
 	BooleanIterator bit(solver);
-	while(bit.hasNext()) {
-		Boolean *b=bit.next();
+	while (bit.hasNext()) {
+		Boolean *b = bit.next();
 		if (b->type == BOOLEANVAR)
 			processBooleanVar((BooleanVar *)b);
 	}
@@ -26,7 +26,7 @@ void Preprocess::doTransform() {
 }
 
 void Preprocess::resolveBooleanVars() {
-	SetIteratorBoolean * iterator = toremove.iterator();
+	SetIteratorBoolean *iterator = toremove.iterator();
 	while (iterator->hasNext()) {
 		BooleanVar *bv = (BooleanVar *) iterator->next();
 		if (bv->polarity == P_TRUE) {
@@ -38,9 +38,9 @@ void Preprocess::resolveBooleanVars() {
 	delete iterator;
 }
 
-void Preprocess::processBooleanVar(BooleanVar * b) {
-	if (b->polarity==P_TRUE ||
-			b->polarity==P_FALSE) {
+void Preprocess::processBooleanVar(BooleanVar *b) {
+	if (b->polarity == P_TRUE ||
+			b->polarity == P_FALSE) {
 		toremove.add(b);
 	}
 }
diff --git a/src/ASTTransform/preprocess.h b/src/ASTTransform/preprocess.h
index ea9800d..2bca8bc 100644
--- a/src/ASTTransform/preprocess.h
+++ b/src/ASTTransform/preprocess.h
@@ -4,15 +4,15 @@
 #include "transform.h"
 
 class Preprocess : public Transform {
- public:
+public:
 	Preprocess(CSolver *_solver);
 	~Preprocess();
 	void doTransform();
-	
+
 	CMEMALLOC;
- private:
+private:
 	HashsetBoolean toremove;
-	void processBooleanVar(BooleanVar * b);
+	void processBooleanVar(BooleanVar *b);
 	void resolveBooleanVars();
 };
 
diff --git a/src/Backend/orderpair.cc b/src/Backend/orderpair.cc
index abe29cc..e778247 100644
--- a/src/Backend/orderpair.cc
+++ b/src/Backend/orderpair.cc
@@ -15,21 +15,21 @@ OrderPair::OrderPair() :
 	constraint(E_NULL) {
 }
 
-OrderPair::~OrderPair(){
+OrderPair::~OrderPair() {
 }
 
-Edge OrderPair::getConstraint(){
+Edge OrderPair::getConstraint() {
 	return constraint;
 }
 
-Edge OrderPair::getNegatedConstraint(){
+Edge OrderPair::getNegatedConstraint() {
 	return constraintNegate(constraint);
 }
 
-bool OrderPair::getConstraintValue(CSolver* solver){
+bool OrderPair::getConstraintValue(CSolver *solver) {
 	return getValueCNF(solver->getSATEncoder()->getCNF(), constraint);
 }
 
-bool OrderPair::getNegatedConstraintValue(CSolver* solver){
+bool OrderPair::getNegatedConstraintValue(CSolver *solver) {
 	return getValueCNF(solver->getSATEncoder()->getCNF(), constraintNegate(constraint));
 }
diff --git a/src/Backend/orderpair.h b/src/Backend/orderpair.h
index f650648..7c1cabd 100644
--- a/src/Backend/orderpair.h
+++ b/src/Backend/orderpair.h
@@ -18,11 +18,11 @@ public:
 	OrderPair();
 	virtual ~OrderPair();
 	virtual Edge getConstraint();
-	virtual bool getConstraintValue(CSolver* solver);
+	virtual bool getConstraintValue(CSolver *solver);
 	//for the cases that we swap first and second ... For total order is straight forward.
 	// but for partial order it has some complexity which should be hidden ... -HG
 	virtual Edge getNegatedConstraint();
-	virtual bool getNegatedConstraintValue(CSolver* solver);
+	virtual bool getNegatedConstraintValue(CSolver *solver);
 	uint64_t first;
 	uint64_t second;
 	CMEMALLOC;
diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index fdeee9e..2a58c06 100644
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -37,7 +37,7 @@ void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
 
 Edge SATEncoder::encodeConstraintSATEncoder(BooleanEdge c) {
 	Edge result;
-	Boolean * constraint = c.getBoolean();
+	Boolean *constraint = c.getBoolean();
 
 	if (booledgeMap.contains(constraint)) {
 		Edge e = {(Node *) booledgeMap.get(constraint)};
@@ -96,7 +96,7 @@ Edge SATEncoder::encodeLogicSATEncoder(BooleanLogic *constraint) {
 	case SATC_OR:
 	case SATC_XOR:
 	case SATC_IMPLIES:
-		//Don't handle, translate these away...
+	//Don't handle, translate these away...
 	default:
 		model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
 		exit(-1);
diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index d525bda..56614fa 100644
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -65,7 +65,7 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
 		flipped.second = pair->first;
 		pair = &flipped;
 	}
-	OrderPair* tmp;
+	OrderPair *tmp;
 	if (!(table->contains(pair))) {
 		tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder());
 		table->put(tmp, tmp);
@@ -81,8 +81,8 @@ Edge SATEncoder::getPartialPairConstraint(Order *order, OrderPair *pair) {
 		return gvalue;
 
 	HashtableOrderPair *table = order->getOrderPairTable();
-	
-	OrderPair* tmp;
+
+	OrderPair *tmp;
 	if (!(table->contains(pair))) {
 		Edge constraint = getNewVarSATEncoder();
 		tmp = new OrderPair(pair->first, pair->second, constraint);
@@ -104,7 +104,7 @@ Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
 		boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
 		bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
 		if (doOptOrderStructure) {
-                        ASSERT(boolOrder->order->graph == NULL);
+			ASSERT(boolOrder->order->graph == NULL);
 			boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
 			reachMustAnalysis(solver, boolOrder->order->graph, true);
 		}
@@ -153,7 +153,7 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
 	Edge uoIJ = constraintAND2(cnf, constraintNegate(ij), constraintNegate(ji));
 	Edge uoJK = constraintAND2(cnf, constraintNegate(jk), constraintNegate(kj));
 	Edge uoIK = constraintAND2(cnf, constraintNegate(ik), constraintNegate(ki));
-		
+
 	Edge t1[] = {ij, jk, ik};
 	Edge t2[] = {ji, jk, ik};
 	Edge t3[] = {ij, kj, ki};
@@ -166,7 +166,7 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
 	Edge ct4 = constraintAND(cnf, 3, t4);
 	Edge ct5 = constraintAND(cnf, 3, t5);
 	Edge ct6 = constraintAND(cnf, 3, t6);
-	
+
 	Edge p1[] = {uoIJ, jk, ik};
 	Edge p2[] = {ij, kj, uoIK};
 	Edge p3[] = {ji, uoJK, ki};
@@ -179,7 +179,7 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
 	Edge cp4 = constraintAND(cnf, 3, p4);
 	Edge cp5 = constraintAND(cnf, 3, p5);
 	Edge cp6 = constraintAND(cnf, 3, p6);
-	
+
 	Edge o1[] = {uoIJ, uoJK, ik};
 	Edge o2[] = {ij, uoJK, uoIK};
 	Edge o3[] = {uoIK, jk, uoIK};
@@ -192,15 +192,15 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
 	Edge co4 = constraintAND(cnf, 3, o4);
 	Edge co5 = constraintAND(cnf, 3, o5);
 	Edge co6 = constraintAND(cnf, 3, o6);
-	
+
 	Edge unorder [] = {uoIJ, uoJK, uoIK};
 	Edge cunorder = constraintAND(cnf, 3, unorder);
-	
-	
+
+
 	Edge res[] = {ct1,ct2,ct3,ct4,ct5,ct6,
-			cp1,cp2,cp3,cp4,cp5,cp6,
-			co1,co2,co3,co4,co5,co6,
-			cunorder};
+								cp1,cp2,cp3,cp4,cp5,cp6,
+								co1,co2,co3,co4,co5,co6,
+								cunorder};
 	return constraintOR(cnf, 19, res);
 }
 
@@ -248,7 +248,7 @@ void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) {
 				Edge constKI = getPartialPairConstraint(order, &pairKI);
 				Edge constKJ = getPartialPairConstraint(order, &pairKJ);
 				addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI,
-					constJK, constKJ, constIK, constKI));
+																																				constJK, constKJ, constIK, constKI));
 			}
 		}
 	}
diff --git a/src/Collections/corestructs.h b/src/Collections/corestructs.h
index 5e8a7de..7a8104d 100644
--- a/src/Collections/corestructs.h
+++ b/src/Collections/corestructs.h
@@ -10,32 +10,32 @@
 #define PTRSHIFT 5
 
 class BooleanEdge {
- public:
- BooleanEdge() : b(NULL) {}
- BooleanEdge(Boolean * _b) : b(_b) {}
+public:
+	BooleanEdge() : b(NULL) {}
+	BooleanEdge(Boolean *_b) : b(_b) {}
 	BooleanEdge negate() {return BooleanEdge((Boolean *)(((uintptr_t) b) ^ 1));}
-	bool operator==(BooleanEdge e) { return b==e.b;}
-	bool operator!=(BooleanEdge e) { return b!=e.b;}
+	bool operator==(BooleanEdge e) { return b == e.b;}
+	bool operator!=(BooleanEdge e) { return b != e.b;}
 	bool isNegated() { return ((uintptr_t) b) & 1; }
-	Boolean * getBoolean() {return (Boolean *)(((uintptr_t)b) & ~((uintptr_t) 1));}
-	Boolean * getRaw() {return b;}
-	Boolean * operator->() {return getBoolean();}
+	Boolean *getBoolean() {return (Boolean *)(((uintptr_t)b) & ~((uintptr_t) 1));}
+	Boolean *getRaw() {return b;}
+	Boolean *operator->() {return getBoolean();}
 	operator bool() const {return b != NULL;}
- private:
+private:
 	Boolean *b;
 };
 
 inline bool boolEdgeEquals(BooleanEdge b1, BooleanEdge b2) {
-	return b1==b2;
+	return b1 == b2;
 }
 
 inline unsigned int boolEdgeHash(BooleanEdge b) {
-	return (unsigned int) (((uintptr_t)b.getRaw())>>PTRSHIFT);
+	return (unsigned int) (((uintptr_t)b.getRaw()) >> PTRSHIFT);
 }
-									
-typedef Hashset<BooleanEdge, uintptr_t, PTRSHIFT, & boolEdgeHash, & boolEdgeEquals> HashsetBooleanEdge;
+
+typedef Hashset<BooleanEdge, uintptr_t, PTRSHIFT, &boolEdgeHash, &boolEdgeEquals> HashsetBooleanEdge;
 typedef Hashset<Order *, uintptr_t, PTRSHIFT> HashsetOrder;
-typedef SetIterator<BooleanEdge, uintptr_t, PTRSHIFT, & boolEdgeHash, & boolEdgeEquals> SetIteratorBooleanEdge;
+typedef SetIterator<BooleanEdge, uintptr_t, PTRSHIFT, &boolEdgeHash, &boolEdgeEquals> SetIteratorBooleanEdge;
 typedef SetIterator<Order *, uintptr_t, PTRSHIFT> SetIteratorOrder;
 
 #endif
diff --git a/src/Collections/qsort.cc b/src/Collections/qsort.cc
index 0c415b5..f4e7ec9 100644
--- a/src/Collections/qsort.cc
+++ b/src/Collections/qsort.cc
@@ -75,23 +75,23 @@
  * isn't worth optimizing; the SWAP's get sped up by the cache, and pointer
  * arithmetic gets lost in the time required for comparison function calls.
  */
-#define	SWAP(a, b, count, size, tmp) { \
-	count = size; \
-	do { \
-		tmp = *a; \
-		*a++ = *b; \
-		*b++ = tmp; \
-	} while (--count); \
+#define SWAP(a, b, count, size, tmp) { \
+		count = size; \
+		do { \
+			tmp = *a; \
+			*a++ = *b; \
+			*b++ = tmp; \
+		} while (--count); \
 }
 
 /* Copy one block of size size to another. */
 #define COPY(a, b, count, size, tmp1, tmp2) { \
-	count = size; \
-	tmp1 = a; \
-	tmp2 = b; \
-	do { \
-		*tmp1++ = *tmp2++; \
-	} while (--count); \
+		count = size; \
+		tmp1 = a; \
+		tmp2 = b; \
+		do { \
+			*tmp1++ = *tmp2++; \
+		} while (--count); \
 }
 
 /*
@@ -102,18 +102,18 @@
  * j < nmemb, select largest of Ki, Kj and Kj+1.
  */
 #define CREATE(initval, nmemb, par_i, child_i, par, child, size, count, tmp) { \
-	for (par_i = initval; (child_i = par_i * 2) <= nmemb; \
-	    par_i = child_i) { \
-		child = base + child_i * size; \
-		if (child_i < nmemb && compar(child, child + size) < 0) { \
-			child += size; \
-			++child_i; \
+		for (par_i = initval; (child_i = par_i * 2) <= nmemb; \
+				 par_i = child_i) { \
+			child = base + child_i * size; \
+			if (child_i < nmemb && compar(child, child + size) < 0) { \
+				child += size; \
+				++child_i; \
+			} \
+			par = base + par_i * size; \
+			if (compar(child, par) <= 0) \
+				break; \
+			SWAP(par, child, count, size, tmp); \
 		} \
-		par = base + par_i * size; \
-		if (compar(child, par) <= 0) \
-			break; \
-		SWAP(par, child, count, size, tmp); \
-	} \
 }
 
 /*
@@ -134,26 +134,26 @@
  * XXX Don't break the #define SELECT line, below.  Reiser cpp gets upset.
  */
 #define SELECT(par_i, child_i, nmemb, par, child, size, k, count, tmp1, tmp2) { \
-	for (par_i = 1; (child_i = par_i * 2) <= nmemb; par_i = child_i) { \
-		child = base + child_i * size; \
-		if (child_i < nmemb && compar(child, child + size) < 0) { \
-			child += size; \
-			++child_i; \
+		for (par_i = 1; (child_i = par_i * 2) <= nmemb; par_i = child_i) { \
+			child = base + child_i * size; \
+			if (child_i < nmemb && compar(child, child + size) < 0) { \
+				child += size; \
+				++child_i; \
+			} \
+			par = base + par_i * size; \
+			COPY(par, child, count, size, tmp1, tmp2); \
 		} \
-		par = base + par_i * size; \
-		COPY(par, child, count, size, tmp1, tmp2); \
-	} \
-	for (;;) { \
-		child_i = par_i; \
-		par_i = child_i / 2; \
-		child = base + child_i * size; \
-		par = base + par_i * size; \
-		if (child_i == 1 || compar(k, par) < 0) { \
-			COPY(child, k, count, size, tmp1, tmp2); \
-			break; \
+		for (;; ) { \
+			child_i = par_i; \
+			par_i = child_i / 2; \
+			child = base + child_i * size; \
+			par = base + par_i * size; \
+			if (child_i == 1 || compar(k, par) < 0) { \
+				COPY(child, k, count, size, tmp1, tmp2); \
+				break; \
+			} \
+			COPY(child, par, count, size, tmp1, tmp2); \
 		} \
-		COPY(child, par, count, size, tmp1, tmp2); \
-	} \
 }
 
 /*
@@ -165,7 +165,7 @@
  */
 int
 bsdheapsort(void *vbase, size_t nmemb, size_t size,
-    int (*compar)(const void *, const void *))
+						int (*compar)(const void *, const void *))
 {
 	size_t cnt, i, j, l;
 	char tmp, *tmp1, *tmp2;
@@ -188,7 +188,7 @@ bsdheapsort(void *vbase, size_t nmemb, size_t size,
 	 */
 	base = (char *)vbase - size;
 
-	for (l = nmemb / 2 + 1; --l;)
+	for (l = nmemb / 2 + 1; --l; )
 		CREATE(l, nmemb, i, j, t, p, size, cnt, tmp);
 
 	/*
@@ -207,10 +207,10 @@ bsdheapsort(void *vbase, size_t nmemb, size_t size,
 }
 
 
-static __inline char	*med3(char *, char *, char *, int (*)(const void *, const void *));
-static __inline void	 swapfunc(char *, char *, size_t, int);
+static __inline char  *med3(char *, char *, char *, int (*)(const void *, const void *));
+static __inline void swapfunc(char *, char *, size_t, int);
 
-#define min(a, b)	(a) < (b) ? a : b
+#define min(a, b) (a) < (b) ? a : b
 
 /*
  * Qsort routine from Bentley & McIlroy's "Engineering a Sort Function".
@@ -230,24 +230,24 @@ static __inline void	 swapfunc(char *, char *, size_t, int);
  *   4. Tail recursion is eliminated when sorting the larger of two
  *	subpartitions to save stack space.
  */
-#define SWAPTYPE_BYTEV	1
-#define SWAPTYPE_INTV	2
-#define SWAPTYPE_LONGV	3
-#define SWAPTYPE_INT	4
-#define SWAPTYPE_LONG	5
+#define SWAPTYPE_BYTEV  1
+#define SWAPTYPE_INTV 2
+#define SWAPTYPE_LONGV  3
+#define SWAPTYPE_INT  4
+#define SWAPTYPE_LONG 5
 
-#define TYPE_ALIGNED(TYPE, a, es)			\
+#define TYPE_ALIGNED(TYPE, a, es)     \
 	(((char *)a - (char *)0) % sizeof(TYPE) == 0 && es % sizeof(TYPE) == 0)
 
-#define swapcode(TYPE, parmi, parmj, n) { 		\
-	size_t i = (n) / sizeof (TYPE); 		\
-	TYPE *pi = (TYPE *) (parmi); 			\
-	TYPE *pj = (TYPE *) (parmj); 			\
-	do { 						\
-		TYPE	t = *pi;			\
-		*pi++ = *pj;				\
-		*pj++ = t;				\
-        } while (--i > 0);				\
+#define swapcode(TYPE, parmi, parmj, n) {     \
+		size_t i = (n) / sizeof (TYPE);     \
+		TYPE *pi = (TYPE *) (parmi);      \
+		TYPE *pj = (TYPE *) (parmj);      \
+		do {            \
+			TYPE t = *pi;      \
+			*pi++ = *pj;        \
+			*pj++ = t;        \
+		} while (--i > 0);        \
 }
 
 static __inline void
@@ -268,47 +268,47 @@ swapfunc(char *a, char *b, size_t n, int swaptype)
 	}
 }
 
-#define swap(a, b)	do {				\
-	switch (swaptype) {				\
-	case SWAPTYPE_INT: {				\
-		int t = *(int *)(a);			\
-		*(int *)(a) = *(int *)(b);		\
-		*(int *)(b) = t;			\
-		break;					\
-	    }						\
-	case SWAPTYPE_LONG: {				\
-		long t = *(long *)(a);			\
-		*(long *)(a) = *(long *)(b);		\
-		*(long *)(b) = t;			\
-		break;					\
-	    }						\
-	default:					\
-		swapfunc(a, b, es, swaptype);		\
-	}						\
+#define swap(a, b)  do {        \
+		switch (swaptype) {       \
+		case SWAPTYPE_INT: {        \
+			int t = *(int *)(a);      \
+			*(int *)(a) = *(int *)(b);    \
+			*(int *)(b) = t;      \
+			break;          \
+		}           \
+		case SWAPTYPE_LONG: {       \
+			long t = *(long *)(a);      \
+			*(long *)(a) = *(long *)(b);    \
+			*(long *)(b) = t;     \
+			break;          \
+		}           \
+		default:          \
+			swapfunc(a, b, es, swaptype);   \
+		}           \
 } while (0)
 
-#define vecswap(a, b, n) 	if ((n) > 0) swapfunc(a, b, n, swaptype)
+#define vecswap(a, b, n)  if ((n) > 0) swapfunc(a, b, n, swaptype)
 
 static __inline char *
 med3(char *a, char *b, char *c, int (*cmp)(const void *, const void *))
 {
 	return cmp(a, b) < 0 ?
-	       (cmp(b, c) < 0 ? b : (cmp(a, c) < 0 ? c : a ))
-              :(cmp(b, c) > 0 ? b : (cmp(a, c) < 0 ? a : c ));
+				 (cmp(b, c) < 0 ? b : (cmp(a, c) < 0 ? c : a))
+				 : (cmp(b, c) > 0 ? b : (cmp(a, c) < 0 ? a : c));
 }
 
 static void
 introsort(char *a, size_t n, size_t es, size_t maxdepth, int swaptype,
-    int (*cmp)(const void *, const void *))
+					int (*cmp)(const void *, const void *))
 {
 	char *pa, *pb, *pc, *pd, *pl, *pm, *pn;
 	int cmp_result;
 	size_t r, s;
 
-loop:	if (n < 7) {
+loop: if (n < 7) {
 		for (pm = a + es; pm < a + n * es; pm += es)
 			for (pl = pm; pl > a && cmp(pl - es, pl) > 0;
-			     pl -= es)
+					 pl -= es)
 				swap(pl, pl - es);
 		return;
 	}
@@ -332,7 +332,7 @@ loop:	if (n < 7) {
 	swap(a, pm);
 	pa = pb = a + es;
 	pc = pd = a + (n - 1) * es;
-	for (;;) {
+	for (;; ) {
 		while (pb <= pc && (cmp_result = cmp(pb, a)) <= 0) {
 			if (cmp_result == 0) {
 				swap(pa, pb);
@@ -370,7 +370,7 @@ loop:	if (n < 7) {
 		if (s > es) {
 			if (r > es) {
 				introsort(a, r / es, es, maxdepth,
-				    swaptype, cmp);
+									swaptype, cmp);
 			}
 			a = pn - s;
 			n = s / es;
@@ -381,7 +381,7 @@ loop:	if (n < 7) {
 		if (r > es) {
 			if (s > es) {
 				introsort(pn - s, s / es, es, maxdepth,
-				    swaptype, cmp);
+									swaptype, cmp);
 			}
 			n = r / es;
 			goto loop;
diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index 80ec918..6c53253 100644
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -81,7 +81,7 @@
 	void setVector ## name(Vector ## name * vector, uint index, type item) { \
 		vector->array[index] = item;                                          \
 	}                                                                     \
-	uint getSizeVector ## name(const Vector ## name * vector) {						\
+	uint getSizeVector ## name(const Vector ## name * vector) {           \
 		return vector->size;                                                \
 	}                                                                     \
 	void deleteVector ## name(Vector ## name * vector) {                     \
diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index ace0313..e42f398 100644
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -28,7 +28,7 @@ void naiveEncodingConstraint(Boolean *This) {
 		return;
 	}
 	case ORDERCONST: {
-		if(((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
+		if (((BooleanOrder *) This)->order->encoding.type == ORDER_UNASSIGNED)
 			((BooleanOrder *) This)->order->setOrderEncodingType(PAIRWISE);
 		return;
 	}
diff --git a/src/Encoders/orderencoding.cc b/src/Encoders/orderencoding.cc
index 556554e..e3c150a 100644
--- a/src/Encoders/orderencoding.cc
+++ b/src/Encoders/orderencoding.cc
@@ -8,8 +8,8 @@ OrderEncoding::OrderEncoding(Order *_order) :
 {
 }
 
-OrderEncoding::~OrderEncoding(){
-	if(resolver!= NULL){
+OrderEncoding::~OrderEncoding() {
+	if (resolver != NULL) {
 		delete resolver;
 	}
 }
diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index fc4cd7b..cd1e1a2 100644
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -1,8 +1,8 @@
 
-/* 
+/*
  * File:   deserializer.cc
  * Author: hamed
- * 
+ *
  * Created on September 7, 2017, 6:08 PM
  */
 
@@ -15,11 +15,11 @@
 #include "element.h"
 #include "mutableset.h"
 
-Deserializer::Deserializer(const char* file):
+Deserializer::Deserializer(const char *file) :
 	solver(new CSolver())
 {
 	filedesc = open(file, O_RDONLY);
- 
+
 	if (filedesc < 0) {
 		exit(-1);
 	}
@@ -27,98 +27,98 @@ Deserializer::Deserializer(const char* file):
 
 Deserializer::~Deserializer() {
 	delete solver;
-	
-	if (-1 == close(filedesc)){
+
+	if (-1 == close(filedesc)) {
 		exit(-1);
 	}
 }
 
-ssize_t Deserializer::myread(void* __buf, size_t __nbytes){
+ssize_t Deserializer::myread(void *__buf, size_t __nbytes) {
 	return read (filedesc, __buf, __nbytes);
 }
 
-CSolver * Deserializer::deserialize(){
+CSolver *Deserializer::deserialize() {
 	ASTNodeType nodeType;
-	while(myread(&nodeType, sizeof(ASTNodeType) ) >0){
-		switch(nodeType){
-			case BOOLEANEDGE:
-				deserializeBooleanEdge();
-				break;
-			case BOOLEANVAR:
-				deserializeBooleanVar();
-				break;
-			case ORDERCONST:
-				deserializeBooleanOrder();
-				break;
-			case ORDERTYPE:
-				deserializeOrder();
-				break;
-			case SETTYPE:
-				deserializeSet();
-				break;
-			case LOGICOP:
-				deserializeBooleanLogic();
-				break;
-			case PREDICATEOP:
-				deserializeBooleanPredicate();
-				break;
-			case PREDTABLETYPE:
-				deserializePredicateTable();
-				break;
-			case PREDOPERTYPE:
-				deserializePredicateOperator();
-				break;
-			case TABLETYPE:
-				deserializeTable();
-				break;
-			case ELEMSET:
-				deserializeElementSet();
-				break;
-			case ELEMCONST:
-				deserializeElementConst();
-				break;
-			case ELEMFUNCRETURN:
-				deserializeElementFunction();
-				break;
-			case FUNCOPTYPE:
-				deserializeFunctionOperator();
-				break;
-			case FUNCTABLETYPE:
-				deserializeFunctionTable();
-				break;
-			default:
-				ASSERT(0);
+	while (myread(&nodeType, sizeof(ASTNodeType) ) > 0) {
+		switch (nodeType) {
+		case BOOLEANEDGE:
+			deserializeBooleanEdge();
+			break;
+		case BOOLEANVAR:
+			deserializeBooleanVar();
+			break;
+		case ORDERCONST:
+			deserializeBooleanOrder();
+			break;
+		case ORDERTYPE:
+			deserializeOrder();
+			break;
+		case SETTYPE:
+			deserializeSet();
+			break;
+		case LOGICOP:
+			deserializeBooleanLogic();
+			break;
+		case PREDICATEOP:
+			deserializeBooleanPredicate();
+			break;
+		case PREDTABLETYPE:
+			deserializePredicateTable();
+			break;
+		case PREDOPERTYPE:
+			deserializePredicateOperator();
+			break;
+		case TABLETYPE:
+			deserializeTable();
+			break;
+		case ELEMSET:
+			deserializeElementSet();
+			break;
+		case ELEMCONST:
+			deserializeElementConst();
+			break;
+		case ELEMFUNCRETURN:
+			deserializeElementFunction();
+			break;
+		case FUNCOPTYPE:
+			deserializeFunctionOperator();
+			break;
+		case FUNCTABLETYPE:
+			deserializeFunctionTable();
+			break;
+		default:
+			ASSERT(0);
 		}
 	}
 	return solver;
 }
 
-void Deserializer::deserializeBooleanEdge(){
+void Deserializer::deserializeBooleanEdge() {
 	Boolean *b;
-	myread(&b, sizeof(Boolean*));
+	myread(&b, sizeof(Boolean *));
 	BooleanEdge tmp(b);
 	bool isNegated = tmp.isNegated();
 	ASSERT(map.contains(tmp.getBoolean()));
-	b = (Boolean*) map.get(tmp.getBoolean());
+	b = (Boolean *) map.get(tmp.getBoolean());
 	BooleanEdge res(b);
-	solver->addConstraint(isNegated?res.negate():res);
+	solver->addConstraint(isNegated ? res.negate() : res);
 }
 
-void Deserializer::deserializeBooleanVar(){
+void Deserializer::deserializeBooleanVar() {
 	BooleanVar *b;
-	myread(&b, sizeof(BooleanVar*));
+	myread(&b, sizeof(BooleanVar *));
 	VarType vtype;
 	myread(&vtype, sizeof(VarType));
 	map.put(b, solver->getBooleanVar(vtype).getBoolean());
 }
 
-void Deserializer::deserializeBooleanOrder(){
-	BooleanOrder* bo_ptr;
-	myread(&bo_ptr, sizeof(BooleanOrder*));
-	Order* order;
-	myread(&order, sizeof(Order*));
+void Deserializer::deserializeBooleanOrder() {
+	BooleanOrder *bo_ptr;
+	myread(&bo_ptr, sizeof(BooleanOrder *));
+	Order *order;
+	myread(&order, sizeof(Order *));
 	ASSERT(map.contains(order));
-	order  = (Order*) map.get(order);
+	order  = (Order *) map.get(order);
 	uint64_t first;
 	myread(&first, sizeof(uint64_t));
 	uint64_t second;
@@ -126,21 +126,21 @@ void Deserializer::deserializeBooleanOrder(){
 	map.put(bo_ptr, solver->orderConstraint(order, first, second).getBoolean());
 }
 
-void Deserializer::deserializeOrder(){
-	Order* o_ptr;
-	myread(&o_ptr, sizeof(Order*));
+void Deserializer::deserializeOrder() {
+	Order *o_ptr;
+	myread(&o_ptr, sizeof(Order *));
 	OrderType type;
 	myread(&type, sizeof(OrderType));
-	Set * set_ptr;
+	Set *set_ptr;
 	myread(&set_ptr, sizeof(Set *));
 	ASSERT(map.contains(set_ptr));
-	Set* set  = (Set*) map.get(set_ptr);
+	Set *set  = (Set *) map.get(set_ptr);
 	map.put(o_ptr, solver->createOrder(type, set));
 }
 
-void Deserializer::deserializeSet(){
+void Deserializer::deserializeSet() {
 	Set *s_ptr;
-	myread(&s_ptr, sizeof(Set*));
+	myread(&s_ptr, sizeof(Set *));
 	VarType type;
 	myread(&type, sizeof(VarType));
 	bool isRange;
@@ -152,29 +152,29 @@ void Deserializer::deserializeSet(){
 	bool isMutable;
 	myread(&isMutable, sizeof(bool));
 	Set *set;
-	if(isMutable){
+	if (isMutable) {
 		set = new MutableSet(type);
 	}
 	uint size;
 	myread(&size, sizeof(uint));
 	Vector<uint64_t> members;
-	for(uint i=0; i<size; i++){
+	for (uint i = 0; i < size; i++) {
 		uint64_t mem;
 		myread(&mem, sizeof(uint64_t));
-		if(isMutable) {
-			((MutableSet*) set)->addElementMSet(mem);
-		}else {
+		if (isMutable) {
+			((MutableSet *) set)->addElementMSet(mem);
+		} else {
 			members.push(mem);
 		}
 	}
-	if(!isMutable){
-		set = isRange? solver->createRangeSet(type, low, high):
-			solver->createSet(type, members.expose(), size);
+	if (!isMutable) {
+		set = isRange ? solver->createRangeSet(type, low, high) :
+					solver->createSet(type, members.expose(), size);
 	}
 	map.put(s_ptr, set);
 }
 
-void Deserializer::deserializeBooleanLogic(){
+void Deserializer::deserializeBooleanLogic() {
 	BooleanLogic *bl_ptr;
 	myread(&bl_ptr, sizeof(BooleanLogic *));
 	LogicOp op;
@@ -182,134 +182,134 @@ void Deserializer::deserializeBooleanLogic(){
 	uint size;
 	myread(&size, sizeof(uint));
 	Vector<BooleanEdge> members;
-	for(uint i=0; i<size; i++){
-		Boolean* member;
+	for (uint i = 0; i < size; i++) {
+		Boolean *member;
 		myread(&member, sizeof(Boolean *));
 		BooleanEdge tmp(member);
 		bool isNegated = tmp.isNegated();
 		ASSERT(map.contains(tmp.getBoolean()));
-		member = (Boolean*) map.get(tmp.getBoolean());
+		member = (Boolean *) map.get(tmp.getBoolean());
 		BooleanEdge res(member);
-		members.push( isNegated?res.negate():res );
+		members.push( isNegated ? res.negate() : res );
 	}
 	map.put(bl_ptr, solver->applyLogicalOperation(op, members.expose(), size).getBoolean());
 }
 
-void Deserializer::deserializeBooleanPredicate(){
+void Deserializer::deserializeBooleanPredicate() {
 	BooleanPredicate *bp_ptr;
 	myread(&bp_ptr, sizeof(BooleanPredicate *));
-	Predicate* predicate;
-	myread(&predicate, sizeof(Predicate*));
+	Predicate *predicate;
+	myread(&predicate, sizeof(Predicate *));
 	ASSERT(map.contains(predicate));
-	predicate = (Predicate*) map.get(predicate);
+	predicate = (Predicate *) map.get(predicate);
 	uint size;
 	myread(&size, sizeof(uint));
-	Vector<Element*> members;
-	for(uint i=0; i<size; i++){
-		Element* input;
+	Vector<Element *> members;
+	for (uint i = 0; i < size; i++) {
+		Element *input;
 		myread(&input, sizeof(Element *));
 		ASSERT(map.contains(input));
-		input = (Element*) map.get(input);
+		input = (Element *) map.get(input);
 		members.push(input);
 	}
-	
-	Boolean* stat_ptr;
+
+	Boolean *stat_ptr;
 	myread(&stat_ptr, sizeof(Boolean *));
 	BooleanEdge undefStatus;
-	if(stat_ptr != NULL){
+	if (stat_ptr != NULL) {
 		BooleanEdge tmp(stat_ptr);
 		bool isNegated = tmp.isNegated();
 		ASSERT(map.contains(tmp.getBoolean()));
-		stat_ptr = (Boolean*) map.get(tmp.getBoolean());
+		stat_ptr = (Boolean *) map.get(tmp.getBoolean());
 		BooleanEdge res(stat_ptr);
-		undefStatus = isNegated?res.negate():res;
+		undefStatus = isNegated ? res.negate() : res;
 	} else {
 		undefStatus = NULL;
 	}
 	map.put(bp_ptr, solver->applyPredicateTable(predicate, members.expose(), size, undefStatus).getBoolean());
 }
 
-void Deserializer::deserializePredicateTable(){
+void Deserializer::deserializePredicateTable() {
 	PredicateTable *pt_ptr;
 	myread(&pt_ptr, sizeof(PredicateTable *));
-	Table* table;
-	myread(&table, sizeof(Table*));
+	Table *table;
+	myread(&table, sizeof(Table *));
 	ASSERT(map.contains(table));
-	table = (Table*) map.get(table);
+	table = (Table *) map.get(table);
 	UndefinedBehavior undefinedbehavior;
 	myread(&undefinedbehavior, sizeof(UndefinedBehavior));
-	
+
 	map.put(pt_ptr, solver->createPredicateTable(table, undefinedbehavior));
 }
 
-void Deserializer::deserializePredicateOperator(){
+void Deserializer::deserializePredicateOperator() {
 	PredicateOperator *po_ptr;
 	myread(&po_ptr, sizeof(PredicateOperator *));
 	CompOp op;
 	myread(&op, sizeof(CompOp));
 	uint size;
 	myread(&size, sizeof(uint));
-	Vector<Set*> domains;
-	for(uint i=0; i<size; i++){
-		Set* domain;
-		myread(&domain, sizeof(Set*));
+	Vector<Set *> domains;
+	for (uint i = 0; i < size; i++) {
+		Set *domain;
+		myread(&domain, sizeof(Set *));
 		ASSERT(map.contains(domain));
-		domain = (Set*) map.get(domain);
+		domain = (Set *) map.get(domain);
 		domains.push(domain);
 	}
 
 	map.put(po_ptr, solver->createPredicateOperator(op, domains.expose(), size));
 }
 
-void Deserializer::deserializeTable(){
+void Deserializer::deserializeTable() {
 	Table *t_ptr;
 	myread(&t_ptr, sizeof(Table *));
 	uint size;
 	myread(&size, sizeof(uint));
-	Vector<Set*> domains;
-	for(uint i=0; i<size; i++){
-		Set* domain;
-		myread(&domain, sizeof(Set*));
+	Vector<Set *> domains;
+	for (uint i = 0; i < size; i++) {
+		Set *domain;
+		myread(&domain, sizeof(Set *));
 		ASSERT(map.contains(domain));
-		domain = (Set*) map.get(domain);
+		domain = (Set *) map.get(domain);
 		domains.push(domain);
 	}
-	Set* range;
-	myread(&range, sizeof(Set*));
-	if(range != NULL){
+	Set *range;
+	myread(&range, sizeof(Set *));
+	if (range != NULL) {
 		ASSERT(map.contains(range));
-		range = (Set*) map.get(range);
+		range = (Set *) map.get(range);
 	}
-	Table* table = solver->createTable(domains.expose(), size, range);
+	Table *table = solver->createTable(domains.expose(), size, range);
 	myread(&size, sizeof(uint));
-	for(uint i=0; i<size; i++){
+	for (uint i = 0; i < size; i++) {
 		uint64_t output;
 		myread(&output, sizeof(uint64_t));
 		uint inputSize;
 		myread(&inputSize, sizeof(uint));
 		Vector<uint64_t> inputs;
 		inputs.setSize(inputSize);
-		myread(inputs.expose(), sizeof(uint64_t)*inputSize);
+		myread(inputs.expose(), sizeof(uint64_t) * inputSize);
 		table->addNewTableEntry(inputs.expose(), inputSize, output);
 	}
-	
+
 	map.put(t_ptr, table);
 }
 
 
-void Deserializer::deserializeElementSet(){
-	ElementSet* es_ptr;
-	myread(&es_ptr, sizeof(ElementSet*));
-	Set * set;
+void Deserializer::deserializeElementSet() {
+	ElementSet *es_ptr;
+	myread(&es_ptr, sizeof(ElementSet *));
+	Set *set;
 	myread(&set, sizeof(Set *));
 	ASSERT(map.contains(set));
-	set  = (Set*) map.get(set);
+	set  = (Set *) map.get(set);
 	map.put(es_ptr, solver->getElementVar(set));
 }
 
-void Deserializer::deserializeElementConst(){
-	ElementSet* es_ptr;
-	myread(&es_ptr, sizeof(ElementSet*));
+void Deserializer::deserializeElementConst() {
+	ElementSet *es_ptr;
+	myread(&es_ptr, sizeof(ElementSet *));
 	VarType type;
 	myread(&type, sizeof(VarType));
 	uint64_t value;
@@ -317,70 +317,70 @@ void Deserializer::deserializeElementConst(){
 	map.put(es_ptr, solver->getElementConst(type, value));
 }
 
-void Deserializer::deserializeElementFunction(){
+void Deserializer::deserializeElementFunction() {
 	ElementFunction *ef_ptr;
 	myread(&ef_ptr, sizeof(ElementFunction *));
 	Function *function;
-	myread(&function, sizeof(Function*));
+	myread(&function, sizeof(Function *));
 	ASSERT(map.contains(function));
-	function = (Function*) map.get(function);
+	function = (Function *) map.get(function);
 	uint size;
 	myread(&size, sizeof(uint));
-	Vector<Element*> members;
-	for(uint i=0; i<size; i++){
-		Element* input;
+	Vector<Element *> members;
+	for (uint i = 0; i < size; i++) {
+		Element *input;
 		myread(&input, sizeof(Element *));
 		ASSERT(map.contains(input));
-		input = (Element*) map.get(input);
+		input = (Element *) map.get(input);
 		members.push(input);
 	}
-	
-	Boolean* overflowstatus;
+
+	Boolean *overflowstatus;
 	myread(&overflowstatus, sizeof(Boolean *));
 	BooleanEdge tmp(overflowstatus);
 	bool isNegated = tmp.isNegated();
 	ASSERT(map.contains(tmp.getBoolean()));
-	overflowstatus = (Boolean*) map.get(tmp.getBoolean());
+	overflowstatus = (Boolean *) map.get(tmp.getBoolean());
 	BooleanEdge res(overflowstatus);
-	BooleanEdge undefStatus = isNegated?res.negate():res;
-	
+	BooleanEdge undefStatus = isNegated ? res.negate() : res;
+
 	map.put(ef_ptr, solver->applyFunction(function, members.expose(), size, undefStatus));
 }
 
 
-void Deserializer::deserializeFunctionOperator(){
+void Deserializer::deserializeFunctionOperator() {
 	FunctionOperator *fo_ptr;
 	myread(&fo_ptr, sizeof(FunctionOperator *));
 	ArithOp op;
 	myread(&op, sizeof(ArithOp));
 	uint size;
 	myread(&size, sizeof(uint));
-	Vector<Set*> domains;
-	for(uint i=0; i<size; i++){
-		Set* domain;
-		myread(&domain, sizeof(Set*));
+	Vector<Set *> domains;
+	for (uint i = 0; i < size; i++) {
+		Set *domain;
+		myread(&domain, sizeof(Set *));
 		ASSERT(map.contains(domain));
-		domain = (Set*) map.get(domain);
+		domain = (Set *) map.get(domain);
 		domains.push(domain);
 	}
-	Set* range;
-	myread(&range, sizeof(Set*));
+	Set *range;
+	myread(&range, sizeof(Set *));
 	ASSERT(map.contains(range));
-	range = (Set*) map.get(range);
+	range = (Set *) map.get(range);
 	OverFlowBehavior overflowbehavior;
 	myread(&overflowbehavior, sizeof(OverFlowBehavior));
 	map.put(fo_ptr, solver->createFunctionOperator(op, domains.expose(), size, range, overflowbehavior));
 }
 
-void Deserializer::deserializeFunctionTable(){
+void Deserializer::deserializeFunctionTable() {
 	FunctionTable *ft_ptr;
 	myread(&ft_ptr, sizeof(FunctionTable *));
-	Table* table;
-	myread(&table, sizeof(Table*));
+	Table *table;
+	myread(&table, sizeof(Table *));
 	ASSERT(map.contains(table));
-	table = (Table*) map.get(table);
+	table = (Table *) map.get(table);
 	UndefinedBehavior undefinedbehavior;
 	myread(&undefinedbehavior, sizeof(UndefinedBehavior));
-	
+
 	map.put(ft_ptr, solver->completeTable(table, undefinedbehavior));
 }
\ No newline at end of file
diff --git a/src/Serialize/deserializer.h b/src/Serialize/deserializer.h
index 057346d..6335c89 100644
--- a/src/Serialize/deserializer.h
+++ b/src/Serialize/deserializer.h
@@ -1,5 +1,5 @@
 
-/* 
+/*
  * File:   deserializer.h
  * Author: hamed
  *
@@ -14,12 +14,12 @@
 /**
  * Style of serialized file:
  * ASTNodeType#Pointer#ObjectDATA
- * 
+ *
  * @param file
  */
 class Deserializer {
 public:
-	Deserializer(const char* file);
+	Deserializer(const char *file);
 	CSolver *deserialize();
 	virtual ~Deserializer();
 private:
@@ -44,5 +44,5 @@ private:
 	CloneMap map;
 };
 
-#endif /* DESERIALIZER_H */
+#endif/* DESERIALIZER_H */
 
diff --git a/src/Serialize/serializer.cc b/src/Serialize/serializer.cc
index b49b98b..810ece8 100644
--- a/src/Serialize/serializer.cc
+++ b/src/Serialize/serializer.cc
@@ -1,8 +1,8 @@
 
-/* 
+/*
  * File:   serializer.cc
  * Author: hamed
- * 
+ *
  * Created on September 7, 2017, 3:38 PM
  */
 
@@ -13,29 +13,29 @@
 
 Serializer::Serializer(const char *file) {
 	filedesc = open(file, O_WRONLY | O_CREAT | O_TRUNC, 0666);
- 
+
 	if (filedesc < 0) {
 		exit(-1);
 	}
 }
 
 Serializer::~Serializer() {
-	if (-1 == close(filedesc)){
+	if (-1 == close(filedesc)) {
 		exit(-1);
 	}
 }
 
-void Serializer::mywrite(const void *__buf, size_t __n){
+void Serializer::mywrite(const void *__buf, size_t __n) {
 	write (filedesc, __buf, __n);
 }
 
 
-void serializeBooleanEdge(Serializer* serializer, BooleanEdge be){
-	if(be == BooleanEdge(NULL))
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be) {
+	if (be == BooleanEdge(NULL))
 		return;
 	be.getBoolean()->serialize(serializer);
 	ASTNodeType type = BOOLEANEDGE;
 	serializer->mywrite(&type, sizeof(ASTNodeType));
-	Boolean* boolean = be.getRaw();
-	serializer->mywrite(&boolean, sizeof(Boolean*));
+	Boolean *boolean = be.getRaw();
+	serializer->mywrite(&boolean, sizeof(Boolean *));
 }
\ No newline at end of file
diff --git a/src/Serialize/serializer.h b/src/Serialize/serializer.h
index e6d2b50..f147773 100644
--- a/src/Serialize/serializer.h
+++ b/src/Serialize/serializer.h
@@ -1,5 +1,5 @@
 
-/* 
+/*
  * File:   serializer.h
  * Author: hamed
  *
@@ -26,14 +26,14 @@ private:
 	CloneMap map;
 };
 
-inline bool Serializer::isSerialized(void* obj){
+inline bool Serializer::isSerialized(void *obj) {
 	return map.contains(obj);
 }
 
 
 
 
-void serializeBooleanEdge(Serializer* serializer, BooleanEdge be);
+void serializeBooleanEdge(Serializer *serializer, BooleanEdge be);
 
-#endif /* SERIALIZER_H */
+#endif/* SERIALIZER_H */
 
diff --git a/src/Test/bug1.cc b/src/Test/bug1.cc
index 52707c5..208d9a9 100644
--- a/src/Test/bug1.cc
+++ b/src/Test/bug1.cc
@@ -13,8 +13,8 @@
  * 8=>9
  * 9=>2
  * 6=>2
- * 
- * 
+ *
+ *
  */
 int main(int numargs, char **argv) {
 	CSolver *solver = new CSolver();
@@ -22,110 +22,110 @@ int main(int numargs, char **argv) {
 	Set *s = solver->createSet(0, set1, 10);
 	Order *order = solver->createOrder(SATC_TOTAL, s);
 	BooleanEdge b01 =  solver->orderConstraint(order, 0, 1);
-        solver->addConstraint(b01);
+	solver->addConstraint(b01);
 	BooleanEdge b12 =  solver->orderConstraint(order, 1, 2);
-        solver->addConstraint(b12);
+	solver->addConstraint(b12);
 	BooleanEdge b23 =  solver->orderConstraint(order, 2, 3);
-        solver->addConstraint(b23);
+	solver->addConstraint(b23);
 	BooleanEdge b14 =  solver->orderConstraint(order, 1, 4);
-        solver->addConstraint(b14);
+	solver->addConstraint(b14);
 	BooleanEdge b45 =  solver->orderConstraint(order, 4, 5);
-        solver->addConstraint(b45);
+	solver->addConstraint(b45);
 	BooleanEdge b56 =  solver->orderConstraint(order, 5, 6);
-        solver->addConstraint(b56);
+	solver->addConstraint(b56);
 	BooleanEdge b17 =  solver->orderConstraint(order, 1, 7);
-        solver->addConstraint(b17);
+	solver->addConstraint(b17);
 	BooleanEdge b78 =  solver->orderConstraint(order, 7, 8);
-        solver->addConstraint(b78);
+	solver->addConstraint(b78);
 	BooleanEdge b89 =  solver->orderConstraint(order, 8, 9);
-        solver->addConstraint(b89);
+	solver->addConstraint(b89);
 	BooleanEdge b92 =  solver->orderConstraint(order, 9, 2);
-        solver->addConstraint(b92);
+	solver->addConstraint(b92);
 	BooleanEdge b62 =  solver->orderConstraint(order, 6, 2);
-        solver->addConstraint(b62);
+	solver->addConstraint(b62);
 
-        BooleanEdge v1 = solver->getBooleanVar(0);
-        solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v1));
-        BooleanEdge v2 = solver->getBooleanVar(0);
-        solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v2));
-        BooleanEdge v3 = solver->getBooleanVar(0);
-        BooleanEdge v4 = solver->getBooleanVar(0);
-        BooleanEdge v5 = solver->getBooleanVar(0);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_IFF, v3, v4),
-                v5));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v5));
-        BooleanEdge v6 = solver->getBooleanVar(0);
-        BooleanEdge v7 = solver->getBooleanVar(0);
-        BooleanEdge v8 = solver->getBooleanVar(0);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_IFF, v7, v8),
-                v6));
+	BooleanEdge v1 = solver->getBooleanVar(0);
+	solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v1));
+	BooleanEdge v2 = solver->getBooleanVar(0);
+	solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v2));
+	BooleanEdge v3 = solver->getBooleanVar(0);
+	BooleanEdge v4 = solver->getBooleanVar(0);
+	BooleanEdge v5 = solver->getBooleanVar(0);
+	solver->addConstraint(
+		solver->applyLogicalOperation(SATC_OR,
+																	solver->applyLogicalOperation(SATC_IFF, v3, v4),
+																	v5));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v5));
+	BooleanEdge v6 = solver->getBooleanVar(0);
+	BooleanEdge v7 = solver->getBooleanVar(0);
+	BooleanEdge v8 = solver->getBooleanVar(0);
+	solver->addConstraint(
+		solver->applyLogicalOperation(SATC_OR,
+																	solver->applyLogicalOperation(SATC_IFF, v7, v8),
+																	v6));
 	solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v6));
-        BooleanEdge v9 = solver->getBooleanVar(0);
+	BooleanEdge v9 = solver->getBooleanVar(0);
 	solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v9, v3));
-        BooleanEdge v10 = solver->getBooleanVar(0);
-        BooleanEdge v11 = solver->getBooleanVar(0);
-        BooleanEdge v12 = solver->getBooleanVar(0);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_OR, v10, v11),
-                solver->applyLogicalOperation(SATC_IFF, v1, v12)));
-        BooleanEdge b48 =  solver->orderConstraint(order, 4, 8);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_OR, v10, v11),
-                b48));
-        BooleanEdge v13 = solver->getBooleanVar(0);
-        BooleanEdge v14 = solver->getBooleanVar(0);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_IMPLIES, v10, v11),
-                solver->applyLogicalOperation(SATC_AND,
-                        solver->applyLogicalOperation(SATC_IFF, v12, v13),
-                        solver->applyLogicalOperation(SATC_NOT,b48))
-        ));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v11));
-        solver->addConstraint(v14);
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v8, v12));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v12, v8));
-        BooleanEdge v15 = solver->getBooleanVar(0);
-        BooleanEdge v16 = solver->getBooleanVar(0);
-        BooleanEdge v17 = solver->getBooleanVar(0);
-        BooleanEdge v18 = solver->getBooleanVar(0);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_OR, 
-                solver->applyLogicalOperation(SATC_OR, v15, v16),
-                solver->applyLogicalOperation(SATC_IFF, v17, v2)
-        ));
-        BooleanEdge b57 =  solver->orderConstraint(order, 5, 7);
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_IMPLIES, 
-                b57,
-                solver->applyLogicalOperation(SATC_OR, v15, v16)
-        ));
-        solver->addConstraint(
-                solver->applyLogicalOperation(SATC_IMPLIES, 
-                solver->applyLogicalOperation(SATC_AND, v15, solver->applyLogicalOperation(SATC_NOT,v16)),
-                solver->applyLogicalOperation(SATC_AND, b57, solver->applyLogicalOperation(SATC_IFF, v17, v14))
-        ));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v16));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v13, v17));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v13));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v4, v17));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v4));
-        solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v18, v9));
-        solver->addConstraint(v18);
-        
-        if (solver->solve() == 1){
+	BooleanEdge v10 = solver->getBooleanVar(0);
+	BooleanEdge v11 = solver->getBooleanVar(0);
+	BooleanEdge v12 = solver->getBooleanVar(0);
+	solver->addConstraint(
+		solver->applyLogicalOperation(SATC_OR,
+																	solver->applyLogicalOperation(SATC_OR, v10, v11),
+																	solver->applyLogicalOperation(SATC_IFF, v1, v12)));
+	BooleanEdge b48 =  solver->orderConstraint(order, 4, 8);
+	solver->addConstraint(
+		solver->applyLogicalOperation(SATC_OR,
+																	solver->applyLogicalOperation(SATC_OR, v10, v11),
+																	b48));
+	BooleanEdge v13 = solver->getBooleanVar(0);
+	BooleanEdge v14 = solver->getBooleanVar(0);
+	solver->addConstraint(
+		solver->applyLogicalOperation(SATC_OR,
+																	solver->applyLogicalOperation(SATC_IMPLIES, v10, v11),
+																	solver->applyLogicalOperation(SATC_AND,
+																																solver->applyLogicalOperation(SATC_IFF, v12, v13),
+																																solver->applyLogicalOperation(SATC_NOT,b48))
+																	));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v11));
+	solver->addConstraint(v14);
+	solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v8, v12));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v12, v8));
+	BooleanEdge v15 = solver->getBooleanVar(0);
+	BooleanEdge v16 = solver->getBooleanVar(0);
+	BooleanEdge v17 = solver->getBooleanVar(0);
+	BooleanEdge v18 = solver->getBooleanVar(0);
+	solver->addConstraint(
+		solver->applyLogicalOperation(SATC_OR,
+																	solver->applyLogicalOperation(SATC_OR, v15, v16),
+																	solver->applyLogicalOperation(SATC_IFF, v17, v2)
+																	));
+	BooleanEdge b57 =  solver->orderConstraint(order, 5, 7);
+	solver->addConstraint(
+		solver->applyLogicalOperation(SATC_IMPLIES,
+																	b57,
+																	solver->applyLogicalOperation(SATC_OR, v15, v16)
+																	));
+	solver->addConstraint(
+		solver->applyLogicalOperation(SATC_IMPLIES,
+																	solver->applyLogicalOperation(SATC_AND, v15, solver->applyLogicalOperation(SATC_NOT,v16)),
+																	solver->applyLogicalOperation(SATC_AND, b57, solver->applyLogicalOperation(SATC_IFF, v17, v14))
+																	));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v16));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v13, v17));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v13));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v4, v17));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v17, v4));
+	solver->addConstraint(solver->applyLogicalOperation(SATC_IMPLIES, v18, v9));
+	solver->addConstraint(v18);
+
+	if (solver->solve() == 1) {
 		printf("SAT\n");
-		printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
-			solver->getOrderConstraintValue(order, 5, 1), 
-			solver->getOrderConstraintValue(order, 1, 4),
-			solver->getOrderConstraintValue(order, 5, 4),
-			solver->getOrderConstraintValue(order, 1, 5));
+		printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
+					 solver->getOrderConstraintValue(order, 5, 1),
+					 solver->getOrderConstraintValue(order, 1, 4),
+					 solver->getOrderConstraintValue(order, 5, 4),
+					 solver->getOrderConstraintValue(order, 1, 5));
 	} else {
 		printf("UNSAT\n");
 	}
diff --git a/src/Test/bug_minimal.cc b/src/Test/bug_minimal.cc
index 8780b27..1d1124c 100644
--- a/src/Test/bug_minimal.cc
+++ b/src/Test/bug_minimal.cc
@@ -13,8 +13,8 @@
  * 8=>9
  * 9=>2
  * 6=>2
- * 
- * 
+ *
+ *
  */
 int main(int numargs, char **argv) {
 	CSolver *solver = new CSolver();
@@ -53,11 +53,11 @@ int main(int numargs, char **argv) {
 	BooleanEdge b57 =  solver->orderConstraint(order, 5, 7);
 	solver->addConstraint(b57);
 
-	
-	if (solver->solve() == 1){
+
+	if (solver->solve() == 1) {
 		printf("SAT\n");
-		printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
-					 solver->getOrderConstraintValue(order, 5, 1), 
+		printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
+					 solver->getOrderConstraintValue(order, 5, 1),
 					 solver->getOrderConstraintValue(order, 1, 4),
 					 solver->getOrderConstraintValue(order, 5, 4),
 					 solver->getOrderConstraintValue(order, 1, 5));
diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
index e2c46e0..148235a 100644
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -17,13 +17,13 @@ int main(int numargs, char **argv) {
 	solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b1, solver->applyLogicalOperation(SATC_NOT, b2)));
 	solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b2, solver->applyLogicalOperation(SATC_NOT, b1)));
 	solver->serialize();
-	if (solver->solve() == 1){
+	if (solver->solve() == 1) {
 		printf("SAT\n");
-		printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", 
-			solver->getOrderConstraintValue(order, 5, 1), 
-			solver->getOrderConstraintValue(order, 1, 4),
-			solver->getOrderConstraintValue(order, 5, 4),
-			solver->getOrderConstraintValue(order, 1, 5));
+		printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n",
+					 solver->getOrderConstraintValue(order, 5, 1),
+					 solver->getOrderConstraintValue(order, 1, 4),
+					 solver->getOrderConstraintValue(order, 5, 4),
+					 solver->getOrderConstraintValue(order, 1, 5));
 	} else {
 		printf("UNSAT\n");
 	}
diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
index 8a177fa..64ebc34 100644
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -51,12 +51,12 @@ bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) {
 	}
 }
 
-bool DecomposeOrderResolver::resolvePartialOrder(OrderNode* first, OrderNode* second){
-	if(first->sccNum > second->sccNum){
+bool DecomposeOrderResolver::resolvePartialOrder(OrderNode *first, OrderNode *second) {
+	if (first->sccNum > second->sccNum) {
 		return false;
 	} else {
 		return graph->isTherePath(first, second);
 	}
-		
+
 }
 
diff --git a/src/Translator/decomposeorderresolver.h b/src/Translator/decomposeorderresolver.h
index f1d06c6..1f3b266 100644
--- a/src/Translator/decomposeorderresolver.h
+++ b/src/Translator/decomposeorderresolver.h
@@ -17,7 +17,7 @@ class DecomposeOrderResolver : public OrderResolver {
 public:
 	DecomposeOrderResolver(OrderGraph *graph, Vector<Order *> &orders);
 	bool resolveOrder(uint64_t first, uint64_t second);
-	bool resolvePartialOrder(OrderNode* first, OrderNode* second);
+	bool resolvePartialOrder(OrderNode *first, OrderNode *second);
 	virtual ~DecomposeOrderResolver();
 private:
 	OrderGraph *graph;
diff --git a/src/Translator/orderpairresolver.cc b/src/Translator/orderpairresolver.cc
index e32a757..6044e06 100644
--- a/src/Translator/orderpairresolver.cc
+++ b/src/Translator/orderpairresolver.cc
@@ -38,7 +38,7 @@ bool OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) {
 		ASSERT(to != NULL);
 
 		OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
-		
+
 		if (edge != NULL && edge->mustPos) {
 			return true;
 		} else if ( edge != NULL && edge->mustNeg) {
diff --git a/src/Translator/orderpairresolver.h b/src/Translator/orderpairresolver.h
index dde7378..79212ae 100644
--- a/src/Translator/orderpairresolver.h
+++ b/src/Translator/orderpairresolver.h
@@ -15,13 +15,13 @@ class OrderPairResolver : public OrderResolver {
 public:
 	OrderPairResolver(CSolver *_solver, Order *_order);
 	bool resolveOrder(uint64_t first, uint64_t second);
-	HashtableOrderPair* getOrderPairTable() { return orderPairTable;}
+	HashtableOrderPair *getOrderPairTable() { return orderPairTable;}
 	virtual ~OrderPairResolver();
 private:
 	CSolver *solver;
 	Order *order;
 	HashtableOrderPair *orderPairTable;
-	
+
 	bool getOrderConstraintValue(uint64_t first, uint64_t second);
 };
 
diff --git a/src/Tuner/searchtuner.cc b/src/Tuner/searchtuner.cc
index 3e95860..c119597 100644
--- a/src/Tuner/searchtuner.cc
+++ b/src/Tuner/searchtuner.cc
@@ -54,9 +54,9 @@ unsigned int tunableSettingHash(TunableSetting *setting) {
 
 bool tunableSettingEquals(TunableSetting *setting1, TunableSetting *setting2) {
 	return setting1->hasVar == setting2->hasVar &&
-		setting1->type1 == setting2->type1 &&
-		setting1->type2 == setting2->type2 &&
-		setting1->param == setting2->param;
+				 setting1->type1 == setting2->type1 &&
+				 setting1->type2 == setting2->type2 &&
+				 setting1->param == setting2->param;
 }
 
 SearchTuner::SearchTuner() {
@@ -110,7 +110,7 @@ int SearchTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam
 		result = settings.get(&setting);
 		if ( result == NULL) {
 			result = new
-				TunableSetting(vartype1, vartype2, param);
+							 TunableSetting(vartype1, vartype2, param);
 			uint value = descriptor->lowValue + (random() % (1 + descriptor->highValue - descriptor->lowValue));
 			result->setDecision(descriptor->lowValue, descriptor->highValue, descriptor->defaultValue, value);
 			settings.add(result);
diff --git a/src/common.h b/src/common.h
index a15f7df..52c0b5f 100644
--- a/src/common.h
+++ b/src/common.h
@@ -19,17 +19,17 @@
 #include "time.h"
 
 /*
-	extern int model_out;
-	extern int model_err;
-	extern int switch_alloc;
-	
-	#define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
-	#define model_print(fmt, ...) do { printf(fmt, ## __VA_ARGS__); } while (0)
-	#define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
- 
-	#define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
- 
-	#define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
+   extern int model_out;
+   extern int model_err;
+   extern int switch_alloc;
+
+ #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
+ #define model_print(fmt, ...) do { printf(fmt, ## __VA_ARGS__); } while (0)
+ #define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
+
+ #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
+
+ #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
  */
 
 #define model_print printf
diff --git a/src/csolver.cc b/src/csolver.cc
index 592d1d5..0988a57 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -103,7 +103,7 @@ void CSolver::serialize() {
 		Deserializer deserializer("dump");
 		deserializer.deserialize();
 	}
-	
+
 }
 
 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
@@ -118,7 +118,7 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
 	return set;
 }
 
-VarType CSolver::getSetVarType(Set *set){
+VarType CSolver::getSetVarType(Set *set) {
 	return set->getType();
 }
 
@@ -143,7 +143,7 @@ uint64_t CSolver::createUniqueItem(MutableSet *set) {
 	return element;
 }
 
-void CSolver::finalizeMutableSet(MutableSet* set){
+void CSolver::finalizeMutableSet(MutableSet *set) {
 	set->finalize();
 }
 
@@ -153,7 +153,7 @@ Element *CSolver::getElementVar(Set *set) {
 	return element;
 }
 
-Set* CSolver::getElementRange (Element* element){
+Set *CSolver::getElementRange (Element *element) {
 	return element->getRange();
 }
 
@@ -260,11 +260,11 @@ BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs,
 }
 
 bool CSolver::isTrue(BooleanEdge b) {
-        return b.isNegated()?b->isFalse():b->isTrue();
+	return b.isNegated() ? b->isFalse() : b->isTrue();
 }
 
 bool CSolver::isFalse(BooleanEdge b) {
-        return b.isNegated()?b->isTrue():b->isFalse();
+	return b.isNegated() ? b->isTrue() : b->isFalse();
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
@@ -279,7 +279,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
 
 static int ptrcompares(const void *p1, const void *p2) {
 	uintptr_t b1 = *(uintptr_t const *) p1;
-  uintptr_t b2 = *(uintptr_t const *) p2;
+	uintptr_t b2 = *(uintptr_t const *) p2;
 	if (b1 < b2)
 		return -1;
 	else if (b1 == b2)
@@ -288,11 +288,11 @@ static int ptrcompares(const void *p1, const void *p2) {
 		return 1;
 }
 
-BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge * array, uint asize) {
+BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
 	BooleanEdge newarray[asize];
 	memcpy(newarray, array, asize * sizeof(BooleanEdge));
-	for(uint i=0; i < asize; i++) {
-		BooleanEdge b=newarray[i];
+	for (uint i = 0; i < asize; i++) {
+		BooleanEdge b = newarray[i];
 		if (b->type == LOGICOP) {
 			if (((BooleanLogic *) b.getBoolean())->replaced) {
 				newarray[i] = doRewrite(newarray[i]);
@@ -312,14 +312,14 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 	case SATC_IFF: {
 		for (uint i = 0; i < 2; i++) {
 			if (array[i]->type == BOOLCONST) {
-				if (isTrue(array[i])) { // It can be undefined
+				if (isTrue(array[i])) {	// It can be undefined
 					return array[1 - i];
-				} else if(isFalse(array[i])) {
+				} else if (isFalse(array[i])) {
 					newarray[0] = array[1 - i];
 					return applyLogicalOperation(SATC_NOT, newarray, 1);
 				}
 			} else if (array[i]->type == LOGICOP) {
-				BooleanLogic *b =(BooleanLogic *)array[i].getBoolean();
+				BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
 				if (b->replaced) {
 					return rewriteLogicalOperation(op, array, asize);
 				}
@@ -328,7 +328,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 		break;
 	}
 	case SATC_OR: {
-		for (uint i =0; i <asize; i++) {
+		for (uint i = 0; i < asize; i++) {
 			newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
 		}
 		return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
@@ -344,9 +344,9 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 			if (b->type == BOOLCONST) {
 				if (isTrue(b))
 					continue;
-				else{
+				else {
 					return boolFalse;
-                                }
+				}
 			} else
 				newarray[newindex++] = b;
 		}
@@ -393,21 +393,21 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-	if(constraint.isNegated())
+	if (constraint.isNegated())
 		model_print("!");
 	constraint.getBoolean()->print();
 	if (isTrue(constraint))
 		return;
 	else if (isFalse(constraint)) {
-		int t=0;
+		int t = 0;
 		setUnSAT();
 	}
 	else {
 		if (constraint->type == LOGICOP) {
-			BooleanLogic *b=(BooleanLogic *) constraint.getBoolean();
+			BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
 			if (!constraint.isNegated()) {
-				if (b->op==SATC_AND) {
-					for(uint i=0;i<b->inputs.getSize();i++) {
+				if (b->op == SATC_AND) {
+					for (uint i = 0; i < b->inputs.getSize(); i++) {
 						addConstraint(b->inputs.get(i));
 					}
 					return;
@@ -419,12 +419,12 @@ void CSolver::addConstraint(BooleanEdge constraint) {
 			}
 		}
 		constraints.add(constraint);
-		Boolean *ptr=constraint.getBoolean();
-		
+		Boolean *ptr = constraint.getBoolean();
+
 		if (ptr->boolVal == BV_UNSAT) {
 			setUnSAT();
 		}
-		
+
 		replaceBooleanWithTrueNoRemove(constraint);
 		constraint->parents.clear();
 	}
@@ -449,7 +449,7 @@ int CSolver::solve() {
 
 	Preprocess pp(this);
 	pp.doTransform();
-	
+
 	DecomposeOrderTransform dot(this);
 	dot.doTransform();
 
@@ -459,12 +459,12 @@ int CSolver::solve() {
 	EncodingGraph eg(this);
 	eg.buildGraph();
 	eg.encode();
-	
+
 	naiveEncodingDecision(this);
 	satEncoder->encodeAllSATEncoder(this);
-        model_print("Is problem UNSAT after encoding: %d\n", unsat);
+	model_print("Is problem UNSAT after encoding: %d\n", unsat);
 	int result = unsat ? IS_UNSAT : satEncoder->solve();
-        model_print("Result Computed in CSolver: %d\n", result);
+	model_print("Result Computed in CSolver: %d\n", result);
 	long long finishTime = getTimeNano();
 	elapsedTime = finishTime - startTime;
 	if (deleteTuner) {
@@ -487,7 +487,7 @@ uint64_t CSolver::getElementValue(Element *element) {
 }
 
 bool CSolver::getBooleanValue(BooleanEdge bedge) {
-	Boolean *boolean=bedge.getBoolean();
+	Boolean *boolean = bedge.getBoolean();
 	switch (boolean->type) {
 	case BOOLEANVAR:
 		return getBooleanVariableValueSATTranslator(this, boolean);
diff --git a/src/csolver.h b/src/csolver.h
index 41c4627..71ee874 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -20,7 +20,7 @@ public:
 	Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
 
 	VarType getSetVarType(Set *set);
-	
+
 	Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
 
 	/** This function creates a mutable set. */
@@ -37,11 +37,11 @@ public:
 	    items to the set. */
 
 	uint64_t createUniqueItem(MutableSet *set);
-	
+
 	/**
 	 * Freeze and finalize the mutableSet ...
 	 */
-	void finalizeMutableSet(MutableSet* set);
+	void finalizeMutableSet(MutableSet *set);
 
 	/** This function creates an element variable over a set. */
 
@@ -49,8 +49,8 @@ public:
 
 	/** This function creates an element constrant. */
 	Element *getElementConst(VarType type, uint64_t value);
-	
-	Set* getElementRange (Element* element);
+
+	Set *getElementRange (Element *element);
 
 	BooleanEdge getBooleanTrue();
 
@@ -136,11 +136,11 @@ public:
 	bool isUnSAT() { return unsat; }
 
 	Vector<Order *> *getOrders() { return &allOrders;}
-	HashsetOrder * getActiveOrders() { return &activeOrders;}
+	HashsetOrder *getActiveOrders() { return &activeOrders;}
 
 	Tuner *getTuner() { return tuner; }
 
-	SetIteratorBooleanEdge * getConstraints() { return constraints.iterator(); }
+	SetIteratorBooleanEdge *getConstraints() { return constraints.iterator(); }
 
 	SATEncoder *getSATEncoder() {return satEncoder;}
 
@@ -189,7 +189,7 @@ private:
 	Vector<Order *> allOrders;
 
 	HashsetOrder activeOrders;
-	
+
 	/** This is a vector of all function structs that we have allocated. */
 	Vector<Function *> allFunctions;
 
diff --git a/src/mymemory.h b/src/mymemory.h
index 7c63aa1..9708936 100644
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -24,13 +24,13 @@
    void ourfree(void *ptr);
    void * ourcalloc(size_t count, size_t size);
    void * ourrealloc(void *ptr, size_t size);
-*/
+ */
 
 #if 0
-void * model_malloc(size_t size);
+void *model_malloc(size_t size);
 void model_free(void *ptr);
-void * model_calloc(size_t count, size_t size);
-void * model_realloc(void *ptr, size_t size);
+void *model_calloc(size_t count, size_t size);
+void *model_realloc(void *ptr, size_t size);
 
 
 #define ourmalloc model_malloc