From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 21 Mar 2019 20:58:54 +0000 (-0700)
Subject: commit after merge
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=e5c1ee81132998d6a80d83e95f1faf2ca06ac7fb;hp=24940f1c2b64462da246d0ed237f0825dd04e6ca;p=satune.git

commit after merge
---

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index e63549e..04898aa 100644
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -33,7 +33,7 @@ BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) :
 }
 
 void BooleanOrder::updateParents() {
-	order->constraints.push(this);
+	order->addOrderConstraint(this);
 }
 
 BooleanPredicate::BooleanPredicate(Predicate *_predicate, Element **_inputs, uint _numInputs, BooleanEdge _undefinedStatus) :
diff --git a/src/AST/order.h b/src/AST/order.h
index 866b1ab..cbbe846 100644
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -20,6 +20,7 @@ public:
 	void print();
 	Vector<BooleanOrder *> constraints;
 	OrderEncoding encoding;
+
 	void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};
 	void initializeOrderElementsHashtable();
 	void addOrderConstraint(BooleanOrder *constraint);
diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index fef4dcb..a53180e 100644
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -23,7 +23,7 @@ void CSolver::replaceBooleanWithFalseNoRemove(BooleanEdge bexpr) {
 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
 	updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
 
-	ASSERT((bexpr->boolVal != BV_UNSAT ) || unsat);
+	ASSERT((bexpr->boolVal != BV_UNSAT) || unsat);
 
 	uint size = bexpr->parents.getSize();
 	for (uint i = 0; i < size; i++) {
diff --git a/src/ASTAnalyses/Polarity/polarityassignment.cc b/src/ASTAnalyses/Polarity/polarityassignment.cc
index b8b01d0..8a94f0a 100644
--- a/src/ASTAnalyses/Polarity/polarityassignment.cc
+++ b/src/ASTAnalyses/Polarity/polarityassignment.cc
@@ -2,7 +2,7 @@
 #include "csolver.h"
 
 void computePolarities(CSolver *This) {
-	if(This->isUnSAT()){
+	if (This->isUnSAT()) {
 		return;
 	}
 	SetIteratorBooleanEdge *iterator = This->getConstraints();
diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 4b3fc4a..e63cb74 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -28,7 +28,7 @@ DecomposeOrderTransform::~DecomposeOrderTransform() {
 }
 
 void DecomposeOrderTransform::doTransform() {
-	if(solver->isUnSAT())
+	if (solver->isUnSAT())
 		return;
 	HashsetOrder *orders = solver->getActiveOrders()->copy();
 	SetIteratorOrder *orderit = orders->iterator();
@@ -331,11 +331,11 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
 		BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
 		updateEdgePolarity(benew, be);
 		if (solver->isTrue(benew))
-		  solver->replaceBooleanWithTrue(be);
+			solver->replaceBooleanWithTrue(be);
 		else if (solver->isFalse(benew))
-		  solver->replaceBooleanWithFalse(be);
+			solver->replaceBooleanWithFalse(be);
 		else
-		  solver->replaceBooleanWithBoolean(be, benew);
+			solver->replaceBooleanWithBoolean(be, benew);
 	}
 	dstnode->inEdges.reset();
 	delete inedgeit;
@@ -366,11 +366,11 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
 		BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
 		updateEdgePolarity(benew, be);
 		if (solver->isTrue(benew))
-		  solver->replaceBooleanWithTrue(be);
+			solver->replaceBooleanWithTrue(be);
 		else if (solver->isFalse(benew))
-		  solver->replaceBooleanWithFalse(be);
+			solver->replaceBooleanWithFalse(be);
 		else
-		  solver->replaceBooleanWithBoolean(be, benew);
+			solver->replaceBooleanWithBoolean(be, benew);
 	}
 	dstnode->outEdges.reset();
 	delete outedgeit;
diff --git a/src/ASTTransform/elementopt.cc b/src/ASTTransform/elementopt.cc
index 899f659..22a6dbe 100644
--- a/src/ASTTransform/elementopt.cc
+++ b/src/ASTTransform/elementopt.cc
@@ -9,7 +9,7 @@
 
 ElementOpt::ElementOpt(CSolver *_solver)
 	: Transform(_solver),
-	  updateSets(false)
+	updateSets(false)
 {
 }
 
@@ -22,7 +22,7 @@ void ElementOpt::doTransform() {
 
 	//Set once we know we are going to use it.
 	updateSets = solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1;
-	
+
 	SetIteratorBooleanEdge *iterator = solver->getConstraints();
 	while (iterator->hasNext()) {
 		BooleanEdge constraint = iterator->next();
diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index 2a7b901..d5d769d 100644
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -17,7 +17,7 @@ IntegerEncodingTransform::~IntegerEncodingTransform() {
 }
 
 void IntegerEncodingTransform::doTransform() {
-	if(solver->isUnSAT()){
+	if (solver->isUnSAT()) {
 		return;
 	}
 	HashsetOrder *orders = solver->getActiveOrders()->copy();
diff --git a/src/ASTTransform/varorderingopt.cc b/src/ASTTransform/varorderingopt.cc
index 9fd8c60..c78252c 100644
--- a/src/ASTTransform/varorderingopt.cc
+++ b/src/ASTTransform/varorderingopt.cc
@@ -26,7 +26,7 @@ VarOrderingOpt::~VarOrderingOpt() {
 }
 
 void VarOrderingOpt::doTransform() {
-	if(solver->isUnSAT()){
+	if (solver->isUnSAT()) {
 		return;
 	}
 	BooleanVarOrdering direction = (BooleanVarOrdering)solver->getTuner()->getTunable(VARIABLEORDER, &boolVarOrderingDesc);
diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index 618b8c1..00219ef 100644
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -35,7 +35,7 @@ int SATEncoder::solve(long timeout) {
 }
 
 void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
-	if(csolver->isUnSAT()){
+	if (csolver->isUnSAT()) {
 		return;
 	}
 	SetIteratorBooleanEdge *iterator = csolver->getConstraints();
diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index 6c53253..2dd5e69 100644
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -9,9 +9,9 @@
 		type *array;                                                       \
 	};                                                                    \
 	typedef struct Vector ## name Vector ## name;                         \
-	Vector ## name * allocVector ## name(uint capacity);                  \
-	Vector ## name * allocDefVector ## name();                            \
-	Vector ## name * allocVectorArray ## name(uint capacity, type * array); \
+	Vector ## name *allocVector ## name(uint capacity);                  \
+	Vector ## name *allocDefVector ## name();                            \
+	Vector ## name *allocVectorArray ## name(uint capacity, type * array); \
 	void pushVector ## name(Vector ## name * vector, type item);           \
 	type lastVector ## name(Vector ## name * vector);                      \
 	void popVector ## name(Vector ## name * vector);                       \
@@ -29,18 +29,18 @@
 	void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array);
 
 #define VectorImpl(name, type, defcap)                                  \
-	Vector ## name * allocDefVector ## name() {                           \
+	Vector ## name *allocDefVector ## name() {                           \
 		return allocVector ## name(defcap);                                 \
 	}                                                                     \
-	Vector ## name * allocVector ## name(uint capacity) {                 \
-		Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name));  \
+	Vector ## name *allocVector ## name(uint capacity) {                 \
+		Vector ## name *tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name));  \
 		tmp->size = 0;                                                      \
 		tmp->capacity = capacity;                                           \
 		tmp->array = (type *) ourmalloc(sizeof(type) * capacity);           \
 		return tmp;                                                         \
 	}                                                                     \
-	Vector ## name * allocVectorArray ## name(uint capacity, type * array)  { \
-		Vector ## name * tmp = allocVector ## name(capacity);               \
+	Vector ## name *allocVectorArray ## name(uint capacity, type * array)  { \
+		Vector ## name *tmp = allocVector ## name(capacity);               \
 		tmp->size = capacity;                                                 \
 		memcpy(tmp->array, array, capacity * sizeof(type));                 \
 		return tmp;                                                         \
diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index ac20be5..e3d1305 100644
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -15,7 +15,7 @@
 #include <strings.h>
 
 void naiveEncodingDecision(CSolver *This) {
-	if(This->isUnSAT()){
+	if (This->isUnSAT()) {
 		return;
 	}
 	SetIteratorBooleanEdge *iterator = This->getConstraints();
diff --git a/src/Interpreter/alloyinterpreter.cc b/src/Interpreter/alloyinterpreter.cc
index 021b087..d802529 100644
--- a/src/Interpreter/alloyinterpreter.cc
+++ b/src/Interpreter/alloyinterpreter.cc
@@ -19,37 +19,37 @@ using namespace std;
 #define ALLOYFILENAME "satune.als"
 #define ALLOYSOLUTIONFILE "solution.sol"
 
-AlloyInterpreter::AlloyInterpreter(CSolver *_solver): 
-	Interpreter(_solver) 
+AlloyInterpreter::AlloyInterpreter(CSolver *_solver) :
+	Interpreter(_solver)
 {
 	output.open(ALLOYFILENAME);
-	if(!output.is_open()){
+	if (!output.is_open()) {
 		model_print("AlloyEnc:Error in opening the dump file satune.als\n");
 		exit(-1);
 	}
 }
 
-AlloyInterpreter::~AlloyInterpreter(){
-	if(output.is_open()){
+AlloyInterpreter::~AlloyInterpreter() {
+	if (output.is_open()) {
 		output.close();
 	}
 }
 
-ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id){
+ValuedSignature *AlloyInterpreter::getBooleanSignature(uint id) {
 	return new AlloyBoolSig(id);
 }
 
-ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig){
+ValuedSignature *AlloyInterpreter::getElementSignature(uint id, Signature *ssig) {
 	return new AlloyElementSig(id, ssig);
 }
 
-Signature *AlloyInterpreter::getSetSignature(uint id, Set *set){
+Signature *AlloyInterpreter::getSetSignature(uint id, Set *set) {
 	return new AlloySetSig(id, set);
 }
 
-void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
+void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts) {
 	output << "fact {" << endl;
-	for(uint i=0; i< facts.getSize(); i++){
+	for (uint i = 0; i < facts.getSize(); i++) {
 		char *cstr = facts.get(i);
 		writeToFile(cstr);
 	}
@@ -57,24 +57,24 @@ void AlloyInterpreter::dumpAllConstraints(Vector<char *> &facts){
 }
 
 
-int AlloyInterpreter::getResult(){
+int AlloyInterpreter::getResult() {
 	ifstream input(ALLOYSOLUTIONFILE, ios::in);
 	string line;
-	while(getline(input, line)){
-		if(line.find("Unsatisfiable.")== 0){
+	while (getline(input, line)) {
+		if (line.find("Unsatisfiable.") == 0) {
 			return IS_UNSAT;
 		}
-		if(line.find("univ") == 0){
+		if (line.find("univ") == 0) {
 			continue;
 		}
-		if(line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0){
+		if (line.find("this/AbsBool<:value") == 0 || line.find("this/AbsElement<:value=") == 0) {
 			const char delim [2] = ",";
-			char cline [line.size()+1];
+			char cline [line.size() + 1];
 			strcpy ( cline, line.c_str() );
 			char *token = strtok(cline, delim);
-			while( token != NULL ) {
+			while ( token != NULL ) {
 				uint i1, i2, i3;
-				if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)){
+				if (3 == sscanf(token,"%*[^0123456789]%u%*[^0123456789]%d%*[^0123456789]%u", &i1, &i2, &i3)) {
 					model_print("Signature%u = %u\n", i1, i3);
 					sigEnc.setValue(i1, i3);
 				}
@@ -86,86 +86,86 @@ int AlloyInterpreter::getResult(){
 }
 
 
-int AlloyInterpreter::getAlloyIntScope(){
+int AlloyInterpreter::getAlloyIntScope() {
 	double mylog = log2(sigEnc.getMaxValue() + 1);
-	return floor(mylog) == mylog ? (int)mylog + 1: (int)mylog + 2;
+	return floor(mylog) == mylog ? (int)mylog + 1 : (int)mylog + 2;
 }
 
-void AlloyInterpreter::dumpFooter(){
+void AlloyInterpreter::dumpFooter() {
 	output << "pred show {}" << endl;
 	output << "run show for " << getAlloyIntScope() << " int" << endl;
 }
 
-void AlloyInterpreter::dumpHeader(){
+void AlloyInterpreter::dumpHeader() {
 	output << "open util/integer" << endl;
 }
 
-void AlloyInterpreter::compileRunCommand(char * command, size_t size){
+void AlloyInterpreter::compileRunCommand(char *command, size_t size) {
 	model_print("Calling Alloy...\n");
 	snprintf(command, size, "./run.sh timeout %u java -Xmx10000m edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz %s > %s", getTimeout(), ALLOYFILENAME, ALLOYSOLUTIONFILE);
 }
 
-string AlloyInterpreter::negateConstraint(string constr){
+string AlloyInterpreter::negateConstraint(string constr) {
 	return "not ( " + constr + " )";
 }
 
-string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl){
+string AlloyInterpreter::encodeBooleanLogic( BooleanLogic *bl) {
 	uint size = bl->inputs.getSize();
 	string array[size];
 	for (uint i = 0; i < size; i++)
 		array[i] = encodeConstraint(bl->inputs.get(i));
 	string op;
-	switch (bl->op){
-		case SATC_OR:
-			op = " or ";
-			break;
-		case SATC_AND:
-			op = " and ";
-			break;
-		case SATC_NOT:
-			op = " not ";
-			break;
-		case SATC_IFF:
-			op = " iff ";
-			break;
-		case SATC_IMPLIES:
-			op = " implies ";
-			break;
-		case SATC_XOR:
-		default:
-			ASSERT(0);
+	switch (bl->op) {
+	case SATC_OR:
+		op = " or ";
+		break;
+	case SATC_AND:
+		op = " and ";
+		break;
+	case SATC_NOT:
+		op = " not ";
+		break;
+	case SATC_IFF:
+		op = " iff ";
+		break;
+	case SATC_IMPLIES:
+		op = " implies ";
+		break;
+	case SATC_XOR:
+	default:
+		ASSERT(0);
 	}
 	switch (bl->op) {
-		case SATC_OR:
-		case SATC_AND:{
-			ASSERT(size >= 2);
-			string res = "( ";
-			res += array[0];
-			for( uint i=1; i< size; i++){
-				res += op + array[i];
-			}
-			res += " )";
-			return res;
-		}
-		case SATC_NOT:{
-			return "not ( " + array[0] + " )";
+	case SATC_OR:
+	case SATC_AND: {
+		ASSERT(size >= 2);
+		string res = "( ";
+		res += array[0];
+		for ( uint i = 1; i < size; i++) {
+			res += op + array[i];
 		}
-		case SATC_IMPLIES:
-		case SATC_IFF:
-			return "( " + array[0] + op + array[1] + " )";
-		case SATC_XOR:
-		default:
-			ASSERT(0);
+		res += " )";
+		return res;
+	}
+	case SATC_NOT: {
+		return "not ( " + array[0] + " )";
+	}
+	case SATC_IMPLIES:
+	case SATC_IFF:
+		return "( " + array[0] + op + array[1] + " )";
+	case SATC_XOR:
+	default:
+		ASSERT(0);
 
 	}
 }
 
-string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv){
-	ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
+string AlloyInterpreter::encodeBooleanVar( BooleanVar *bv) {
+	ValuedSignature *boolSig = sigEnc.getBooleanSignature(bv);
 	return *boolSig + " = 1";
 }
 
-string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
+string AlloyInterpreter::processElementFunction(ElementFunction *elemFunc, ValuedSignature *signature) {
 	FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
 	uint numDomains = elemFunc->inputs.getSize();
 	ASSERT(numDomains > 1);
@@ -174,39 +174,39 @@ string AlloyInterpreter::processElementFunction(ElementFunction* elemFunc, Value
 	for (uint i = 0; i < numDomains; i++) {
 		Element *elem = elemFunc->inputs.get(i);
 		inputs[i] = sigEnc.getElementSignature(elem);
-		if(elem->type == ELEMFUNCRETURN){
+		if (elem->type == ELEMFUNCRETURN) {
 			result += processElementFunction((ElementFunction *) elem, inputs[i]);
 		}
 	}
 	string op;
-	switch(function->op){
-		case SATC_ADD:
-			op = ".add";
-			break;
-		case SATC_SUB:
-			op = ".sub";
-			break;
-		default:
-			ASSERT(0);
+	switch (function->op) {
+	case SATC_ADD:
+		op = ".add";
+		break;
+	case SATC_SUB:
+		op = ".sub";
+		break;
+	default:
+		ASSERT(0);
 	}
 	result += *signature + " = " + *inputs[0];
 	for (uint i = 1; i < numDomains; i++) {
-		result += op + "["+ *inputs[i] +"]";
+		result += op + "[" + *inputs[i] + "]";
 	}
 	result += "\n";
 	return result;
 }
 
-string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
+string AlloyInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) {
 	switch (op) {
-		case SATC_EQUALS:
-			return *elemSig1 + " = " + *elemSig2;
-		case SATC_LT:
-			return *elemSig1 + " < " + *elemSig2;
-		case SATC_GT:
-			return *elemSig1 + " > " + *elemSig2;
-		default:
-			ASSERT(0);
+	case SATC_EQUALS:
+		return *elemSig1 + " = " + *elemSig2;
+	case SATC_LT:
+		return *elemSig1 + " < " + *elemSig2;
+	case SATC_GT:
+		return *elemSig1 + " > " + *elemSig2;
+	default:
+		ASSERT(0);
 	}
 }
 
diff --git a/src/Interpreter/alloyinterpreter.h b/src/Interpreter/alloyinterpreter.h
index e4a1e3b..310f3d9 100644
--- a/src/Interpreter/alloyinterpreter.h
+++ b/src/Interpreter/alloyinterpreter.h
@@ -7,7 +7,7 @@
 #include <iostream>
 #include <fstream>
 
-class AlloyInterpreter: public Interpreter{
+class AlloyInterpreter : public Interpreter {
 public:
 	AlloyInterpreter(CSolver *solver);
 	virtual ValuedSignature *getBooleanSignature(uint id);
@@ -18,7 +18,7 @@ protected:
 	virtual void dumpFooter();
 	virtual void dumpHeader();
 	int getAlloyIntScope();
-	virtual void compileRunCommand(char * command , size_t size);
+	virtual void compileRunCommand(char *command, size_t size);
 	virtual int getResult();
 	virtual void dumpAllConstraints(Vector<char *> &facts);
 	virtual string negateConstraint(string constr);
diff --git a/src/Interpreter/alloysig.cc b/src/Interpreter/alloysig.cc
index 1b98cd8..b7eeb86 100644
--- a/src/Interpreter/alloysig.cc
+++ b/src/Interpreter/alloysig.cc
@@ -5,18 +5,18 @@ bool AlloyBoolSig::encodeAbs = true;
 bool AlloySetSig::encodeAbs = true;
 bool AlloyElementSig::encodeAbs = true;
 
-AlloyBoolSig::AlloyBoolSig(uint id):
+AlloyBoolSig::AlloyBoolSig(uint id) :
 	ValuedSignature(id)
 {
 }
 
-string AlloyBoolSig::toString() const{
+string AlloyBoolSig::toString() const {
 	return "Boolean" + to_string(id) + ".value";
 }
 
-string AlloyBoolSig::getSignature() const{
+string AlloyBoolSig::getSignature() const {
 	string str;
-	if(encodeAbs){
+	if (encodeAbs) {
 		encodeAbs = false;
 		str += getAbsSignature();
 	}
@@ -24,15 +24,15 @@ string AlloyBoolSig::getSignature() const{
 	return str;
 }
 
-string AlloyBoolSig::getAbsSignature() const{
+string AlloyBoolSig::getAbsSignature() const {
 	string str;
-	if(AlloySetSig::encodeAbs){
+	if (AlloySetSig::encodeAbs) {
 		AlloySetSig::encodeAbs = false;
 		str += "abstract sig AbsSet {\
 		domain: set Int\
 		}\n";
 	}
-	str +="one sig BooleanSet extends AbsSet {}{\n\
+	str += "one sig BooleanSet extends AbsSet {}{\n\
 	domain = 0 + 1 \n\
 	}\n\
 	abstract sig AbsBool {\
@@ -43,19 +43,19 @@ string AlloyBoolSig::getAbsSignature() const{
 	return str;
 }
 
-AlloyElementSig::AlloyElementSig(uint id, Signature *_ssig): 
+AlloyElementSig::AlloyElementSig(uint id, Signature *_ssig) :
 	ValuedSignature(id),
 	ssig(_ssig)
 {
 }
 
-string AlloyElementSig::toString() const{
+string AlloyElementSig::toString() const {
 	return "Element" + to_string(id) + ".value";
 }
 
-string AlloyElementSig::getSignature() const{
+string AlloyElementSig::getSignature() const {
 	string str;
-	if(encodeAbs){
+	if (encodeAbs) {
 		encodeAbs = false;
 		str += getAbsSignature();
 	}
@@ -65,28 +65,28 @@ string AlloyElementSig::getSignature() const{
 	return str;
 }
 
-string AlloyElementSig::getAbsSignature() const{
+string AlloyElementSig::getAbsSignature() const {
 	return "abstract sig AbsElement {\n\
 		value: Int\n\
 		}\n";
-	
+
 }
 
-AlloySetSig::AlloySetSig(uint id, Set *set): Signature(id){
+AlloySetSig::AlloySetSig(uint id, Set *set) : Signature(id) {
 	ASSERT(set->getSize() > 0);
 	domain = to_string(set->getElement(0));
-	for(uint i=1; i< set->getSize(); i++){
+	for (uint i = 1; i < set->getSize(); i++) {
 		domain += " + " + to_string(set->getElement(i));
 	}
 }
 
-string AlloySetSig::toString() const{
+string AlloySetSig::toString() const {
 	return "Set" + to_string(id) + ".domain";
 }
 
-string AlloySetSig::getSignature() const{
+string AlloySetSig::getSignature() const {
 	string str;
-	if(encodeAbs){
+	if (encodeAbs) {
 		encodeAbs = false;
 		str += getAbsSignature();
 	}
@@ -96,9 +96,9 @@ string AlloySetSig::getSignature() const{
 	return str;
 }
 
-string AlloySetSig::getAbsSignature() const{
+string AlloySetSig::getAbsSignature() const {
 	return "abstract sig AbsSet {\n\
 		domain: set Int\n\
 		}\n";
-	
+
 }
diff --git a/src/Interpreter/alloysig.h b/src/Interpreter/alloysig.h
index 3fb2d10..7bffadf 100644
--- a/src/Interpreter/alloysig.h
+++ b/src/Interpreter/alloysig.h
@@ -6,10 +6,10 @@
 #include "classlist.h"
 using namespace std;
 
-class AlloyBoolSig: public ValuedSignature{
+class AlloyBoolSig : public ValuedSignature {
 public:
 	AlloyBoolSig(uint id);
-	virtual ~AlloyBoolSig(){}
+	virtual ~AlloyBoolSig() {}
 	virtual string toString() const;
 	virtual string getAbsSignature() const;
 	virtual string getSignature() const;
@@ -17,10 +17,10 @@ private:
 	static bool encodeAbs;
 };
 
-class AlloySetSig: public Signature{
+class AlloySetSig : public Signature {
 public:
 	AlloySetSig(uint id, Set *set);
-	virtual ~AlloySetSig(){}
+	virtual ~AlloySetSig() {}
 	virtual string toString() const;
 	virtual string getAbsSignature() const;
 	virtual string getSignature() const;
@@ -29,10 +29,10 @@ private:
 	string domain;
 };
 
-class AlloyElementSig: public ValuedSignature{
+class AlloyElementSig : public ValuedSignature {
 public:
 	AlloyElementSig(uint id, Signature *ssig);
-	virtual ~AlloyElementSig(){}
+	virtual ~AlloyElementSig() {}
 	virtual string toString() const;
 	virtual string getAbsSignature() const;
 	virtual string getSignature() const;
diff --git a/src/Interpreter/interpreter.cc b/src/Interpreter/interpreter.cc
index a5927f7..c4c7f8a 100644
--- a/src/Interpreter/interpreter.cc
+++ b/src/Interpreter/interpreter.cc
@@ -14,49 +14,49 @@
 
 using namespace std;
 
-Interpreter::Interpreter(CSolver *_solver): 
+Interpreter::Interpreter(CSolver *_solver) :
 	csolver(_solver),
 	sigEnc(this)
 {
 }
 
-Interpreter::~Interpreter(){
+Interpreter::~Interpreter() {
 }
 
-void Interpreter::encode(){
+void Interpreter::encode() {
 	dumpHeader();
 	SetIteratorBooleanEdge *iterator = csolver->getConstraints();
 	Vector<char *> facts;
-	while(iterator->hasNext()){
+	while (iterator->hasNext()) {
 		BooleanEdge constraint = iterator->next();
 		string constr = encodeConstraint(constraint);
-		char *cstr = new char [constr.length()+1];
+		char *cstr = new char [constr.length() + 1];
 		strcpy (cstr, constr.c_str());
 		facts.push(cstr);
 	}
 	dumpAllConstraints(facts);
-	for(uint i=0; i< facts.getSize(); i++){
+	for (uint i = 0; i < facts.getSize(); i++) {
 		char *cstr = facts.get(i);
 		delete[] cstr;
 	}
 	delete iterator;
 }
 
-uint Interpreter::getTimeout(){
-	uint timeout =csolver->getSatSolverTimeout(); 
-	return timeout == (uint)NOTIMEOUT? 1000: timeout;
+uint Interpreter::getTimeout() {
+	uint timeout = csolver->getSatSolverTimeout();
+	return timeout == (uint)NOTIMEOUT ? 1000 : timeout;
 }
 
-int Interpreter::solve(){
+int Interpreter::solve() {
 	dumpFooter();
 	int result = IS_INDETER;
 	char buffer [512];
-	if( output.is_open()){
+	if ( output.is_open()) {
 		output.close();
 	}
 	compileRunCommand(buffer, sizeof(buffer));
 	int status = system(buffer);
-	if (status == 0 || status == 512 ) { //For some unknown reason, SMTSat returns 512 when the problem successfully gets solved
+	if (status == 0 || status == 512 ) {//For some unknown reason, SMTSat returns 512 when the problem successfully gets solved
 		//Read data in from results file
 		result = getResult();
 	} else {
@@ -66,73 +66,73 @@ int Interpreter::solve(){
 	return result;
 }
 
-string Interpreter::encodeConstraint(BooleanEdge c){
+string Interpreter::encodeConstraint(BooleanEdge c) {
 	Boolean *constraint = c.getBoolean();
 	string res;
-	switch(constraint->type){
-		case LOGICOP:{
-			res = encodeBooleanLogic((BooleanLogic *) constraint);
-			break;
-		}
-		case PREDICATEOP:{
-			res = encodePredicate((BooleanPredicate *) constraint);
-			break;
-		}
-		case BOOLEANVAR:{
-			res = encodeBooleanVar( (BooleanVar *) constraint);
-			break;
-		}
-		default:
-			ASSERT(0);
+	switch (constraint->type) {
+	case LOGICOP: {
+		res = encodeBooleanLogic((BooleanLogic *) constraint);
+		break;
 	}
-	if(c.isNegated()){
+	case PREDICATEOP: {
+		res = encodePredicate((BooleanPredicate *) constraint);
+		break;
+	}
+	case BOOLEANVAR: {
+		res = encodeBooleanVar( (BooleanVar *) constraint);
+		break;
+	}
+	default:
+		ASSERT(0);
+	}
+	if (c.isNegated()) {
 		return negateConstraint(res);
 	}
 	return res;
 }
 
-string Interpreter::encodePredicate( BooleanPredicate *bp){
+string Interpreter::encodePredicate( BooleanPredicate *bp) {
 	switch (bp->predicate->type) {
-		case TABLEPRED:
-			ASSERT(0);
-		case OPERATORPRED:
-			return encodeOperatorPredicate(bp);
-		default:
-			ASSERT(0);
+	case TABLEPRED:
+		ASSERT(0);
+	case OPERATORPRED:
+		return encodeOperatorPredicate(bp);
+	default:
+		ASSERT(0);
 	}
 }
 
-string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint){
+string Interpreter::encodeOperatorPredicate(BooleanPredicate *constraint) {
 	PredicateOperator *predicate = (PredicateOperator *) constraint->predicate;
 	ASSERT(constraint->inputs.getSize() == 2);
 	string str;
 	Element *elem0 = constraint->inputs.get(0);
 	ASSERT(elem0->type == ELEMSET || elem0->type == ELEMFUNCRETURN || elem0->type == ELEMCONST);
 	ValuedSignature *elemSig1 = sigEnc.getElementSignature(elem0);
-	if(elem0->type == ELEMFUNCRETURN){
+	if (elem0->type == ELEMFUNCRETURN) {
 		str += processElementFunction((ElementFunction *) elem0, elemSig1);
 	}
 	Element *elem1 = constraint->inputs.get(1);
 	ASSERT(elem1->type == ELEMSET || elem1->type == ELEMFUNCRETURN || elem1->type == ELEMCONST);
 	ValuedSignature *elemSig2 = sigEnc.getElementSignature(elem1);
-	if(elem1->type == ELEMFUNCRETURN){
+	if (elem1->type == ELEMFUNCRETURN) {
 		str += processElementFunction((ElementFunction *) elem1, elemSig2);
 	}
 	str += operatorPredicateConstraint(predicate->getOp(), elemSig1, elemSig2);
 	return str;
 }
 
-void Interpreter::writeToFile(string str){
-	if(!str.empty()){
+void Interpreter::writeToFile(string str) {
+	if (!str.empty()) {
 		output << str << endl;
 	}
 }
 
-bool Interpreter::getBooleanValue(Boolean *b){
+bool Interpreter::getBooleanValue(Boolean *b) {
 	return (bool)sigEnc.getValue(b);
 }
 
-uint64_t Interpreter::getValue(Element * element){
+uint64_t Interpreter::getValue(Element *element) {
 	return (uint64_t)sigEnc.getValue(element);
 }
 
diff --git a/src/Interpreter/interpreter.h b/src/Interpreter/interpreter.h
index 32eed4a..dc61c18 100644
--- a/src/Interpreter/interpreter.h
+++ b/src/Interpreter/interpreter.h
@@ -8,7 +8,7 @@
 #include <fstream>
 using namespace std;
 
-class Interpreter{
+class Interpreter {
 public:
 	Interpreter(CSolver *solver);
 	void encode();
@@ -24,7 +24,7 @@ protected:
 	virtual void dumpFooter() = 0;
 	virtual void dumpHeader() = 0;
 	uint getTimeout();
-	virtual void compileRunCommand(char * command, size_t size) = 0;
+	virtual void compileRunCommand(char *command, size_t size) = 0;
 	string encodeConstraint(BooleanEdge constraint);
 	virtual int getResult() = 0;
 	virtual string negateConstraint(string constr) = 0;
diff --git a/src/Interpreter/mathsatinterpreter.cc b/src/Interpreter/mathsatinterpreter.cc
index 5123efe..8fb5f09 100644
--- a/src/Interpreter/mathsatinterpreter.cc
+++ b/src/Interpreter/mathsatinterpreter.cc
@@ -4,48 +4,48 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   smtsolvers.cc
  * Author: hamed
- * 
+ *
  * Created on February 21, 2019, 12:26 PM
  */
 
 #include "mathsatinterpreter.h"
 #include "solver_interface.h"
 
-MathSATInterpreter::MathSATInterpreter(CSolver *solver):
+MathSATInterpreter::MathSATInterpreter(CSolver *solver) :
 	SMTInterpreter(solver)
-{	
+{
 }
 
-void MathSATInterpreter::compileRunCommand(char * command , size_t size){
+void MathSATInterpreter::compileRunCommand(char *command, size_t size) {
 	model_print("Calling MathSAT...\n");
 	snprintf(command, size, "./run.sh timeout %u mathsat -model %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 }
 
-MathSATInterpreter::~MathSATInterpreter(){
+MathSATInterpreter::~MathSATInterpreter() {
 }
 
-int MathSATInterpreter::getResult(){
+int MathSATInterpreter::getResult() {
 	ifstream input(SMTSOLUTIONFILE, ios::in);
 	string line;
-	while(getline(input, line)){
-		if(line.find("unsat")!= line.npos){
+	while (getline(input, line)) {
+		if (line.find("unsat") != line.npos) {
 			return IS_UNSAT;
 		}
-		if(line.find("(") != line.npos){
-			char cline [line.size()+1];
+		if (line.find("(") != line.npos) {
+			char cline [line.size() + 1];
 			strcpy ( cline, line.c_str() );
 			char valuestr [512];
 			uint id;
-			if (2 == sscanf(cline,"%*[^0123456789]%u %s", &id, valuestr)){
+			if (2 == sscanf(cline,"%*[^0123456789]%u %s", &id, valuestr)) {
 				uint value;
-				if (strcmp (valuestr, "true)") == 0 ){
-					value =1;
-				}else if (strcmp(valuestr, "false)") == 0){
+				if (strcmp (valuestr, "true)") == 0 ) {
+					value = 1;
+				} else if (strcmp(valuestr, "false)") == 0) {
 					value = 0;
-				}else {
+				} else {
 					ASSERT(2 == sscanf(cline, "%*[^0123456789]%u%*[^0123456789]%u", &id, &value));
 				}
 
diff --git a/src/Interpreter/mathsatinterpreter.h b/src/Interpreter/mathsatinterpreter.h
index ef2ec9f..2110f59 100644
--- a/src/Interpreter/mathsatinterpreter.h
+++ b/src/Interpreter/mathsatinterpreter.h
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   mathsatinterpreter.h
  * Author: hamed
  *
@@ -17,15 +17,15 @@
 #include "smtinterpreter.h"
 
 
-class MathSATInterpreter: public SMTInterpreter{
+class MathSATInterpreter : public SMTInterpreter {
 public:
 	MathSATInterpreter(CSolver *solver);
 	virtual ~MathSATInterpreter();
 protected:
-	virtual void compileRunCommand(char * command , size_t size);
+	virtual void compileRunCommand(char *command, size_t size);
 	virtual int getResult();
 };
 
 
-#endif /* SMTSOLVERS_H */
+#endif/* SMTSOLVERS_H */
 
diff --git a/src/Interpreter/signature.cc b/src/Interpreter/signature.cc
index 94efbb2..d9724c9 100644
--- a/src/Interpreter/signature.cc
+++ b/src/Interpreter/signature.cc
@@ -1,21 +1,21 @@
 #include "signature.h"
 #include "set.h"
 
-ValuedSignature::ValuedSignature(uint id): 
-	Signature(id), 
-	value(-1) 
+ValuedSignature::ValuedSignature(uint id) :
+	Signature(id),
+	value(-1)
 {
 }
 
-int ValuedSignature::getValue(){
+int ValuedSignature::getValue() {
 	ASSERT(value != -1);
 	return value;
 }
 
-string Signature::operator+(const string& str){
+string Signature::operator+(const string &str) {
 	return toString() + str;
 }
 
-string operator+(const string& str, const Signature& sig){
-        return str + sig.toString();
+string operator+(const string &str, const Signature &sig) {
+	return str + sig.toString();
 }
diff --git a/src/Interpreter/signature.h b/src/Interpreter/signature.h
index e8c9e1c..3121051 100644
--- a/src/Interpreter/signature.h
+++ b/src/Interpreter/signature.h
@@ -5,27 +5,27 @@
 #include "classlist.h"
 using namespace std;
 
-class Signature{
+class Signature {
 public:
-	Signature(uint _id):id(_id){}
-	string operator+(const string& s);
+	Signature(uint _id) : id(_id) {}
+	string operator+(const string &s);
 	virtual string toString() const = 0;
-	virtual string getAbsSignature() const =0;
-	virtual string getSignature() const =0;
-	virtual ~Signature(){}
+	virtual string getAbsSignature() const = 0;
+	virtual string getSignature() const = 0;
+	virtual ~Signature() {}
 protected:
 	uint id;
 };
 
-class ValuedSignature: public Signature{
+class ValuedSignature : public Signature {
 public:
 	ValuedSignature(uint id);
 	int getValue();
-	void setValue(int v){value = v;}
+	void setValue(int v) {value = v;}
 protected:
 	int value;
 };
 
-string operator+(const string& str, const Signature& sig);
+string operator+(const string &str, const Signature &sig);
 
 #endif
diff --git a/src/Interpreter/signatureenc.cc b/src/Interpreter/signatureenc.cc
index cdc8aa1..1672c7a 100644
--- a/src/Interpreter/signatureenc.cc
+++ b/src/Interpreter/signatureenc.cc
@@ -4,30 +4,30 @@
 #include "signature.h"
 #include "interpreter.h"
 
-SignatureEnc::SignatureEnc(Interpreter *inter): 
+SignatureEnc::SignatureEnc(Interpreter *inter) :
 	interpreter(inter),
 	maxValue(0)
 {
 }
 
-SignatureEnc::~SignatureEnc(){
-	for(uint i=0; i<signatures.getSize(); i++){
+SignatureEnc::~SignatureEnc() {
+	for (uint i = 0; i < signatures.getSize(); i++) {
 		Signature *s = signatures.get(i);
 		delete s;
 	}
 }
 
-void SignatureEnc::updateMaxValue(Set *set){
-	for(uint i=0; i< set->getSize(); i++){
-		if(set->getElement(i) > maxValue){
+void SignatureEnc::updateMaxValue(Set *set) {
+	for (uint i = 0; i < set->getSize(); i++) {
+		if (set->getElement(i) > maxValue) {
 			maxValue = set->getElement(i);
 		}
 	}
 }
 
-ValuedSignature *SignatureEnc::getBooleanSignature(Boolean *bvar){
+ValuedSignature *SignatureEnc::getBooleanSignature(Boolean *bvar) {
 	ValuedSignature *bsig = (ValuedSignature *)encoded.get((void *)bvar);
-	if(bsig == NULL){
+	if (bsig == NULL) {
 		bsig = interpreter->getBooleanSignature(getUniqueSigID());
 		encoded.put(bvar, bsig);
 		signatures.push(bsig);
@@ -36,12 +36,12 @@ ValuedSignature *SignatureEnc::getBooleanSignature(Boolean *bvar){
 	return bsig;
 }
 
-ValuedSignature *SignatureEnc::getElementSignature(Element *element){
+ValuedSignature *SignatureEnc::getElementSignature(Element *element) {
 	ValuedSignature *esig = (ValuedSignature *)encoded.get((void *)element);
-	if(esig == NULL){
+	if (esig == NULL) {
 		Set *set = element->getRange();
 		Signature *ssig = (Signature *)encoded.get((void *)set);
-		if(ssig == NULL){
+		if (ssig == NULL) {
 			ssig = interpreter->getSetSignature(getUniqueSigID(), set);
 			encoded.put(set, ssig);
 			signatures.push(ssig);
@@ -57,13 +57,13 @@ ValuedSignature *SignatureEnc::getElementSignature(Element *element){
 	return esig;
 }
 
-void SignatureEnc::setValue(uint id, uint value){
+void SignatureEnc::setValue(uint id, uint value) {
 	ValuedSignature *sig = getValuedSignature(id);
 	ASSERT(sig != NULL);
 	sig->setValue(value);
 }
 
-int SignatureEnc::getValue(void *astnode){
+int SignatureEnc::getValue(void *astnode) {
 	ValuedSignature *sig = (ValuedSignature *)encoded.get(astnode);
 	ASSERT(sig != NULL);
 	return sig->getValue();
diff --git a/src/Interpreter/signatureenc.h b/src/Interpreter/signatureenc.h
index 988ac71..b11d9c5 100644
--- a/src/Interpreter/signatureenc.h
+++ b/src/Interpreter/signatureenc.h
@@ -13,13 +13,13 @@ public:
 	ValuedSignature *getElementSignature(Element *element);
 	ValuedSignature *getBooleanSignature(Boolean *bvar);
 	int getValue(void *astnode);
-	uint64_t getMaxValue(){ return maxValue;}
+	uint64_t getMaxValue() { return maxValue;}
 private:
-	ValuedSignature *getValuedSignature(uint uniqueID){return (ValuedSignature*)signatures.get(uniqueID-1);}
-	uint getUniqueSigID(){return signatures.getSize() +1;}
+	ValuedSignature *getValuedSignature(uint uniqueID) {return (ValuedSignature *)signatures.get(uniqueID - 1);}
+	uint getUniqueSigID() {return signatures.getSize() + 1;}
 	void updateMaxValue(Set *set);
 	CloneMap encoded;
-	Vector<Signature*> signatures;
+	Vector<Signature *> signatures;
 	Interpreter *interpreter;
 	uint64_t maxValue;
 };
diff --git a/src/Interpreter/smtinterpreter.cc b/src/Interpreter/smtinterpreter.cc
index 7780931..1b5e028 100644
--- a/src/Interpreter/smtinterpreter.cc
+++ b/src/Interpreter/smtinterpreter.cc
@@ -15,53 +15,53 @@
 
 using namespace std;
 
-SMTInterpreter::SMTInterpreter(CSolver *_solver): 
-	Interpreter(_solver) 
+SMTInterpreter::SMTInterpreter(CSolver *_solver) :
+	Interpreter(_solver)
 {
 	output.open(SMTFILENAME);
-	if(!output.is_open()){
+	if (!output.is_open()) {
 		model_print("AlloyEnc:Error in opening the dump file satune.smt\n");
 		exit(-1);
 	}
 }
 
-SMTInterpreter::~SMTInterpreter(){
-	if(output.is_open()){
+SMTInterpreter::~SMTInterpreter() {
+	if (output.is_open()) {
 		output.close();
 	}
 }
 
 
-ValuedSignature *SMTInterpreter::getBooleanSignature(uint id){
+ValuedSignature *SMTInterpreter::getBooleanSignature(uint id) {
 	return new SMTBoolSig(id);
 }
 
-ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig){
+ValuedSignature *SMTInterpreter::getElementSignature(uint id, Signature *ssig) {
 	return new SMTElementSig(id, (SMTSetSig *)ssig);
 }
 
-Signature *SMTInterpreter::getSetSignature(uint id, Set *set){
+Signature *SMTInterpreter::getSetSignature(uint id, Set *set) {
 	return new SMTSetSig(id, set);
 }
 
-void SMTInterpreter::dumpAllConstraints(Vector<char *> &facts){
-	for(uint i=0; i< facts.getSize(); i++){
+void SMTInterpreter::dumpAllConstraints(Vector<char *> &facts) {
+	for (uint i = 0; i < facts.getSize(); i++) {
 		char *cstr = facts.get(i);
 		writeToFile("(assert " + string(cstr) + ")");
 	}
 }
 
-void SMTInterpreter::extractValue(char *idline, char *valueline){
+void SMTInterpreter::extractValue(char *idline, char *valueline) {
 	uint id;
-	if (1 == sscanf(idline,"%*[^0123456789]%u", &id)){
+	if (1 == sscanf(idline,"%*[^0123456789]%u", &id)) {
 		char valuestr [512];
 		ASSERT(1 == sscanf(valueline,"%s)", valuestr));
 		uint value;
-		if (strcmp (valuestr, "true)") == 0 ){
-			value =1;
-		}else if (strcmp(valuestr, "false)") == 0){
+		if (strcmp (valuestr, "true)") == 0 ) {
+			value = 1;
+		} else if (strcmp(valuestr, "false)") == 0) {
 			value = 0;
-		}else {
+		} else {
 			ASSERT(1 == sscanf(valueline, "%*[^0123456789]%u", &value));
 		}
 
@@ -72,19 +72,19 @@ void SMTInterpreter::extractValue(char *idline, char *valueline){
 	}
 }
 
-int SMTInterpreter::getResult(){
+int SMTInterpreter::getResult() {
 	ifstream input(SMTSOLUTIONFILE, ios::in);
 	string line;
-	while(getline(input, line)){
-		if(line.find("unsat")!= line.npos){
+	while (getline(input, line)) {
+		if (line.find("unsat") != line.npos) {
 			return IS_UNSAT;
 		}
-		if(line.find("(define-fun") != line.npos || line.find("( (") != line.npos){
+		if (line.find("(define-fun") != line.npos || line.find("( (") != line.npos) {
 			string valueline;
 			ASSERT(getline(input, valueline));
-			char cline [line.size()+1];
+			char cline [line.size() + 1];
 			strcpy ( cline, line.c_str() );
-			char vline [valueline.size()+1];
+			char vline [valueline.size() + 1];
 			strcpy ( vline, valueline.c_str() );
 			extractValue(cline, vline);
 		}
@@ -92,75 +92,75 @@ int SMTInterpreter::getResult(){
 	return IS_SAT;
 }
 
-void SMTInterpreter::dumpFooter(){
+void SMTInterpreter::dumpFooter() {
 	output << "(check-sat)" << endl;
 	output << "(get-model)" << endl;
 }
 
-void SMTInterpreter::dumpHeader(){
+void SMTInterpreter::dumpHeader() {
 }
 
-void SMTInterpreter::compileRunCommand(char * command, size_t size){
+void SMTInterpreter::compileRunCommand(char *command, size_t size) {
 	model_print("Calling Z3...\n");
 	snprintf(command, size, "./run.sh z3 -T:%u -in < %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 }
 
-string SMTInterpreter::negateConstraint(string constr){
+string SMTInterpreter::negateConstraint(string constr) {
 	return "( not " + constr + " )";
 }
 
-string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl){
+string SMTInterpreter::encodeBooleanLogic( BooleanLogic *bl) {
 	uint size = bl->inputs.getSize();
 	string array[size];
 	for (uint i = 0; i < size; i++)
 		array[i] = encodeConstraint(bl->inputs.get(i));
 	string op;
-	switch (bl->op){
-		case SATC_OR:
-			op = "or";
-			break;
-		case SATC_AND:
-			op = "and";
-			break;
-		case SATC_NOT:
-			op = "not";
-			break;
-		case SATC_IMPLIES:
-			op = "=>";
-			break;
-		case SATC_XOR:
-		default:
-			ASSERT(0);
+	switch (bl->op) {
+	case SATC_OR:
+		op = "or";
+		break;
+	case SATC_AND:
+		op = "and";
+		break;
+	case SATC_NOT:
+		op = "not";
+		break;
+	case SATC_IMPLIES:
+		op = "=>";
+		break;
+	case SATC_XOR:
+	default:
+		ASSERT(0);
 	}
 	switch (bl->op) {
-		case SATC_XOR:
-		case SATC_OR:
-		case SATC_AND:{
-			ASSERT(size >= 2);
-			string res = array[0];
-			for( uint i=1; i< size; i++){
-				res = "( " + op + " " + res + " " +  array[i] + " )";
-			}
-			return res;
+	case SATC_XOR:
+	case SATC_OR:
+	case SATC_AND: {
+		ASSERT(size >= 2);
+		string res = array[0];
+		for ( uint i = 1; i < size; i++) {
+			res = "( " + op + " " + res + " " +  array[i] + " )";
 		}
-		case SATC_NOT:{
-			return "( not " + array[0] + " )";
-		}
-		case SATC_IMPLIES:
-			return "( " + op + " " + array[0] + " " + array[1] + " )";
-		case SATC_IFF:
-		default:
-			ASSERT(0);
+		return res;
+	}
+	case SATC_NOT: {
+		return "( not " + array[0] + " )";
+	}
+	case SATC_IMPLIES:
+		return "( " + op + " " + array[0] + " " + array[1] + " )";
+	case SATC_IFF:
+	default:
+		ASSERT(0);
 
 	}
 }
 
-string SMTInterpreter::encodeBooleanVar( BooleanVar *bv){
-	ValuedSignature * boolSig = sigEnc.getBooleanSignature(bv);
+string SMTInterpreter::encodeBooleanVar( BooleanVar *bv) {
+	ValuedSignature *boolSig = sigEnc.getBooleanSignature(bv);
 	return *boolSig + "";
 }
 
-string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedSignature *signature){
+string SMTInterpreter::processElementFunction(ElementFunction *elemFunc, ValuedSignature *signature) {
 	FunctionOperator *function = (FunctionOperator *) elemFunc->getFunction();
 	uint numDomains = elemFunc->inputs.getSize();
 	ASSERT(numDomains > 1);
@@ -169,22 +169,22 @@ string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedS
 	for (uint i = 0; i < numDomains; i++) {
 		Element *elem = elemFunc->inputs.get(i);
 		inputs[i] = sigEnc.getElementSignature(elem);
-		if(elem->type == ELEMFUNCRETURN){
+		if (elem->type == ELEMFUNCRETURN) {
 			result += processElementFunction((ElementFunction *) elem, inputs[i]);
 		}
 	}
 	string op;
-	switch(function->op){
-		case SATC_ADD:
-			op = "+";
-			break;
-		case SATC_SUB:
-			op = "-";
-			break;
-		default:
-			ASSERT(0);
+	switch (function->op) {
+	case SATC_ADD:
+		op = "+";
+		break;
+	case SATC_SUB:
+		op = "-";
+		break;
+	default:
+		ASSERT(0);
 	}
-	result += "( = " + *signature; 
+	result += "( = " + *signature;
 	string tmp = "" + *inputs[0];
 	for (uint i = 1; i < numDomains; i++) {
 		tmp = "( " + op + " " + tmp + " " + *inputs[i] + " )";
@@ -193,16 +193,16 @@ string SMTInterpreter::processElementFunction(ElementFunction* elemFunc, ValuedS
 	return result;
 }
 
-string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2){
+string SMTInterpreter::operatorPredicateConstraint(CompOp op, ValuedSignature *elemSig1, ValuedSignature *elemSig2) {
 	switch (op) {
-		case SATC_EQUALS:
-			return "( = " + *elemSig1 + " " + *elemSig2 +" )";
-		case SATC_LT:
-			return "( < " + *elemSig1 + " " + *elemSig2 + " )";
-		case SATC_GT:
-			return "(> " + *elemSig1 + " " + *elemSig2 + " )";
-		default:
-			ASSERT(0);
+	case SATC_EQUALS:
+		return "( = " + *elemSig1 + " " + *elemSig2 + " )";
+	case SATC_LT:
+		return "( < " + *elemSig1 + " " + *elemSig2 + " )";
+	case SATC_GT:
+		return "(> " + *elemSig1 + " " + *elemSig2 + " )";
+	default:
+		ASSERT(0);
 	}
 }
 
diff --git a/src/Interpreter/smtinterpreter.h b/src/Interpreter/smtinterpreter.h
index 035e76b..37dae88 100644
--- a/src/Interpreter/smtinterpreter.h
+++ b/src/Interpreter/smtinterpreter.h
@@ -10,7 +10,7 @@
 #define SMTFILENAME "satune.smt"
 #define SMTSOLUTIONFILE "solution.sol"
 
-class SMTInterpreter: public Interpreter{
+class SMTInterpreter : public Interpreter {
 public:
 	SMTInterpreter(CSolver *solver);
 	virtual ValuedSignature *getBooleanSignature(uint id);
@@ -20,7 +20,7 @@ public:
 protected:
 	virtual void dumpFooter();
 	virtual void dumpHeader();
-	virtual void compileRunCommand(char * command , size_t size);
+	virtual void compileRunCommand(char *command, size_t size);
 	virtual int getResult();
 	virtual void dumpAllConstraints(Vector<char *> &facts);
 	virtual string negateConstraint(string constr);
diff --git a/src/Interpreter/smtratinterpreter.cc b/src/Interpreter/smtratinterpreter.cc
index 9742bda..2a59cc5 100644
--- a/src/Interpreter/smtratinterpreter.cc
+++ b/src/Interpreter/smtratinterpreter.cc
@@ -4,24 +4,24 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   smtratinterpreter.cc
  * Author: hamed
- * 
+ *
  * Created on February 21, 2019, 2:33 PM
  */
 
 #include "smtratinterpreter.h"
 
-SMTRatInterpreter::SMTRatInterpreter(CSolver *solver): 
+SMTRatInterpreter::SMTRatInterpreter(CSolver *solver) :
 	SMTInterpreter(solver)
-{	
+{
 }
 
-void SMTRatInterpreter::compileRunCommand(char * command , size_t size){
+void SMTRatInterpreter::compileRunCommand(char *command, size_t size) {
 	model_print("Calling SMTRat...\n");
 	snprintf(command, size, "./run.sh timeout %u smtrat %s > %s", getTimeout(), SMTFILENAME, SMTSOLUTIONFILE);
 }
 
-SMTRatInterpreter::~SMTRatInterpreter(){
+SMTRatInterpreter::~SMTRatInterpreter() {
 }
diff --git a/src/Interpreter/smtratinterpreter.h b/src/Interpreter/smtratinterpreter.h
index f2afb49..f6eea03 100644
--- a/src/Interpreter/smtratinterpreter.h
+++ b/src/Interpreter/smtratinterpreter.h
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   smtratinterpreter.h
  * Author: hamed
  *
@@ -15,13 +15,13 @@
 #define SMTRATINTERPRETER_H
 #include "smtinterpreter.h"
 
-class SMTRatInterpreter: public SMTInterpreter{
+class SMTRatInterpreter : public SMTInterpreter {
 public:
 	SMTRatInterpreter(CSolver *solver);
 	virtual ~SMTRatInterpreter();
 protected:
-	void compileRunCommand(char * command , size_t size);
+	void compileRunCommand(char *command, size_t size);
 };
 
-#endif /* SMTRATINTERPRETER_H */
+#endif/* SMTRATINTERPRETER_H */
 
diff --git a/src/Interpreter/smtsig.cc b/src/Interpreter/smtsig.cc
index 4c77493..6ccbd22 100644
--- a/src/Interpreter/smtsig.cc
+++ b/src/Interpreter/smtsig.cc
@@ -1,39 +1,39 @@
 #include "smtsig.h"
 #include "set.h"
 
-SMTBoolSig::SMTBoolSig(uint id):
+SMTBoolSig::SMTBoolSig(uint id) :
 	ValuedSignature(id)
 {
 }
 
-string SMTBoolSig::toString() const{
+string SMTBoolSig::toString() const {
 	return "b" + to_string(id);
 }
 
-string SMTBoolSig::getSignature() const{
+string SMTBoolSig::getSignature() const {
 	return "(declare-const b" + to_string(id) + " Bool)";
 }
 
-string SMTBoolSig::getAbsSignature() const{
+string SMTBoolSig::getAbsSignature() const {
 	return "";
 }
 
-SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig): 
+SMTElementSig::SMTElementSig(uint id, SMTSetSig *_ssig) :
 	ValuedSignature(id),
 	ssig(_ssig)
 {
 }
 
-string SMTElementSig::toString() const{
+string SMTElementSig::toString() const {
 	return "e" + to_string(id);
 }
 
-string SMTElementSig::getSignature() const{
+string SMTElementSig::getSignature() const {
 	string str = "(declare-const e" + to_string(id) + " Int)\n";
 	string constraint = ssig->getAbsSignature();
 	size_t start_pos;
 	string placeholder = "$";
-	while((start_pos = constraint.find(placeholder)) != string::npos){
+	while ((start_pos = constraint.find(placeholder)) != string::npos) {
 		constraint.replace(start_pos, placeholder.size(), to_string(id));
 	}
 	//constraint.replace(constraint.begin(), constraint.end(), "$", );
@@ -41,41 +41,41 @@ string SMTElementSig::getSignature() const{
 	return str;
 }
 
-string SMTElementSig::getAbsSignature() const{
+string SMTElementSig::getAbsSignature() const {
 	return "";
-	
+
 }
 
-SMTSetSig::SMTSetSig(uint id, Set *set): Signature(id){
+SMTSetSig::SMTSetSig(uint id, Set *set) : Signature(id) {
 	ASSERT(set->getSize() > 0);
-	int min = set->getElement(0), max = set->getElement(set->getSize()-1);
+	int min = set->getElement(0), max = set->getElement(set->getSize() - 1);
 	Vector<int> holes;
 	int prev = set->getElement(0);
-	for(uint i=1; i< set->getSize(); i++){
+	for (uint i = 1; i < set->getSize(); i++) {
 		int curr = set->getElement(i);
-		if(prev != curr -1){
-			for(int j=prev+1; j< curr; j++){
+		if (prev != curr - 1) {
+			for (int j = prev + 1; j < curr; j++) {
 				holes.push(j);
 			}
 		}
 		prev = curr;
 	}
-	constraint = "(assert (<= e$ " + to_string(max) +"))\n";
-	constraint += "(assert (>= e$ " + to_string(min) +"))\n";
-	for(uint i=0; i< holes.getSize(); i++){
-		constraint += "(assert (not (= e$ " + to_string(holes.get(i)) +")))\n";
+	constraint = "(assert (<= e$ " + to_string(max) + "))\n";
+	constraint += "(assert (>= e$ " + to_string(min) + "))\n";
+	for (uint i = 0; i < holes.getSize(); i++) {
+		constraint += "(assert (not (= e$ " + to_string(holes.get(i)) + ")))\n";
 	}
 }
 
-string SMTSetSig::toString() const{
+string SMTSetSig::toString() const {
 	return "";
 }
 
-string SMTSetSig::getSignature() const{
+string SMTSetSig::getSignature() const {
 	return "";
 }
 
-string SMTSetSig::getAbsSignature() const{
+string SMTSetSig::getAbsSignature() const {
 	return constraint;
-	
+
 }
diff --git a/src/Interpreter/smtsig.h b/src/Interpreter/smtsig.h
index 7804176..21271e2 100644
--- a/src/Interpreter/smtsig.h
+++ b/src/Interpreter/smtsig.h
@@ -6,19 +6,19 @@
 #include "classlist.h"
 using namespace std;
 
-class SMTBoolSig: public ValuedSignature{
+class SMTBoolSig : public ValuedSignature {
 public:
 	SMTBoolSig(uint id);
-	virtual ~SMTBoolSig(){}
+	virtual ~SMTBoolSig() {}
 	virtual string toString() const;
 	virtual string getAbsSignature() const;
 	virtual string getSignature() const;
 };
 
-class SMTSetSig: public Signature{
+class SMTSetSig : public Signature {
 public:
 	SMTSetSig(uint id, Set *set);
-	virtual ~SMTSetSig(){}
+	virtual ~SMTSetSig() {}
 	virtual string toString() const;
 	virtual string getAbsSignature() const;
 	virtual string getSignature() const;
@@ -26,10 +26,10 @@ private:
 	string constraint;
 };
 
-class SMTElementSig: public ValuedSignature{
+class SMTElementSig : public ValuedSignature {
 public:
 	SMTElementSig(uint id, SMTSetSig *ssig);
-	virtual ~SMTElementSig(){}
+	virtual ~SMTElementSig() {}
 	virtual string toString() const;
 	virtual string getAbsSignature() const;
 	virtual string getSignature() const;
diff --git a/src/Serialize/deserializer.cc b/src/Serialize/deserializer.cc
index eac11e9..d0cfb6c 100644
--- a/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@ -29,7 +29,7 @@ Deserializer::Deserializer(const char *file, InterpreterType itype) :
 	if (filedesc < 0) {
 		exit(-1);
 	}
-	if(itype != SATUNE){
+	if (itype != SATUNE) {
 		solver->setInterpreter(itype);
 	}
 }
diff --git a/src/Test/deserializealloytest.cc b/src/Test/deserializealloytest.cc
index 8677bf3..69c29fb 100644
--- a/src/Test/deserializealloytest.cc
+++ b/src/Test/deserializealloytest.cc
@@ -1,14 +1,14 @@
 #include "csolver.h"
 
 
-InterpreterType getInterpreterType(char * itype){
-	if(strcmp (itype,"--alloy") == 0){
+InterpreterType getInterpreterType(char *itype) {
+	if (strcmp (itype,"--alloy") == 0) {
 		return ALLOY;
-	} else if(strcmp (itype,"--z3") == 0){
+	} else if (strcmp (itype,"--z3") == 0) {
 		return Z3;
-	} else if(strcmp (itype,"--smtrat") == 0){
+	} else if (strcmp (itype,"--smtrat") == 0) {
 		return SMTRAT;
-	} else if(strcmp (itype,"--mathsat") == 0){
+	} else if (strcmp (itype,"--mathsat") == 0) {
 		return MATHSAT;
 	} else {
 		printf("Unknown interpreter type: %s\n", itype);
@@ -24,10 +24,10 @@ int main(int argc, char **argv) {
 		printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat] [timeout]\n");
 		exit(-1);
 	}
-	CSolver *solver; 
-	if(argc >= 3){
+	CSolver *solver;
+	if (argc >= 3) {
 		solver = CSolver::deserialize(argv[1], getInterpreterType(argv[2]));
-		if(argc == 4){
+		if (argc == 4) {
 			solver->setSatSolverTimeout(atol(argv[3]));
 		}
 	} else {
diff --git a/src/Test/printtuner.cc b/src/Test/printtuner.cc
index 8a3ccbd..8a3395a 100644
--- a/src/Test/printtuner.cc
+++ b/src/Test/printtuner.cc
@@ -7,7 +7,7 @@ int main(int argc, char **argv) {
 		printf("You should specify a tuner: %s <best.tuner>\n", argv[0]);
 		exit(-1);
 	}
-	
+
 	SearchTuner *tuner = new SearchTuner(argv[1]);
 	tuner->print();
 	delete tuner;
diff --git a/src/Test/runmultituner.cc b/src/Test/runmultituner.cc
index e2ecbd8..8ba717e 100644
--- a/src/Test/runmultituner.cc
+++ b/src/Test/runmultituner.cc
@@ -5,20 +5,20 @@
 #include "comptuner.h"
 #include "randomtuner.h"
 
-void printKnownTunerTypes(){
+void printKnownTunerTypes() {
 	printf("Known Tuner Types:\nRandom Tuner=1\nComp Tuner=2\nKmeans Tuner=3\nSimulated Annealing Tuner=4\n");
 }
 
-BasicTuner *createTuner(uint tunertype, uint budget, uint rounds, uint timeout){
-	switch(tunertype){
-		case 1: return new RandomTuner(budget, timeout);
-		case 2: return new CompTuner(budget, timeout);
-		case 3: return new KMeansTuner(budget, rounds, timeout);
-		case 4: return new SATuner(budget, timeout);
-		default:
-			printf("Tuner type %u is unknown\n", tunertype);
-			printKnownTunerTypes();
-			exit(-1);
+BasicTuner *createTuner(uint tunertype, uint budget, uint rounds, uint timeout) {
+	switch (tunertype) {
+	case 1: return new RandomTuner(budget, timeout);
+	case 2: return new CompTuner(budget, timeout);
+	case 3: return new KMeansTuner(budget, rounds, timeout);
+	case 4: return new SATuner(budget, timeout);
+	default:
+		printf("Tuner type %u is unknown\n", tunertype);
+		printKnownTunerTypes();
+		exit(-1);
 	}
 
 }
@@ -47,7 +47,7 @@ int main(int argc, char **argv) {
 			else
 				multituner->addProblem(argv[i]);
 		} else
-			multituner->addTuner(new SearchTuner(argv[i], true )); //add settings to usedsettigs
+			multituner->addTuner(new SearchTuner(argv[i], true ));//add settings to usedsettigs
 	}
 
 	if (!tunerfiles) {
diff --git a/src/Tuner/basictuner.cc b/src/Tuner/basictuner.cc
index a2d93bf..6f0f5e0 100644
--- a/src/Tuner/basictuner.cc
+++ b/src/Tuner/basictuner.cc
@@ -4,10 +4,10 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   basictuner.cc
  * Author: hamed
- * 
+ *
  * Created on December 17, 2018, 2:02 PM
  */
 
@@ -38,7 +38,7 @@ void TunerRecord::setTime(Problem *problem, long long time) {
 	timetaken.put(problem, time);
 }
 
-void TunerRecord::print(){
+void TunerRecord::print() {
 	model_print("*************TUNER NUMBER=%d***********\n", tunernumber);
 	tuner->print();
 	model_print("&&&&&&&&&&&&&USED SETTINGS &&&&&&&&&&&&\n");
@@ -46,7 +46,7 @@ void TunerRecord::print(){
 	model_print("\n");
 }
 
-void TunerRecord::printProblemsInfo(){
+void TunerRecord::printProblemsInfo() {
 	for (uint j = 0; j < problems.getSize(); j++) {
 		Problem *problem = problems.get(j);
 		model_print("Problem %s\n", problem->getProblem());
@@ -70,7 +70,7 @@ TunerRecord *TunerRecord::changeTuner(SearchTuner *_newtuner) {
 
 
 BasicTuner::BasicTuner(uint _budget, uint _timeout) :
-	budget(_budget), timeout(_timeout), execnum(0){
+	budget(_budget), timeout(_timeout), execnum(0) {
 }
 
 BasicTuner::~BasicTuner() {
@@ -102,10 +102,10 @@ void BasicTuner::printData() {
 	}
 }
 
-bool BasicTuner::tunerExists(TunerRecord *tunerec){
+bool BasicTuner::tunerExists(TunerRecord *tunerec) {
 	SearchTuner *tuner = tunerec->getTuner();
-	for(uint i=0; i< explored.getSize(); i++){
-		if(explored.get(i)->getTuner()->equalUsed(tuner)){
+	for (uint i = 0; i < explored.getSize(); i++) {
+		if (explored.get(i)->getTuner()->equalUsed(tuner)) {
 			model_print("************Tuner <%d> is replicate of Tuner <%d>\n", tunerec->getTunerNumber(), explored.get(i)->getTunerNumber());
 			return true;
 		}
@@ -210,10 +210,10 @@ SearchTuner *BasicTuner::mutateTuner(SearchTuner *oldTuner, uint k) {
 	return newTuner;
 }
 
-int BasicTuner::subTunerIndex(SearchTuner *newTuner){
-	for (uint i=0; i< explored.getSize(); i++){
+int BasicTuner::subTunerIndex(SearchTuner *newTuner) {
+	for (uint i = 0; i < explored.getSize(); i++) {
 		SearchTuner *tuner = explored.get(i)->getTuner();
-		if(tuner->isSubTunerof(newTuner)){
+		if (tuner->isSubTunerof(newTuner)) {
 			return i;
 		}
 	}
diff --git a/src/Tuner/basictuner.h b/src/Tuner/basictuner.h
index 14ab7d8..0df9a65 100644
--- a/src/Tuner/basictuner.h
+++ b/src/Tuner/basictuner.h
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   basictuner.h
  * Author: hamed
  *
@@ -25,11 +25,11 @@ class Problem {
 public:
 	Problem(const char *problem);
 	char *getProblem() {return problem;}
-	inline int getResult(){return result;}
-	inline int getProblemNumber(){return problemnumber;}
-	inline void setResult(int res){result = res;}
-	inline void setProblemNumber(int probNum){problemnumber = probNum;}
-	inline long long getBestTime() {return besttime ;} 
+	inline int getResult() {return result;}
+	inline int getProblemNumber() {return problemnumber;}
+	inline void setResult(int res) {result = res;}
+	inline void setProblemNumber(int probNum) {problemnumber = probNum;}
+	inline long long getBestTime() {return besttime ;}
 	inline void setBestTime(long long time) {besttime = time;}
 	~Problem();
 	CMEMALLOC;
@@ -45,18 +45,18 @@ public:
 	TunerRecord(SearchTuner *_tuner) : tuner(_tuner), tunernumber(-1), isduplicate(false) {}
 	TunerRecord(SearchTuner *_tuner, int _tunernumber) : tuner(_tuner), tunernumber(_tunernumber), isduplicate(false) {}
 	SearchTuner *getTuner() {return tuner;}
-	void inline addProblem(Problem * problem){problems.push(problem);}
+	void inline addProblem(Problem *problem) {problems.push(problem);}
 	TunerRecord *changeTuner(SearchTuner *_newtuner);
 	void updateTuner(SearchTuner *_newtuner) {tuner = _newtuner;}
 	long long getTime(Problem *problem);
 	void setTime(Problem *problem, long long time);
-	inline void setTunerNumber(int numb){tunernumber = numb;}
-	inline int getTunerNumber(){return tunernumber;}
+	inline void setTunerNumber(int numb) {tunernumber = numb;}
+	inline int getTunerNumber() {return tunernumber;}
 	inline uint problemsSize() {return problems.getSize();}
 	inline void setDuplicate(bool _duplicate) { isduplicate = _duplicate;}
 	inline bool isDuplicate() {return isduplicate;}
-	inline Problem *getProblem(uint index){return problems.get(index);}
-        void print();
+	inline Problem *getProblem(uint index) {return problems.get(index);}
+	void print();
 	void printProblemsInfo();
 	CMEMALLOC;
 private:
@@ -80,12 +80,12 @@ public:
 protected:
 	long long evaluate(Problem *problem, TunerRecord *tuner);
 	/**
-         * returns the index of the tuner which is subtune of
-         * the newTuner 
-         * @param newTuner
-         * @return 
-         */
-        int subTunerIndex(SearchTuner *newTuner);
+	 * returns the index of the tuner which is subtune of
+	 * the newTuner
+	 * @param newTuner
+	 * @return
+	 */
+	int subTunerIndex(SearchTuner *newTuner);
 	bool tunerExists(TunerRecord *tunerRec);
 	SearchTuner *mutateTuner(SearchTuner *oldTuner, uint k);
 	void updateTimeout(Problem *problem, long long metric);
@@ -98,5 +98,5 @@ protected:
 	int execnum;
 };
 
-#endif /* BASICTUNER_H */
+#endif/* BASICTUNER_H */
 
diff --git a/src/Tuner/comptuner.cc b/src/Tuner/comptuner.cc
index 895e06b..8069915 100644
--- a/src/Tuner/comptuner.cc
+++ b/src/Tuner/comptuner.cc
@@ -11,8 +11,8 @@ CompTuner::CompTuner(uint _budget, uint _timeout) :
 {
 }
 
-CompTuner::~CompTuner(){
-	
+CompTuner::~CompTuner() {
+
 }
 
 void CompTuner::findBestThreeTuners() {
@@ -127,12 +127,12 @@ void CompTuner::tune() {
 		model_print("Round %u of %u\n", b, budget);
 		Hashtable<TunerRecord *, int, uint64_t> scores;
 		Vector<Vector<TunerRecord *> *> allplaces;
-		for(uint ii=0; ii< problems.getSize(); ii++){
+		for (uint ii = 0; ii < problems.getSize(); ii++) {
 			allplaces.push(new Vector<TunerRecord *>());
 		}
 		for (uint j = 0; j < tunerV->getSize(); j++) {
 			TunerRecord *tuner = tunerV->get(j);
-			
+
 			for (uint i = 0; i < problems.getSize(); i++) {
 				Vector<TunerRecord *> *places = allplaces.get(i);
 				Problem *problem = problems.get(i);
@@ -148,8 +148,8 @@ void CompTuner::tune() {
 						tuner->setTime(problem, metric);
 					else
 						tuner->setTime(problem, -2);
-					
-					if(tunerExists(tuner)){
+
+					if (tunerExists(tuner)) {
 						//Solving the problem and noticing the tuner
 						//already exists
 						tuner->setDuplicate(true);
@@ -167,13 +167,13 @@ void CompTuner::tune() {
 				}
 			}
 		}
-		for(uint ii=0; ii < problems.getSize(); ii++){
+		for (uint ii = 0; ii < problems.getSize(); ii++) {
 			Problem *problem = problems.get(ii);
 			Vector<TunerRecord *> *places = allplaces.get(ii);
 			int points = 9;
 			for (uint k = 0; k < places->getSize() && points; k++) {
 				TunerRecord *tuner = places->get(k);
-				if(tuner->isDuplicate()){
+				if (tuner->isDuplicate()) {
 					continue;
 				}
 				int currScore = 0;
@@ -186,7 +186,7 @@ void CompTuner::tune() {
 				points = points / 3;
 			}
 		}
-		for(uint ii=0; ii< problems.getSize(); ii++){
+		for (uint ii = 0; ii < problems.getSize(); ii++) {
 			delete allplaces.get(ii);
 		}
 		Vector<TunerRecord *> ranking;
@@ -220,7 +220,7 @@ void CompTuner::tune() {
 		uint tSize = tunerV->getSize();
 		for (uint i = 0; i < tSize; i++) {
 			SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), b);
-			while(subTunerIndex(tmpTuner) != -1){
+			while (subTunerIndex(tmpTuner) != -1) {
 				model_print("******** New Tuner already explored...\n");
 				delete tmpTuner;
 				tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), b);
diff --git a/src/Tuner/comptuner.h b/src/Tuner/comptuner.h
index dd28105..39e7946 100644
--- a/src/Tuner/comptuner.h
+++ b/src/Tuner/comptuner.h
@@ -13,7 +13,7 @@ public:
 	void tune();
 	void findBestThreeTuners();
 protected:
-	
+
 };
 
 inline long long min(long long num1, long long num2, long long num3) {
diff --git a/src/Tuner/kmeanstuner.cc b/src/Tuner/kmeanstuner.cc
index 333d9d9..a4c1cdc 100644
--- a/src/Tuner/kmeanstuner.cc
+++ b/src/Tuner/kmeanstuner.cc
@@ -4,10 +4,10 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   kmeanstuner.cc
  * Author: hamed
- * 
+ *
  * Created on December 19, 2018, 4:16 PM
  */
 
@@ -16,7 +16,7 @@
 #include "searchtuner.h"
 #include "math.h"
 
-KMeansTuner::KMeansTuner(uint budget, uint _rounds, uint timeout) : 
+KMeansTuner::KMeansTuner(uint budget, uint _rounds, uint timeout) :
 	BasicTuner(budget, timeout),
 	rounds(_rounds) {
 }
diff --git a/src/Tuner/kmeanstuner.h b/src/Tuner/kmeanstuner.h
index a6025a3..1e8adb3 100644
--- a/src/Tuner/kmeanstuner.h
+++ b/src/Tuner/kmeanstuner.h
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   kmeanstuner.h
  * Author: hamed
  *
@@ -30,5 +30,5 @@ private:
 	uint rounds;
 };
 
-#endif /* KMEANSTUNER_H */
+#endif/* KMEANSTUNER_H */
 
diff --git a/src/Tuner/randomtuner.cc b/src/Tuner/randomtuner.cc
index 6fefc46..04b5e7c 100644
--- a/src/Tuner/randomtuner.cc
+++ b/src/Tuner/randomtuner.cc
@@ -8,24 +8,24 @@
 
 #define UNSETVALUE -1
 
-RandomTuner::RandomTuner(uint _budget, uint _timeout) : 
+RandomTuner::RandomTuner(uint _budget, uint _timeout) :
 	BasicTuner(_budget, _timeout) {
 }
 
-RandomTuner::~RandomTuner(){
-	
+RandomTuner::~RandomTuner() {
+
 }
 
 void RandomTuner::tune() {
 	for (uint r = 0; r < budget; r++) {
 		model_print("Round %u of %u\n", r, budget);
-		for (uint i = 0; i < tuners.getSize(); i++){
+		for (uint i = 0; i < tuners.getSize(); i++) {
 			TunerRecord *tuner = tuners.get(i);
 			bool isNew = true;
-			for (uint j = 0; j < problems.getSize(); j++){
+			for (uint j = 0; j < problems.getSize(); j++) {
 				Problem *problem = problems.get(j);
 				long long metric = tuner->getTime(problem);
-				if(metric == -1){
+				if (metric == -1) {
 					metric = evaluate(problem, tuner);
 					ASSERT(tuner->getTime(problem) == -1);
 					tuner->addProblem(problem);
@@ -34,7 +34,7 @@ void RandomTuner::tune() {
 						tuner->setTime(problem, metric);
 					else
 						tuner->setTime(problem, -2);
-					if(tunerExists(tuner)){
+					if (tunerExists(tuner)) {
 						//Solving the problem and noticing the tuner
 						//already exists
 						isNew = false;
@@ -42,15 +42,15 @@ void RandomTuner::tune() {
 					}
 				}
 			}
-			if(isNew){
+			if (isNew) {
 				explored.push(tuner);
 			}
-			
+
 		}
 		uint tSize = tuners.getSize();
 		for (uint i = 0; i < tSize; i++) {
 			SearchTuner *tmpTuner = mutateTuner(tuners.get(i)->getTuner(), budget);
-			while(subTunerIndex(tmpTuner) != -1){
+			while (subTunerIndex(tmpTuner) != -1) {
 				tmpTuner->randomMutate();
 			}
 			TunerRecord *tmp = new TunerRecord(tmpTuner);
@@ -61,5 +61,5 @@ void RandomTuner::tune() {
 		}
 	}
 	printData();
-	
+
 }
diff --git a/src/Tuner/randomtuner.h b/src/Tuner/randomtuner.h
index 75b8800..47612da 100644
--- a/src/Tuner/randomtuner.h
+++ b/src/Tuner/randomtuner.h
@@ -6,7 +6,7 @@
 #include "basictuner.h"
 
 /**
- * This is a Tuner which is being used for 
+ * This is a Tuner which is being used for
  */
 class RandomTuner : public BasicTuner {
 public:
@@ -14,7 +14,7 @@ public:
 	virtual ~RandomTuner();
 	void tune();
 protected:
-        bool randomMutation(SearchTuner *tuner);        
+	bool randomMutation(SearchTuner *tuner);
 	TunerRecord *tune(SearchTuner *tuner);
 };
 
diff --git a/src/Tuner/satuner.cc b/src/Tuner/satuner.cc
index 0c405ae..2775081 100644
--- a/src/Tuner/satuner.cc
+++ b/src/Tuner/satuner.cc
@@ -12,28 +12,28 @@ SATuner::SATuner(uint _budget, uint _timeout) :
 {
 }
 
-SATuner::~SATuner(){
+SATuner::~SATuner() {
 
 }
 
-void SATuner::rankTunerForProblem(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric){
+void SATuner::rankTunerForProblem(Vector<TunerRecord *> *places, TunerRecord *tuner, Problem *problem, long long metric) {
 	uint k = 0;
 	for (; k < places->getSize(); k++) {
 		if (metric < places->get(k)->getTime(problem))
 			break;
 	}
 	model_print("Problem<%s>:place[%u]=Tuner<%p,%d>\n", problem->getProblem(), k, tuner, tuner->getTunerNumber());
-	places->insertAt(k, tuner);		
+	places->insertAt(k, tuner);
 }
 
-void SATuner::removeTunerIndex(Vector<TunerRecord *> *tunerV, int index,  Vector<Vector<TunerRecord *> *> &allplaces){
+void SATuner::removeTunerIndex(Vector<TunerRecord *> *tunerV, int index,  Vector<Vector<TunerRecord *> *> &allplaces) {
 	TunerRecord *tuner = tunerV->get(index);
 	model_print("Removing Tuner %d\n", tuner->getTunerNumber());
 	tunerV->set(index, NULL);
-	for(uint i=0; i < allplaces.getSize(); i++){
+	for (uint i = 0; i < allplaces.getSize(); i++) {
 		Vector<TunerRecord *> *places = allplaces.get(i);
-		for(uint j=0; j < places->getSize(); j++){
-			if(tuner == places->get(j)){
+		for (uint j = 0; j < places->getSize(); j++) {
+			if (tuner == places->get(j)) {
 				places->removeAt(j);
 				break;
 			}
@@ -42,32 +42,32 @@ void SATuner::removeTunerIndex(Vector<TunerRecord *> *tunerV, int index,  Vector
 
 }
 
-void SATuner::removeNullsFromTunerVector( Vector<TunerRecord *> *tunerV){
-	for (int i= tunerV->getSize() -1; i >= 0; i--){
-		if(tunerV->get(i) == NULL){
+void SATuner::removeNullsFromTunerVector( Vector<TunerRecord *> *tunerV) {
+	for (int i = tunerV->getSize() - 1; i >= 0; i--) {
+		if (tunerV->get(i) == NULL) {
 			tunerV->removeAt(i);
 		}
 	}
 	model_print("TunerV size after removing nulls = %u\n", tunerV->getSize());
 }
 
-void SATuner::initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecord *> *> &allplaces){
-	for(uint ii=0; ii< problems.getSize(); ii++){
+void SATuner::initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecord *> *> &allplaces) {
+	for (uint ii = 0; ii < problems.getSize(); ii++) {
 		allplaces.push(new Vector<TunerRecord *>());
 	}
-	for (uint j = 0; j< tunerV->getSize(); j++){
+	for (uint j = 0; j < tunerV->getSize(); j++) {
 		TunerRecord *tuner = tunerV->get(j);
-		for (uint i=0; i < problems.getSize(); i++){
+		for (uint i = 0; i < problems.getSize(); i++) {
 			Problem *problem = problems.get(i);
 			long long metric = evaluate(problem, tuner);
 			ASSERT(tuner->getTime(problem) == -1);
 			tuner->addProblem(problem);
-			if(metric != -1){
-				tuner->setTime(problem , metric);
-			}else{
-				tuner->setTime(problem , -2);
+			if (metric != -1) {
+				tuner->setTime(problem, metric);
+			} else {
+				tuner->setTime(problem, -2);
 			}
-			if(metric >=0){
+			if (metric >= 0) {
 				Vector<TunerRecord *> *places = allplaces.get(i);
 				rankTunerForProblem(places, tuner, problem, metric);
 			}
@@ -77,27 +77,27 @@ void SATuner::initialize(Vector<TunerRecord *> *tunerV, Vector<Vector<TunerRecor
 }
 
 void SATuner::tune() {
-	Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);	
+	Vector<TunerRecord *> *tunerV = new Vector<TunerRecord *>(&tuners);
 	Vector<Vector<TunerRecord *> *> allplaces;
 	uint tunerNumber = tuners.getSize();
 	//Initialization
 	initialize(tunerV, allplaces);
 	//Starting the body of algorithm
-	for (uint t = budget; t >0; t--) {
+	for (uint t = budget; t > 0; t--) {
 		model_print("Current Temperature = %u\n", t);
 		Hashtable<TunerRecord *, int, uint64_t> scores;
 		for (uint i = 0; i < tunerNumber; i++) {
-			SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), budget-t);
+			SearchTuner *tmpTuner = mutateTuner(tunerV->get(i)->getTuner(), budget - t);
 			int tunerIndex = subTunerIndex(tmpTuner);
 			TunerRecord *tmp = NULL;
-			if(tunerIndex == -1){
+			if (tunerIndex == -1) {
 				tmp = new TunerRecord(tmpTuner);
 				tmp->setTunerNumber(allTuners.getSize());
 				model_print("Mutated tuner %u to generate tuner %u\n", tunerV->get(i)->getTunerNumber(), tmp->getTunerNumber());
-				allTuners.push(tmp);	
-			}else{
+				allTuners.push(tmp);
+			} else {
 				//Previous tuners might get explored with new combination of tuners.
-				tmp = explored.get(tunerIndex);	
+				tmp = explored.get(tunerIndex);
 				model_print("Using exploread tuner <%u>\n", tmp->getTunerNumber());
 			}
 			tunerV->push(tmp);
@@ -129,11 +129,11 @@ void SATuner::tune() {
 				}
 			}
 		}
-		for(uint ii=0; ii < problems.getSize(); ii++){
+		for (uint ii = 0; ii < problems.getSize(); ii++) {
 			Problem *problem = problems.get(ii);
 			ASSERT(ii < allplaces.getSize());
 			Vector<TunerRecord *> *places = allplaces.get(ii);
-			int points = pow(tunerNumber*1.0, 2*tunerNumber - 1);
+			int points = pow(tunerNumber * 1.0, 2 * tunerNumber - 1);
 			for (uint k = 0; k < places->getSize() && points; k++) {
 				TunerRecord *tuner = places->get(k);
 				int currScore = 0;
@@ -147,7 +147,7 @@ void SATuner::tune() {
 			}
 		}
 
-		for(uint i= 0; i < tunerNumber; i++){
+		for (uint i = 0; i < tunerNumber; i++) {
 			ASSERT(i < tunerV->getSize());
 			TunerRecord *tuner1 = tunerV->get(i);
 			TunerRecord *tuner2 = tunerV->get(tunerNumber + i);
@@ -168,26 +168,26 @@ void SATuner::tune() {
 			
 			if( score2 > score1 ){
 				removeTunerIndex(tunerV, i, allplaces);
-			} else if( score2 < score1){
-				model_print("score1=%d\tscore2=%d\tt=%u\texp=%f\n", score1, score2, t, exp((score1-score2)*1.0/t));
-				double prob = 1/(exp((score1-score2)*1.0/t) );
+			} else if ( score2 < score1) {
+				model_print("score1=%d\tscore2=%d\tt=%u\texp=%f\n", score1, score2, t, exp((score1 - score2) * 1.0 / t));
+				double prob = 1 / (exp((score1 - score2) * 1.0 / t) );
 				double random = ((double) rand() / (RAND_MAX));
 				model_print("prob=%f\trandom=%f\n", prob, random);
-				if(prob > random){
+				if (prob > random) {
 					removeTunerIndex(tunerV, i, allplaces);
-				}else{
+				} else {
 					removeTunerIndex(tunerV, tunerNumber + i, allplaces);
 				}
-			} else{
+			} else {
 				double random = ((double) rand() / (RAND_MAX));
-				int index = random > 0.5? i : tunerNumber + i;
+				int index = random > 0.5 ? i : tunerNumber + i;
 				removeTunerIndex(tunerV, index, allplaces);
 			}
 		}
 		removeNullsFromTunerVector(tunerV);
-		
+
 	}
-	for(uint ii=0; ii< allplaces.getSize(); ii++){
+	for (uint ii = 0; ii < allplaces.getSize(); ii++) {
 		delete allplaces.get(ii);
 	}
 	printData();
diff --git a/src/Tuner/satuner.h b/src/Tuner/satuner.h
index fd05423..34ed7ae 100644
--- a/src/Tuner/satuner.h
+++ b/src/Tuner/satuner.h
@@ -5,9 +5,9 @@
 #include "basictuner.h"
 
 /**
-*This tuner has the simulated annealing in its core
-*
-*/
+ * This tuner has the simulated annealing in its core
+ *
+ */
 class SATuner : public BasicTuner {
 public:
 	SATuner(uint budget, uint timeout);
diff --git a/src/Tuner/searchtuner.cc b/src/Tuner/searchtuner.cc
index a600580..9ab6d45 100644
--- a/src/Tuner/searchtuner.cc
+++ b/src/Tuner/searchtuner.cc
@@ -86,7 +86,7 @@ SearchTuner::SearchTuner(const char *filename, bool addused) {
 			}
 			setting->setDecision(lowValue, highValue, defaultValue, selectedValue);
 			settings.add(setting);
-			if(addused){
+			if (addused) {
 				usedSettings.add(setting);
 			}
 		}
@@ -96,20 +96,20 @@ SearchTuner::SearchTuner(const char *filename, bool addused) {
 	}
 }
 
-bool SearchTuner::equalUsed(SearchTuner* tuner){
-	if(tuner->usedSettings.getSize() != usedSettings.getSize()){
+bool SearchTuner::equalUsed(SearchTuner *tuner) {
+	if (tuner->usedSettings.getSize() != usedSettings.getSize()) {
 		return false;
 	}
 	bool result = true;
 	SetIteratorTunableSetting *iterator = usedSettings.iterator();
-	while(iterator->hasNext()){
+	while (iterator->hasNext()) {
 		TunableSetting *setting = iterator->next();
-		if(!tuner->usedSettings.contains(setting)){
+		if (!tuner->usedSettings.contains(setting)) {
 			result = false;
 			break;
-		}else{
+		} else {
 			TunableSetting *tunerSetting = tuner->usedSettings.get(setting);
-			if(tunerSetting->selectedValue != setting->selectedValue){
+			if (tunerSetting->selectedValue != setting->selectedValue) {
 				result = false;
 				break;
 			}
@@ -156,15 +156,15 @@ void SearchTuner::addUsed(const char *filename) {
 	}
 }
 
-bool SearchTuner::isSubTunerof(SearchTuner *newTuner){
+bool SearchTuner::isSubTunerof(SearchTuner *newTuner) {
 	SetIteratorTunableSetting *iterator = usedSettings.iterator();
 	while (iterator->hasNext()) {
 		TunableSetting *setting = iterator->next();
-		if(!newTuner->settings.contains(setting)){
+		if (!newTuner->settings.contains(setting)) {
 			return false;
-		} else{
+		} else {
 			TunableSetting *newSetting = newTuner->settings.get(setting);
-			if(newSetting->selectedValue != setting->selectedValue){
+			if (newSetting->selectedValue != setting->selectedValue) {
 				return false;
 			}
 		}
diff --git a/src/Tuner/searchtuner.h b/src/Tuner/searchtuner.h
index 935f527..9d5913b 100644
--- a/src/Tuner/searchtuner.h
+++ b/src/Tuner/searchtuner.h
@@ -43,7 +43,7 @@ public:
 	void setVarTunable(VarType vartype, TunableParam param, TunableDesc *descriptor, uint value);
 	void setVarTunable(VarType vartype1, VarType vartype2, TunableParam param, TunableDesc *descriptor, uint value);
 	SearchTuner *copyUsed();
-        bool isSubTunerof(SearchTuner *newTuner);
+	bool isSubTunerof(SearchTuner *newTuner);
 	void randomMutate();
 	uint getSize() { return usedSettings.getSize();}
 	void print();
@@ -51,7 +51,7 @@ public:
 	void serialize(const char *file);
 	void serializeUsed(const char *file);
 	void addUsed(const char *file);
-        bool equalUsed(SearchTuner *tuner);
+	bool equalUsed(SearchTuner *tuner);
 	CMEMALLOC;
 protected:
 	/** Used Settings keeps track of settings that were actually used by
diff --git a/src/Tuner/tunabledependent.cc b/src/Tuner/tunabledependent.cc
index e1b0dba..7c5d49a 100644
--- a/src/Tuner/tunabledependent.cc
+++ b/src/Tuner/tunabledependent.cc
@@ -4,16 +4,16 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   TunableDependent.cc
  * Author: hamed
- * 
+ *
  * Created on October 5, 2018, 11:26 AM
  */
 
 #include "tunabledependent.h"
 
-TunableDependent::TunableDependent(Tunables dependent, Tunables parent):
+TunableDependent::TunableDependent(Tunables dependent, Tunables parent) :
 	dependent(dependent),
 	parent(parent)
 {
diff --git a/src/Tuner/tunabledependent.h b/src/Tuner/tunabledependent.h
index 241b9eb..0874316 100644
--- a/src/Tuner/tunabledependent.h
+++ b/src/Tuner/tunabledependent.h
@@ -4,7 +4,7 @@
  * and open the template in the editor.
  */
 
-/* 
+/*
  * File:   TunableDependent.h
  * Author: hamed
  *
@@ -18,12 +18,12 @@
 
 class TunableDependent {
 public:
-        TunableDependent(Tunables dependent, Tunables parent = (Tunables) -1);
-        TunableDependent(TunableDependent &setting);
-        virtual ~TunableDependent();
-        Tunables dependent;
-        Tunables parent;
+	TunableDependent(Tunables dependent, Tunables parent = (Tunables) - 1);
+	TunableDependent(TunableDependent &setting);
+	virtual ~TunableDependent();
+	Tunables dependent;
+	Tunables parent;
 };
 
-#endif /* TUNABLEDEPENDENT_H */
+#endif/* TUNABLEDEPENDENT_H */
 
diff --git a/src/ccsolver.cc b/src/ccsolver.cc
index 05f66a3..d773522 100644
--- a/src/ccsolver.cc
+++ b/src/ccsolver.cc
@@ -54,11 +54,11 @@ void *getBooleanVar(void *solver,unsigned int type) {
 	return CCSOLVER(solver)->getBooleanVar((VarType) type).getRaw();
 }
 
-void *getBooleanTrue(void *solver){
+void *getBooleanTrue(void *solver) {
 	return CCSOLVER(solver)->getBooleanTrue().getRaw();
 }
 
-void *getBooleanFalse(void *solver){
+void *getBooleanFalse(void *solver) {
 	return CCSOLVER(solver)->getBooleanFalse().getRaw();
 }
 
@@ -160,7 +160,7 @@ void mustHaveValue(void *solver, void *element) {
 	CCSOLVER(solver)->mustHaveValue( (Element *) element);
 }
 
-void setInterpreter(void *solver, unsigned int type){
+void setInterpreter(void *solver, unsigned int type) {
 	CCSOLVER(solver)->setInterpreter((InterpreterType)type);
 }
 
diff --git a/src/csolver.cc b/src/csolver.cc
index cd2ec55..1dfe9eb 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -85,8 +85,8 @@ CSolver::~CSolver() {
 	for (uint i = 0; i < size; i++) {
 		delete allFunctions.get(i);
 	}
-	
-	if(interpreter != NULL){
+
+	if (interpreter != NULL) {
 		delete interpreter;
 	}
 
@@ -319,7 +319,7 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
 BooleanEdge CSolver::getBooleanVar(VarType type) {
 	Boolean *boolean = new BooleanVar(type);
 	allBooleans.push(boolean);
-	if(!booleanVarUsed)
+	if (!booleanVarUsed)
 		booleanVarUsed = true;
 	return BooleanEdge(boolean);
 }
@@ -397,7 +397,7 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
-	if(!useInterpreter()){
+	if (!useInterpreter()) {
 		BooleanEdge newarray[asize];
 		switch (op) {
 		case SATC_NOT: {
@@ -460,7 +460,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 			return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
 		}
 		}
-	
+
 		ASSERT(asize != 0);
 		Boolean *boolean = new BooleanLogic(this, op, array, asize);
 		Boolean *b = boolMap.get(boolean);
@@ -478,7 +478,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint
 		Boolean *boolean = new BooleanLogic(this, op, array, asize);
 		allBooleans.push(boolean);
 		return BooleanEdge(boolean);
-	
+
 	}
 }
 
@@ -497,7 +497,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 		}
 	}
 	Boolean *constraint = new BooleanOrder(order, first, second);
-	if (!useInterpreter() ){ 
+	if (!useInterpreter() ) {
 		Boolean *b = boolMap.get(constraint);
 
 		if (b == NULL) {
@@ -534,7 +534,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 }
 
 void CSolver::addConstraint(BooleanEdge constraint) {
-	if(!useInterpreter()){
+	if (!useInterpreter()) {
 		if (isTrue(constraint))
 			return;
 		else if (isFalse(constraint)) {
@@ -572,7 +572,7 @@ void CSolver::addConstraint(BooleanEdge constraint) {
 			replaceBooleanWithTrueNoRemove(constraint);
 			constraint->parents.clear();
 		}
-	} else{
+	} else {
 		constraints.add(constraint);
 		constraint->parents.clear();
 	}
@@ -605,7 +605,7 @@ void CSolver::inferFixedOrders() {
 }
 
 int CSolver::solve() {
-	if(isUnSAT()){
+	if (isUnSAT()) {
 		return IS_UNSAT;
 	}
 	long long startTime = getTimeNano();
@@ -615,12 +615,12 @@ int CSolver::solve() {
 		deleteTuner = true;
 	}
 	int result = IS_INDETER;
-	if(useInterpreter()){
+	if (useInterpreter()) {
 		interpreter->encode();
 		model_print("Problem encoded in Interpreter\n");
 		result = interpreter->solve();
 		model_print("Problem solved by Interpreter\n");
-	} else{
+	} else {
 
 		{
 			SetIteratorOrder *orderit = activeOrders.iterator();
@@ -656,21 +656,21 @@ int CSolver::solve() {
 		eg.encode();
 
 		naiveEncodingDecision(this);
-	//	eg.validate();
+		//	eg.validate();
 
 		VarOrderingOpt bor(this, satEncoder);
 		bor.doTransform();
 
 		time2 = getTimeNano();
 		model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
-		
+
 		satEncoder->encodeAllSATEncoder(this);
 		time1 = getTimeNano();
 
 		model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
 
 		model_print("Is problem UNSAT after encoding: %d\n", unsat);
-		
+
 
 		result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
 		model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
@@ -685,28 +685,28 @@ int CSolver::solve() {
 	return result;
 }
 
-void CSolver::setInterpreter(InterpreterType type){
-	if(interpreter == NULL){
-		switch(type){
-			case SATUNE:
-				break;
-			case ALLOY:{
-				interpreter = new AlloyInterpreter(this);
-				break;
-			}case Z3:{
-				interpreter = new SMTInterpreter(this);
-				break;
-			}
-			case MATHSAT:{
-				interpreter = new MathSATInterpreter(this);
-				break;
-			}
-			case SMTRAT:{
-				interpreter = new SMTRatInterpreter(this);
-				break;
-			}
-			default:
-				ASSERT(0);
+void CSolver::setInterpreter(InterpreterType type) {
+	if (interpreter == NULL) {
+		switch (type) {
+		case SATUNE:
+			break;
+		case ALLOY: {
+			interpreter = new AlloyInterpreter(this);
+			break;
+		} case Z3: {
+			interpreter = new SMTInterpreter(this);
+			break;
+		}
+		case MATHSAT: {
+			interpreter = new MathSATInterpreter(this);
+			break;
+		}
+		case SMTRAT: {
+			interpreter = new SMTRatInterpreter(this);
+			break;
+		}
+		default:
+			ASSERT(0);
 		}
 	}
 }
@@ -729,8 +729,8 @@ uint64_t CSolver::getElementValue(Element *element) {
 	case ELEMSET:
 	case ELEMCONST:
 	case ELEMFUNCRETURN:
-		return useInterpreter()? interpreter->getValue(element):
-			getElementValueSATTranslator(this, element);
+		return useInterpreter() ? interpreter->getValue(element) :
+					 getElementValueSATTranslator(this, element);
 	default:
 		ASSERT(0);
 	}
@@ -741,8 +741,8 @@ bool CSolver::getBooleanValue(BooleanEdge bedge) {
 	Boolean *boolean = bedge.getBoolean();
 	switch (boolean->type) {
 	case BOOLEANVAR:
-		return useInterpreter()? interpreter->getBooleanValue(boolean):
-			getBooleanVariableValueSATTranslator(this, boolean);
+		return useInterpreter() ? interpreter->getBooleanValue(boolean) :
+					 getBooleanVariableValueSATTranslator(this, boolean);
 	default:
 		ASSERT(0);
 	}
diff --git a/src/csolver.h b/src/csolver.h
index 54012de..b99cf80 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -126,7 +126,7 @@ public:
 
 	/** When everything is done, the client calls this function and then csolver starts to encode*/
 	int solve();
-	
+
 	/** After getting the solution from the SAT solver, client can get the value of an element via this function*/
 	uint64_t getElementValue(Element *element);
 
@@ -141,7 +141,7 @@ public:
 	void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; }
 	void setSatSolverTimeout(long seconds) { satsolverTimeout = seconds;}
 	bool isUnSAT() { return unsat; }
-        bool isBooleanVarUsed(){return booleanVarUsed;}
+	bool isBooleanVarUsed() {return booleanVarUsed;}
 	void printConstraint(BooleanEdge boolean);
 	void printConstraints();
 
@@ -219,8 +219,8 @@ private:
 
 	SATEncoder *satEncoder;
 	bool unsat;
-        bool booleanVarUsed;
-        Tuner *tuner;
+	bool booleanVarUsed;
+	Tuner *tuner;
 	long long elapsedTime;
 	long satsolverTimeout;
 	Interpreter *interpreter;
diff --git a/src/satune_SatuneJavaAPI.h b/src/satune_SatuneJavaAPI.h
index bde12a6..db22513 100644
--- a/src/satune_SatuneJavaAPI.h
+++ b/src/satune_SatuneJavaAPI.h
@@ -13,7 +13,7 @@ extern "C" {
  * Signature: ()J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createCCSolver
-  (JNIEnv *, jobject);
+	(JNIEnv *, jobject);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -21,7 +21,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createCCSolver
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_deleteCCSolver
-  (JNIEnv *, jobject, jlong);
+	(JNIEnv *, jobject, jlong);
 
 
 /*
@@ -30,7 +30,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_deleteCCSolver
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_resetCCSolver
-  (JNIEnv *, jobject, jlong);
+	(JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -38,7 +38,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_resetCCSolver
  * Signature: (JIJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createSet
-  (JNIEnv *, jobject, jlong, jint, jlong, jint);
+	(JNIEnv *, jobject, jlong, jint, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -46,7 +46,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createSet
  * Signature: (JIJJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeSet
-  (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jint, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -54,7 +54,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeSet
  * Signature: (JIJJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeVar
-  (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jint, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -62,7 +62,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeVar
  * Signature: (JI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createMutableSet
-  (JNIEnv *, jobject, jlong, jint);
+	(JNIEnv *, jobject, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -70,7 +70,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createMutableSet
  * Signature: (JJJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addItem
-  (JNIEnv *, jobject, jlong, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -78,7 +78,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addItem
  * Signature: (JJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_finalizeMutableSet
-  (JNIEnv *, jobject, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -86,7 +86,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_finalizeMutableSet
  * Signature: (JJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementVar
-  (JNIEnv *, jobject, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -94,7 +94,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementVar
  * Signature: (JIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementConst
-  (JNIEnv *, jobject, jlong, jint, jlong);
+	(JNIEnv *, jobject, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -102,7 +102,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementConst
  * Signature: (JJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementRange
-  (JNIEnv *, jobject, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -110,7 +110,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementRange
  * Signature: (JI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanVar
-  (JNIEnv *, jobject, jlong, jint);
+	(JNIEnv *, jobject, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -118,7 +118,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanVar
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue
-  (JNIEnv *, jobject, jlong);
+	(JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -126,7 +126,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanFalse
-  (JNIEnv *, jobject, jlong);
+	(JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -134,7 +134,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanFalse
  * Signature: (JIJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createFunctionOperator
-  (JNIEnv *, jobject, jlong, jint, jlong, jint);
+	(JNIEnv *, jobject, jlong, jint, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -142,7 +142,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createFunctionOperator
  * Signature: (JI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateOperator
-  (JNIEnv *, jobject, jlong, jint);
+	(JNIEnv *, jobject, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -150,7 +150,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateOperator
  * Signature: (JJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateTable
-  (JNIEnv *, jobject, jlong, jlong, jint);
+	(JNIEnv *, jobject, jlong, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -158,7 +158,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateTable
  * Signature: (JJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTable
-  (JNIEnv *, jobject, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -166,7 +166,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTable
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTableForPredicate
-  (JNIEnv *, jobject, jlong);
+	(JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -174,7 +174,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTableForPredicate
  * Signature: (JJJIJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addTableEntry
-  (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+	(JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -182,7 +182,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addTableEntry
  * Signature: (JJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_completeTable
-  (JNIEnv *, jobject, jlong, jlong, jint);
+	(JNIEnv *, jobject, jlong, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -190,7 +190,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_completeTable
  * Signature: (JJJIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyFunction
-  (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+	(JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -198,7 +198,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyFunction
  * Signature: (JJJIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicateTable
-  (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+	(JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -206,7 +206,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicateTable
  * Signature: (JJJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicate
-  (JNIEnv *, jobject, jlong, jlong, jlong, jint);
+	(JNIEnv *, jobject, jlong, jlong, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -214,7 +214,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicate
  * Signature: (JIJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperation
-  (JNIEnv *, jobject, jlong, jint, jlong, jint);
+	(JNIEnv *, jobject, jlong, jint, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -222,7 +222,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperation
  * Signature: (JIJJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationTwo
-  (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jint, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -230,7 +230,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationTwo
  * Signature: (JIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationOne
-  (JNIEnv *, jobject, jlong, jint, jlong);
+	(JNIEnv *, jobject, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -238,7 +238,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationOne
  * Signature: (JJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addConstraint
-  (JNIEnv *, jobject, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -246,7 +246,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addConstraint
  * Signature: (JJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraint
-  (JNIEnv *, jobject, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -254,7 +254,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraint
  * Signature: (JIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createOrder
-  (JNIEnv *, jobject, jlong, jint, jlong);
+	(JNIEnv *, jobject, jlong, jint, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -262,7 +262,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createOrder
  * Signature: (JJJJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_orderConstraint
-  (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -270,7 +270,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_orderConstraint
  * Signature: (J)I
  */
 JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solve
-  (JNIEnv *, jobject, jlong);
+	(JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -278,7 +278,7 @@ JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solve
  * Signature: (JJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementValue
-  (JNIEnv *, jobject, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -286,7 +286,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementValue
  * Signature: (JJ)I
  */
 JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getBooleanValue
-  (JNIEnv *, jobject, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -294,7 +294,7 @@ JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getBooleanValue
  * Signature: (JJJJ)I
  */
 JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getOrderConstraintValue
-  (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -302,7 +302,7 @@ JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getOrderConstraintValue
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
-  (JNIEnv *, jobject, jlong);
+	(JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -310,7 +310,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_serialize
-  (JNIEnv *, jobject, jlong);
+	(JNIEnv *, jobject, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -318,7 +318,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_serialize
  * Signature: (JJ)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_mustHaveValue
-  (JNIEnv *, jobject, jlong, jlong);
+	(JNIEnv *, jobject, jlong, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -326,7 +326,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_mustHaveValue
  * Signature: (JI)V
  */
 JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_setInterpreter
-  (JNIEnv *, jobject, jlong, jint);
+	(JNIEnv *, jobject, jlong, jint);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -334,7 +334,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_setInterpreter
  * Signature: (J)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_clone
-  (JNIEnv *, jobject, jlong);
+	(JNIEnv *, jobject, jlong);
 
 #ifdef __cplusplus
 }