From: bdemsky <bdemsky@uci.edu>
Date: Fri, 17 Aug 2018 22:49:29 +0000 (-0700)
Subject: Fix tabbing
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=19c299fd9e91386883e788f445d153abfe58430a

Fix tabbing
---

diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index de96bfc..77dc244 100644
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -12,7 +12,7 @@
 
 class Boolean : public ASTNode {
 private:
-    static uint64_t counter;
+	static uint64_t counter;
 public:
 	Boolean(ASTNodeType _type);
 	virtual ~Boolean() {}
@@ -25,7 +25,7 @@ public:
 	BooleanValue boolVal;
 	Vector<ASTNode *> parents;
 	virtual void updateParents() {}
-        uint64_t id;
+	uint64_t id;
 	CMEMALLOC;
 };
 
diff --git a/src/AST/order.cc b/src/AST/order.cc
index 2b3184a..315b112 100644
--- a/src/AST/order.cc
+++ b/src/AST/order.cc
@@ -33,7 +33,7 @@ Order *Order::clone(CSolver *solver, CloneMap *map) {
 
 HashtableOrderPair *Order::getOrderPairTable() {
 	ASSERT( encoding.resolver != NULL);
-	if (OrderPairResolver * t = dynamic_cast<OrderPairResolver *>(encoding.resolver)) {
+	if (OrderPairResolver *t = dynamic_cast<OrderPairResolver *>(encoding.resolver)) {
 		return t->getOrderPairTable();
 	} else {
 		ASSERT(0);
diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index 58ef96b..b5127c6 100644
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -51,7 +51,7 @@ void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
 	}
 }
 
-void CSolver::handleFunction(ElementFunction * ef, BooleanEdge child) {
+void CSolver::handleFunction(ElementFunction *ef, BooleanEdge child) {
 	BooleanEdge childNegate = child.negate();
 	elemMap.remove(ef);
 	if (ef->overflowstatus == child) {
@@ -106,7 +106,7 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
 		} else {
 			BooleanLogic *logicop = (BooleanLogic *) parent;
 			boolMap.remove(logicop);	//could change parent's hash
-			
+
 			uint parentsize = logicop->inputs.getSize();
 			for (uint j = 0; j < parentsize; j++) {
 				BooleanEdge b = logicop->inputs.get(j);
diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 45ae01a..2a741ae 100644
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -79,8 +79,8 @@ void EncodingGraph::encode() {
 					EncodingSubGraph *subgraph = graphMap.get(n);
 					DEBUG("graphMap.get(subgraph=%p, n=%p)\n", subgraph, n);
 					if (subgraph == NULL) {
-					  encoding->encodingArrayInitialization();
-					  continue;
+						encoding->encodingArrayInitialization();
+						continue;
 					}
 					uint encodingSize = subgraph->getEncodingMaxVal(n) + 1;
 					uint paddedSize = encoding->getSizeEncodingArray(encodingSize);
@@ -255,9 +255,9 @@ void EncodingGraph::decideEdges() {
 			return;
 
 		EncodingSubGraph *leftGraph = graphMap.get(left);
-                DEBUG("graphMap.get(left=%p, leftgraph=%p)\n", left, leftGraph);
+		DEBUG("graphMap.get(left=%p, leftgraph=%p)\n", left, leftGraph);
 		EncodingSubGraph *rightGraph = graphMap.get(right);
-                DEBUG("graphMap.get(right=%p, rightgraph=%p)\n", right, rightGraph);
+		DEBUG("graphMap.get(right=%p, rightgraph=%p)\n", right, rightGraph);
 		if (leftGraph == NULL && rightGraph != NULL) {
 			EncodingNode *tmp = left; left = right; right = tmp;
 			EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
diff --git a/src/ASTAnalyses/Polarity/polarityassignment.cc b/src/ASTAnalyses/Polarity/polarityassignment.cc
index f941227..4a772ee 100644
--- a/src/ASTAnalyses/Polarity/polarityassignment.cc
+++ b/src/ASTAnalyses/Polarity/polarityassignment.cc
@@ -24,7 +24,7 @@ void updateEdgePolarity(BooleanEdge dst, Polarity p) {
 	Boolean *bdst = dst.getBoolean();
 	bool isNegated = dst.isNegated();
 	if (isNegated)
-		p=negatePolarity(p);
+		p = negatePolarity(p);
 	updatePolarity(bdst, p);
 }
 
@@ -60,8 +60,8 @@ void computePredicatePolarity(BooleanPredicate *This) {
 	if (This->undefStatus) {
 		computePolarity(This->undefStatus.getBoolean(), P_BOTHTRUEFALSE);
 	}
-	for(uint i=0; i < This->inputs.getSize(); i++) {
-		Element * e = This->inputs.get(i);
+	for (uint i = 0; i < This->inputs.getSize(); i++) {
+		Element *e = This->inputs.get(i);
 		computeElement(e);
 	}
 }
@@ -74,10 +74,10 @@ void computeElement(Element *e) {
 			computePolarity(ef->overflowstatus.getBoolean(), P_BOTHTRUEFALSE);
 		}
 
-		for(uint i=0; i < ef->inputs.getSize(); i++) {
-			Element * echild = ef->inputs.get(i);
+		for (uint i = 0; i < ef->inputs.getSize(); i++) {
+			Element *echild = ef->inputs.get(i);
 			computeElement(echild);
-		}	
+		}
 	}
 }
 
diff --git a/src/ASTTransform/elementopt.cc b/src/ASTTransform/elementopt.cc
old mode 100755
new mode 100644
index 3f1f892..6fec155
--- a/src/ASTTransform/elementopt.cc
+++ b/src/ASTTransform/elementopt.cc
@@ -9,7 +9,7 @@
 
 ElementOpt::ElementOpt(CSolver *_solver)
 	: Transform(_solver),
-		updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
+	updateSets(solver->getTuner()->getTunable(ELEMENTOPTSETS, &onoff) == 1)
 {
 }
 
@@ -19,7 +19,7 @@ ElementOpt::~ElementOpt() {
 void ElementOpt::doTransform() {
 	if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
 		return;
-	
+
 	SetIteratorBooleanEdge *iterator = solver->getConstraints();
 	while (iterator->hasNext()) {
 		BooleanEdge constraint = iterator->next();
@@ -27,38 +27,38 @@ void ElementOpt::doTransform() {
 			workList.push((BooleanPredicate *)constraint.getBoolean());
 	}
 	while (workList.getSize() != 0) {
-		BooleanPredicate * pred = workList.last(); workList.pop();
+		BooleanPredicate *pred = workList.last(); workList.pop();
 		processPredicate(pred);
 	}
 	delete iterator;
 }
 
-void ElementOpt::processPredicate(BooleanPredicate * pred) {
+void ElementOpt::processPredicate(BooleanPredicate *pred) {
 	uint numInputs = pred->inputs.getSize();
 	if (numInputs != 2)
 		return;
 
-	Predicate * p = pred->getPredicate();
+	Predicate *p = pred->getPredicate();
 	if (p->type == TABLEPRED)
-			return;
+		return;
 
-	PredicateOperator * pop = (PredicateOperator *) p;
+	PredicateOperator *pop = (PredicateOperator *) p;
 	CompOp op = pop->getOp();
 
-	Element * left = pred->inputs.get(0);
-	Element * right = pred->inputs.get(1);
+	Element *left = pred->inputs.get(0);
+	Element *right = pred->inputs.get(1);
 
 	if (left->type == ELEMCONST) {
-		Element * tmp = left;
+		Element *tmp = left;
 		left = right;
 		right = tmp;
 		op = flipOp(op);
 	} else if (right->type != ELEMCONST)
 		return;
 
-	if (left->type !=ELEMSET)
+	if (left->type != ELEMSET)
 		return;
-	
+
 	if (op == SATC_EQUALS) {
 		handlePredicateEquals(pred, (ElementSet *) left, (ElementConst *) right);
 	} else if (updateSets) {
@@ -75,8 +75,8 @@ void ElementOpt::handlePredicateEquals(BooleanPredicate *pred, ElementSet *left,
 }
 
 void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
-	Predicate * p = pred->getPredicate();
-	PredicateOperator * pop = (PredicateOperator *) p;
+	Predicate *p = pred->getPredicate();
+	PredicateOperator *pop = (PredicateOperator *) p;
 	CompOp op = pop->getOp();
 
 	if (pred->isFalse()) {
@@ -85,18 +85,18 @@ void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *v
 		ASSERT(0);
 	}
 
-	Set * s = var->getRange();
+	Set *s = var->getRange();
 	if (s->isRange)
 		return;
-	
+
 	uint size = s->getSize();
 	uint64_t elemArray[size];
 	uint count = 0;
 	uint64_t cvalue = value->value;
 
-	switch(op) {
+	switch (op) {
 	case SATC_LT: {
-		for(uint i=0; i<size; i++) {
+		for (uint i = 0; i < size; i++) {
 			uint64_t val = s->getElement(i);
 			if (val < cvalue)
 				elemArray[count++] = val;
@@ -104,7 +104,7 @@ void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *v
 		break;
 	}
 	case SATC_GT: {
-		for(uint i=0; i<size; i++) {
+		for (uint i = 0; i < size; i++) {
 			uint64_t val = s->getElement(i);
 			if (val > cvalue)
 				elemArray[count++] = val;
@@ -112,7 +112,7 @@ void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *v
 		break;
 	}
 	case SATC_LTE: {
-		for(uint i=0; i<size; i++) {
+		for (uint i = 0; i < size; i++) {
 			uint64_t val = s->getElement(i);
 			if (val <= cvalue)
 				elemArray[count++] = val;
@@ -120,40 +120,40 @@ void ElementOpt::handlePredicateInequality(BooleanPredicate *pred, ElementSet *v
 		break;
 	}
 	case SATC_GTE: {
-		for(uint i=0; i<size; i++) {
+		for (uint i = 0; i < size; i++) {
 			uint64_t val = s->getElement(i);
 			if (val >= cvalue)
 				elemArray[count++] = val;
 		}
 		break;
 	}
-		
+
 	default:
 		ASSERT(0);
 	}
 	if (size == count)
 		return;
-	
+
 	Set *newset = solver->createSet(s->type, elemArray, count);
 	solver->elemMap.remove(var);
 	var->set = newset;
 	solver->elemMap.put(var, var);
 
 	if (count == 1) {
-		ElementConst * elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
+		ElementConst *elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
 		replaceVarWithConst(pred, var, elemconst);
 	}
 }
 
 void ElementOpt::constrainVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
-	Set * s = var->getRange();
+	Set *s = var->getRange();
 	if (s->isRange)
 		return;
 	uint size = s->getSize();
 	uint64_t elemArray[size];
 	uint count = 0;
 	uint64_t cvalue = value->value;
-	for(uint i=0; i<size; i++) {
+	for (uint i = 0; i < size; i++) {
 		uint64_t val = s->getElement(i);
 		if (val != cvalue)
 			elemArray[count++] = val;
@@ -167,19 +167,19 @@ void ElementOpt::constrainVarWithConst(BooleanPredicate *pred, ElementSet *var,
 	solver->elemMap.put(var, var);
 
 	if (count == 1) {
-		ElementConst * elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
+		ElementConst *elemconst = (ElementConst *) solver->getElementConst(s->type, elemArray[0]);
 		replaceVarWithConst(pred, var, elemconst);
 	}
 }
 
-void ElementOpt::replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value) {
+void ElementOpt::replaceVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value) {
 	uint size = var->parents.getSize();
-	for(uint i=0; i < size; i++) {
-		ASTNode * parent = var->parents.get(i);
+	for (uint i = 0; i < size; i++) {
+		ASTNode *parent = var->parents.get(i);
 		if (parent->type == PREDICATEOP && pred != parent) {
-			BooleanPredicate * newpred = (BooleanPredicate *) parent;
-			for(uint j=0; j < newpred->inputs.getSize(); j++) {
-				Element * e = newpred->inputs.get(j);
+			BooleanPredicate *newpred = (BooleanPredicate *) parent;
+			for (uint j = 0; j < newpred->inputs.getSize(); j++) {
+				Element *e = newpred->inputs.get(j);
 				if (e == var) {
 					solver->boolMap.remove(newpred);
 					newpred->inputs.set(j, value);
diff --git a/src/ASTTransform/elementopt.h b/src/ASTTransform/elementopt.h
old mode 100755
new mode 100644
index a1f6005..c1b7390
--- a/src/ASTTransform/elementopt.h
+++ b/src/ASTTransform/elementopt.h
@@ -14,7 +14,7 @@ private:
 	void processPredicate(BooleanPredicate *);
 	void handlePredicateEquals(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
 	void handlePredicateInequality(BooleanPredicate *pred, ElementSet *left, ElementConst *right);
-	void replaceVarWithConst(BooleanPredicate * pred, ElementSet *var, ElementConst * value);
+	void replaceVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value);
 	void constrainVarWithConst(BooleanPredicate *pred, ElementSet *var, ElementConst *value);
 
 	Vector<BooleanPredicate *> workList;
diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
index 37a3db4..3022060 100644
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -69,11 +69,11 @@ Node *allocResizeNode(uint capacity) {
 Edge cloneEdge(Edge e) {
 	if (edgeIsVarConst(e))
 		return e;
-	Node * node = getNodePtrFromEdge(e);
+	Node *node = getNodePtrFromEdge(e);
 	bool isneg = isNegEdge(e);
 	uint numEdges = node->numEdges;
-	Node * clone = allocBaseNode(node->type, numEdges);
-	for(uint i=0; i < numEdges; i++) {
+	Node *clone = allocBaseNode(node->type, numEdges);
+	for (uint i = 0; i < numEdges; i++) {
 		clone->edges[i] = cloneEdge(node->edges[i]);
 	}
 	return isneg ? constraintNegate((Edge) {clone}) : (Edge) {clone};
@@ -82,9 +82,9 @@ Edge cloneEdge(Edge e) {
 void freeEdgeRec(Edge e) {
 	if (edgeIsVarConst(e))
 		return;
-	Node * node = getNodePtrFromEdge(e);
+	Node *node = getNodePtrFromEdge(e);
 	uint numEdges = node->numEdges;
-	for(uint i=0; i < numEdges; i++) {
+	for (uint i = 0; i < numEdges; i++) {
 		freeEdgeRec(node->edges[i]);
 	}
 	ourfree(node);
@@ -93,21 +93,21 @@ void freeEdgeRec(Edge e) {
 void freeEdge(Edge e) {
 	if (edgeIsVarConst(e))
 		return;
-	Node * node = getNodePtrFromEdge(e);
+	Node *node = getNodePtrFromEdge(e);
 	ourfree(node);
 }
 
-void freeEdgesRec(uint numEdges, Edge * earray) {
-	for(uint i=0; i < numEdges; i++) {
+void freeEdgesRec(uint numEdges, Edge *earray) {
+	for (uint i = 0; i < numEdges; i++) {
 		Edge e = earray[i];
 		freeEdgeRec(e);
 	}
 }
 
 void freeEdgeCNF(Edge e) {
-	Node * node = getNodePtrFromEdge(e);
+	Node *node = getNodePtrFromEdge(e);
 	uint numEdges = node->numEdges;
-	for(uint i=0; i < numEdges; i++) {
+	for (uint i = 0; i < numEdges; i++) {
 		Edge ec = node->edges[i];
 		if (!edgeIsVarConst(ec)) {
 			ourfree(ec.node_ptr);
@@ -116,7 +116,7 @@ void freeEdgeCNF(Edge e) {
 	ourfree(node);
 }
 
-void addEdgeToResizeNode(Node ** node, Edge e) {
+void addEdgeToResizeNode(Node **node, Edge e) {
 	Node *currnode = *node;
 	if (currnode->capacity == currnode->numEdges) {
 		Node *newnode = allocResizeNode( currnode->capacity << 1);
@@ -124,17 +124,17 @@ void addEdgeToResizeNode(Node ** node, Edge e) {
 		newnode->numEdges = currnode->numEdges;
 		memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
 		ourfree(currnode);
-		*node=newnode;
+		*node = newnode;
 		currnode = newnode;
 	}
 	currnode->edges[currnode->numEdges++] = e;
 }
 
-void mergeFreeNodeToResizeNode(Node **node, Node * innode) {
-	Node * currnode = *node;
+void mergeFreeNodeToResizeNode(Node **node, Node *innode) {
+	Node *currnode = *node;
 	uint currEdges = currnode->numEdges;
 	uint inEdges = innode->numEdges;
-	
+
 	uint newsize = currEdges + inEdges;
 	if (newsize >= currnode->capacity) {
 		if (newsize < innode->capacity) {
@@ -149,7 +149,7 @@ void mergeFreeNodeToResizeNode(Node **node, Node * innode) {
 			newnode->numEdges = currnode->numEdges;
 			memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
 			ourfree(currnode);
-			*node=newnode;
+			*node = newnode;
 			currnode = newnode;
 		}
 	} else {
@@ -166,8 +166,8 @@ void mergeFreeNodeToResizeNode(Node **node, Node * innode) {
 	ourfree(innode);
 }
 
-void mergeNodeToResizeNode(Node **node, Node * innode) {
-	Node * currnode = *node;
+void mergeNodeToResizeNode(Node **node, Node *innode) {
+	Node *currnode = *node;
 	uint currEdges = currnode->numEdges;
 	uint inEdges = innode->numEdges;
 	uint newsize = currEdges + inEdges;
@@ -177,7 +177,7 @@ void mergeNodeToResizeNode(Node **node, Node * innode) {
 		newnode->numEdges = currnode->numEdges;
 		memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
 		ourfree(currnode);
-		*node=newnode;
+		*node = newnode;
 		currnode = newnode;
 	}
 	memcpy(&currnode->edges[currnode->numEdges], innode->edges, inEdges * sizeof(Edge));
@@ -245,7 +245,7 @@ Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
 			ASSERT(!isNodeEdge(e1));
 			if (!sameSignEdge(e1, e2)) {
 				freeEdgesRec(lowindex + 1, edges);
-				freeEdgesRec(numEdges-initindex, &edges[initindex]);
+				freeEdgesRec(numEdges - initindex, &edges[initindex]);
 				return E_False;
 			}
 		} else
@@ -265,22 +265,22 @@ Edge constraintAND(CNF *cnf, uint numEdges, Edge *edges) {
 		Edge *e0edges = getEdgeArray(edges[0]);
 		Edge *e1edges = getEdgeArray(edges[1]);
 		if (sameNodeOppSign(e0edges[0], e1edges[0])) {
-			Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
+			Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[1]));
 			freeEdge(edges[0]);
 			freeEdge(edges[1]);
 			return result;
 		} else if (sameNodeOppSign(e0edges[0], e1edges[1])) {
-			Edge result=constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
+			Edge result = constraintNegate(constraintITE(cnf, e0edges[0], e0edges[1], e1edges[0]));
 			freeEdge(edges[0]);
 			freeEdge(edges[1]);
 			return result;
 		} else if (sameNodeOppSign(e0edges[1], e1edges[0])) {
-			Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
+			Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[1]));
 			freeEdge(edges[0]);
 			freeEdge(edges[1]);
 			return result;
 		} else if (sameNodeOppSign(e0edges[1], e1edges[1])) {
-			Edge result=constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
+			Edge result = constraintNegate(constraintITE(cnf, e0edges[1], e0edges[0], e1edges[0]));
 			freeEdge(edges[0]);
 			freeEdge(edges[1]);
 			return result;
@@ -375,7 +375,7 @@ Edge disjoinLit(Edge vec, Edge lit) {
 	Node *nvec = vec.node_ptr;
 	uint nvecedges = nvec->numEdges;
 
-	for(uint i=0; i < nvecedges; i++) {
+	for (uint i = 0; i < nvecedges; i++) {
 		Edge ce = nvec->edges[i];
 		if (!edgeIsVarConst(ce)) {
 			Node *cne = ce.node_ptr;
@@ -388,18 +388,18 @@ Edge disjoinLit(Edge vec, Edge lit) {
 			nvec->edges[i] = (Edge) {clause};
 		}
 	}
-	nvec->numVars+=nvecedges;
+	nvec->numVars += nvecedges;
 	return vec;
 }
 
-Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
+Edge disjoinAndFree(CNF *cnf, Edge newvec, Edge cnfform) {
 	Node *nnewvec = newvec.node_ptr;
 	Node *ncnfform = cnfform.node_ptr;
 	uint newvecedges = nnewvec->numEdges;
 	uint cnfedges = ncnfform->numEdges;
 	uint newvecvars = nnewvec->numVars;
 	uint cnfvars = ncnfform->numVars;
-	
+
 	if (cnfedges > 3 ||
 			((cnfedges * newvecvars + newvecedges * cnfvars) > (cnfedges + newvecedges + newvecvars + cnfvars))) {
 		Edge proxyVar = constraintNewVar(cnf);
@@ -416,7 +416,7 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
 
 
 
-	if (newvecedges == 1 || cnfedges ==1) {
+	if (newvecedges == 1 || cnfedges == 1) {
 		if (cnfedges != 1) {
 			Node *tmp = nnewvec;
 			nnewvec = ncnfform;
@@ -427,7 +427,7 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
 		Edge e = ncnfform->edges[0];
 		if (!edgeIsVarConst(e)) {
 			Node *n = e.node_ptr;
-			for(uint i=0; i < newvecedges; i++) {
+			for (uint i = 0; i < newvecedges; i++) {
 				Edge ce = nnewvec->edges[i];
 				if (isNodeEdge(ce)) {
 					Node *cne = ce.node_ptr;
@@ -442,7 +442,7 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
 			}
 			nnewvec->numVars += newvecedges * n->numVars;
 		} else {
-			for(uint i=0; i < newvecedges; i++) {
+			for (uint i = 0; i < newvecedges; i++) {
 				Edge ce = nnewvec->edges[i];
 				if (!edgeIsVarConst(ce)) {
 					Node *cne = ce.node_ptr;
@@ -457,16 +457,16 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
 			}
 			nnewvec->numVars += newvecedges;
 		}
-		freeEdgeCNF((Edge){ncnfform});
+		freeEdgeCNF((Edge) {ncnfform});
 		return (Edge) {nnewvec};
 	}
-	
-	Node * result = allocResizeNode(1);
 
-	for(uint i=0; i <newvecedges; i++) {
+	Node *result = allocResizeNode(1);
+
+	for (uint i = 0; i < newvecedges; i++) {
 		Edge nedge = nnewvec->edges[i];
 		uint nSize = isNodeEdge(nedge) ? nedge.node_ptr->numEdges : 1;
-		for(uint j=0; j < cnfedges; j++) {
+		for (uint j = 0; j < cnfedges; j++) {
 			Edge cedge = ncnfform->edges[j];
 			uint cSize = isNodeEdge(cedge) ? cedge.node_ptr->numEdges : 1;
 			if (equalsEdge(cedge, nedge)) {
@@ -484,7 +484,7 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
 				} else {
 					addEdgeToResizeNode(&clause, cedge);
 				}
-				addEdgeToResizeNode(&result, (Edge){clause});
+				addEdgeToResizeNode(&result, (Edge) {clause});
 				result->numVars += clause->numEdges;
 			}
 			//otherwise skip
@@ -503,14 +503,14 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 		return (Edge) {newvec};
 	}
 	bool negated = isNegEdge(input);
-	Node * node = getNodePtrFromEdge(input);
+	Node *node = getNodePtrFromEdge(input);
 	NodeType type = node->type;
 	if (!negated) {
 		if (type == NodeType_AND) {
 			//AND case
 			Node *newvec = allocResizeNode(node->numEdges);
 			uint numEdges = node->numEdges;
-			for(uint i = 0; i < numEdges; i++) {
+			for (uint i = 0; i < numEdges; i++) {
 				Edge e = simplifyCNF(cnf, node->edges[i]);
 				uint enumvars = e.node_ptr->numVars;
 				mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
@@ -530,10 +530,10 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 			//free temporary nodes
 			ourfree(getNodePtrFromEdge(thencons));
 			ourfree(getNodePtrFromEdge(elsecons));
-			Node * result = thencnf.node_ptr;
-			uint elsenumvars=elsecnf.node_ptr->numVars;
+			Node *result = thencnf.node_ptr;
+			uint elsenumvars = elsecnf.node_ptr->numVars;
 			mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
-			result->numVars+=elsenumvars;
+			result->numVars += elsenumvars;
 			return (Edge) {result};
 		}
 	} else {
@@ -542,7 +542,7 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 			uint numEdges = node->numEdges;
 
 			Edge newvec = simplifyCNF(cnf, constraintNegate(node->edges[0]));
-			for(uint i = 1; i < numEdges; i++) {
+			for (uint i = 1; i < numEdges; i++) {
 				Edge e = node->edges[i];
 				Edge cnfform = simplifyCNF(cnf, constraintNegate(e));
 				newvec = disjoinAndFree(cnf, newvec, cnfform);
@@ -558,7 +558,7 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 			Edge thencons = createNode(NodeType_AND, 2, thenedges);
 			Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
 			Edge elsecons = createNode(NodeType_AND, 2, elseedges);
-			
+
 			Edge combinededges[] = {constraintNegate(thencons), constraintNegate(elsecons)};
 			Edge combined = constraintNegate(createNode(NodeType_AND, 2, combinededges));
 			Edge result = simplifyCNF(cnf, combined);
@@ -572,26 +572,26 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 }
 
 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
-	Node * andNode = cnfform.node_ptr;
+	Node *andNode = cnfform.node_ptr;
 	int orvar = getEdgeVar(eorvar);
 	ASSERT(orvar != 0);
 	uint numEdges = andNode->numEdges;
-	for(uint i=0; i < numEdges; i++) {
+	for (uint i = 0; i < numEdges; i++) {
 		Edge e = andNode->edges[i];
 		if (edgeIsVarConst(e)) {
 			int array[2] = {getEdgeVar(e), orvar};
 			ASSERT(array[0] != 0);
 			addArrayClauseLiteral(cnf->solver, 2, array);
 		} else {
-			Node * clause = e.node_ptr;
+			Node *clause = e.node_ptr;
 			uint cnumEdges = clause->numEdges + 1;
 			if (cnumEdges > cnf->asize) {
 				cnf->asize = cnumEdges << 1;
 				ourfree(cnf->array);
 				cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
 			}
-			int * array = cnf->array;
-			for(uint j=0; j < (cnumEdges - 1); j++) {
+			int *array = cnf->array;
+			for (uint j = 0; j < (cnumEdges - 1); j++) {
 				array[j] = getEdgeVar(clause->edges[j]);
 				ASSERT(array[j] != 0);
 			}
@@ -602,24 +602,24 @@ void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar) {
 }
 
 void outputCNF(CNF *cnf, Edge cnfform) {
-	Node * andNode = cnfform.node_ptr;
+	Node *andNode = cnfform.node_ptr;
 	uint numEdges = andNode->numEdges;
-	for(uint i=0; i < numEdges; i++) {
+	for (uint i = 0; i < numEdges; i++) {
 		Edge e = andNode->edges[i];
 		if (edgeIsVarConst(e)) {
 			int array[1] = {getEdgeVar(e)};
 			ASSERT(array[0] != 0);
 			addArrayClauseLiteral(cnf->solver, 1, array);
 		} else {
-			Node * clause = e.node_ptr;
+			Node *clause = e.node_ptr;
 			uint cnumEdges = clause->numEdges;
 			if (cnumEdges > cnf->asize) {
 				cnf->asize = cnumEdges << 1;
 				ourfree(cnf->array);
 				cnf->array = (int *) ourmalloc(sizeof(int) * cnf->asize);
 			}
-			int * array = cnf->array;
-			for(uint j=0; j < cnumEdges; j++) {
+			int *array = cnf->array;
+			for (uint j = 0; j < cnumEdges; j++) {
 				array[j] = getEdgeVar(clause->edges[j]);
 				ASSERT(array[j] != 0);
 			}
@@ -664,7 +664,7 @@ void addConstraintCNF(CNF *cnf, Edge constraint) {
 	printCNF(constraint);
 	model_print("\n******************************\n");
 #endif
-	
+
 	Edge cnfform = simplifyCNF(cnf, constraint);
 	freeEdgeRec(constraint);
 	outputCNF(cnf, cnfform);
@@ -785,7 +785,7 @@ Edge generateLTValueConstraint(CNF *cnf, uint numvars, Edge *vars, uint value) {
 }
 
 void generateAddConstraint(CNF *cnf, uint nSum, Edge *sum, uint nVar1, Edge *var1, uint nVar2, Edge *var2) {
-  //TO WRITE....
+	//TO WRITE....
 }
 
 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
diff --git a/src/Backend/constraint.h b/src/Backend/constraint.h
index bfe3e25..d7d2744 100644
--- a/src/Backend/constraint.h
+++ b/src/Backend/constraint.h
@@ -48,7 +48,7 @@ struct CNF {
 	uint varcount;
 	uint asize;
 	IncrementalSolver *solver;
-	int * array;
+	int *array;
 	long long solveTime;
 	long long encodeTime;
 	bool unsat;
@@ -173,9 +173,9 @@ void printCNF(Edge e);
 Node *allocBaseNode(NodeType type, uint numEdges);
 Node *allocResizeNode(uint capacity);
 Edge cloneEdge(Edge e);
-void addEdgeToResizeNode(Node ** node, Edge e);
-void mergeFreeNodeToResizeNode(Node **node, Node * innode);
-void mergeNodeToResizeNode(Node **node, Node * innode);
+void addEdgeToResizeNode(Node **node, Edge e);
+void mergeFreeNodeToResizeNode(Node **node, Node *innode);
+void mergeNodeToResizeNode(Node **node, Node *innode);
 void freeEdgeRec(Edge e);
 void outputCNF(CNF *cnf, Edge cnfform);
 void outputCNFOR(CNF *cnf, Edge cnfform, Edge eorvar);
diff --git a/src/Backend/satelemencoder.cc b/src/Backend/satelemencoder.cc
index 5342c4f..6062591 100644
--- a/src/Backend/satelemencoder.cc
+++ b/src/Backend/satelemencoder.cc
@@ -7,7 +7,7 @@
 #include "predicate.h"
 
 
-void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool & memo) {
+void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool &memo) {
 	uint numParents = elem->parents.getSize();
 	uint posPolarity = 0;
 	uint negPolarity = 0;
@@ -15,10 +15,10 @@ void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool & memo) {
 	if (elem->type == ELEMFUNCRETURN) {
 		memo = true;
 	}
-	for(uint i = 0; i < numParents; i++) {
-		ASTNode * node = elem->parents.get(i);
+	for (uint i = 0; i < numParents; i++) {
+		ASTNode *node = elem->parents.get(i);
 		if (node->type == PREDICATEOP) {
-			BooleanPredicate * pred = (BooleanPredicate *) node;
+			BooleanPredicate *pred = (BooleanPredicate *) node;
 			Polarity polarity = pred->polarity;
 			FunctionEncodingType encType = pred->encoding.type;
 			bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
@@ -27,49 +27,49 @@ void SATEncoder::shouldMemoize(Element *elem, uint64_t val, bool & memo) {
 
 				UndefinedBehavior undefStatus = ((PredicateTable *)pred->predicate)->undefinedbehavior;
 
-				Polarity tpolarity=polarity;
+				Polarity tpolarity = polarity;
 				if (generateNegation)
 					tpolarity = negatePolarity(tpolarity);
-				if (undefStatus ==SATC_FLAGFORCEUNDEFINED)
+				if (undefStatus == SATC_FLAGFORCEUNDEFINED)
 					tpolarity = P_BOTHTRUEFALSE;
 				if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
 					memo = true;
 				if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
 					memo = true;
 			} else if (pred->predicate->type == OPERATORPRED) {
-					if (pred->encoding.type == ENUMERATEIMPLICATIONS || pred->encoding.type == ENUMERATEIMPLICATIONSNEGATE) {
-						Polarity tpolarity = polarity;
-						if (generateNegation)
-							tpolarity = negatePolarity(tpolarity);
-						PredicateOperator *predicate = (PredicateOperator *)pred->predicate;
-						uint numDomains = pred->inputs.getSize();
-						bool isConstant = true;
-						for (uint i = 0; i < numDomains; i++) {
-							Element *e = pred->inputs.get(i);
-							if (elem != e && e->type != ELEMCONST) {
-								isConstant = false;
-							}
+				if (pred->encoding.type == ENUMERATEIMPLICATIONS || pred->encoding.type == ENUMERATEIMPLICATIONSNEGATE) {
+					Polarity tpolarity = polarity;
+					if (generateNegation)
+						tpolarity = negatePolarity(tpolarity);
+					PredicateOperator *predicate = (PredicateOperator *)pred->predicate;
+					uint numDomains = pred->inputs.getSize();
+					bool isConstant = true;
+					for (uint i = 0; i < numDomains; i++) {
+						Element *e = pred->inputs.get(i);
+						if (elem != e && e->type != ELEMCONST) {
+							isConstant = false;
 						}
-						if (predicate->getOp() == SATC_EQUALS) {
+					}
+					if (predicate->getOp() == SATC_EQUALS) {
+						if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
+							posPolarity++;
+						if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
+							negPolarity++;
+					} else {
+						if (isConstant) {
 							if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
 								posPolarity++;
 							if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
 								negPolarity++;
 						} else {
-							if (isConstant) {
-								if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
-									posPolarity++;
-								if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
-									negPolarity++;
-							} else {
-								if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
-									memo = true;
-								if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
-									memo = true;							
-							}
+							if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_TRUE)
+								memo = true;
+							if (tpolarity == P_BOTHTRUEFALSE || tpolarity == P_FALSE)
+								memo = true;
 						}
 					}
-				} else {
+				}
+			} else {
 				ASSERT(0);
 			}
 		} else if (node->type == ELEMFUNCRETURN) {
@@ -130,7 +130,7 @@ Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, Polarity p,
 		if (elemEnc->isinUseElement(i) && elemEnc->encodingArray[i] == value) {
 			if (elemEnc->numVars == 0)
 				return E_True;
-			
+
 			if (elemEnc->encoding != EENC_NONE && elemEnc->numVars > 1) {
 				if (impliesPolarity(elemEnc->polarityArray[i], p)) {
 					return elemEnc->edgeArray[i];
@@ -142,11 +142,11 @@ Edge SATEncoder::getElementValueBinaryIndexConstraint(Element *elem, Polarity p,
 						generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_BOTHTRUEFALSE);
 						elemEnc->polarityArray[i] = p;
 					} else if (!impliesPolarity(elemEnc->polarityArray[i], P_TRUE)  && impliesPolarity(p, P_TRUE)) {
-						generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_TRUE);			
-						elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i])| ((int)P_TRUE));
-					}	else if (!impliesPolarity(elemEnc->polarityArray[i], P_FALSE)  && impliesPolarity(p, P_FALSE)) {
-						generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_FALSE);			
-						elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i])| ((int)P_FALSE));
+						generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_TRUE);
+						elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i]) | ((int)P_TRUE));
+					} else if (!impliesPolarity(elemEnc->polarityArray[i], P_FALSE)  && impliesPolarity(p, P_FALSE)) {
+						generateProxy(cnf, generateBinaryConstraint(cnf, elemEnc->numVars, elemEnc->variables, i), elemEnc->edgeArray[i], P_FALSE);
+						elemEnc->polarityArray[i] = (Polarity) (((int) elemEnc->polarityArray[i]) | ((int)P_FALSE));
 					}
 					return elemEnc->edgeArray[i];
 				}
@@ -214,7 +214,7 @@ void SATEncoder::generateBinaryValueEncodingVars(ElementEncoding *encoding) {
 	ASSERT(encoding->type == BINARYVAL);
 	allocElementConstraintVariables(encoding, encoding->numBits);
 	getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-	if(encoding->anyValue)
+	if (encoding->anyValue)
 		generateAnyValueBinaryValueEncoding(encoding);
 }
 
@@ -222,7 +222,7 @@ void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
 	ASSERT(encoding->type == BINARYINDEX);
 	allocElementConstraintVariables(encoding, NUMBITS(encoding->encArraySize - 1));
 	getArrayNewVarsSATEncoder(encoding->numVars, encoding->variables);
-	if(encoding->anyValue)
+	if (encoding->anyValue)
 		generateAnyValueBinaryIndexEncoding(encoding);
 }
 
@@ -234,7 +234,7 @@ void SATEncoder::generateOneHotEncodingVars(ElementEncoding *encoding) {
 			addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, encoding->variables[i], encoding->variables[j])));
 		}
 	}
-	if(encoding->anyValue)
+	if (encoding->anyValue)
 		addConstraintCNF(cnf, constraintOR(cnf, encoding->numVars, encoding->variables));
 }
 
@@ -270,30 +270,30 @@ void SATEncoder::generateElementEncoding(Element *element) {
 	}
 }
 
-void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding){
-	if(encoding->numVars == 0)
+void SATEncoder::generateAnyValueBinaryIndexEncoding(ElementEncoding *encoding) {
+	if (encoding->numVars == 0)
 		return;
 	int index = -1;
-	for(uint i= encoding->encArraySize-1; i>=0; i--){
-		if(encoding->isinUseElement(i)){
-			if(i+1 < encoding->encArraySize){
-				index = i+1;
+	for (uint i = encoding->encArraySize - 1; i >= 0; i--) {
+		if (encoding->isinUseElement(i)) {
+			if (i + 1 < encoding->encArraySize) {
+				index = i + 1;
 			}
 			break;
 		}
 	}
-	if( index != -1 ){
+	if ( index != -1 ) {
 		addConstraintCNF(cnf, generateLTValueConstraint(cnf, encoding->numVars, encoding->variables, index));
 	}
-	index = index == -1? encoding->encArraySize-1 : index-1;
-	for(int i= index; i>=0; i--) {
-		if (!encoding->isinUseElement(i)){
+	index = index == -1 ? encoding->encArraySize - 1 : index - 1;
+	for (int i = index; i >= 0; i--) {
+		if (!encoding->isinUseElement(i)) {
 			addConstraintCNF(cnf, constraintNegate( generateBinaryConstraint(cnf, encoding->numVars, encoding->variables, i)));
 		}
 	}
 }
 
-void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding){
+void SATEncoder::generateAnyValueBinaryValueEncoding(ElementEncoding *encoding) {
 	uint64_t minvalueminusoffset = encoding->low - encoding->offset;
 	uint64_t maxvalueminusoffset = encoding->high - encoding->offset;
 	model_print("This is minvalueminus offset: %lu", minvalueminusoffset);
diff --git a/src/Backend/satencoder.cc b/src/Backend/satencoder.cc
index b13541d..659c0d9 100644
--- a/src/Backend/satencoder.cc
+++ b/src/Backend/satencoder.cc
@@ -16,7 +16,7 @@
 SATEncoder::SATEncoder(CSolver *_solver) :
 	cnf(createCNF()),
 	solver(_solver),
-  vector(allocDefVectorEdge()) {
+	vector(allocDefVectorEdge()) {
 }
 
 SATEncoder::~SATEncoder() {
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 7fb889c..0ccf31c 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -22,7 +22,7 @@ public:
 
 	CMEMALLOC;
 private:
-	void shouldMemoize(Element *elem, uint64_t val, bool & memo);
+	void shouldMemoize(Element *elem, uint64_t val, bool &memo);
 	Edge getNewVarSATEncoder();
 	void getArrayNewVarsSATEncoder(uint num, Edge *carray);
 	Edge encodeVarSATEncoder(BooleanVar *constraint);
diff --git a/src/Backend/satfuncopencoder.cc b/src/Backend/satfuncopencoder.cc
index 0cfce9b..ff91dc3 100644
--- a/src/Backend/satfuncopencoder.cc
+++ b/src/Backend/satfuncopencoder.cc
@@ -48,7 +48,7 @@ Edge SATEncoder::encodeEnumOperatorPredicateSATEncoder(BooleanPredicate *constra
 	}
 
 	bool notfinished = true;
-        Edge carray[numDomains];
+	Edge carray[numDomains];
 	while (notfinished) {
 		if (predicate->evalPredicateOperator(vals) != generateNegation) {
 			//Include this in the set of terms
@@ -110,7 +110,7 @@ void SATEncoder::encodeOperatorElementFunctionSATEncoder(ElementFunction *func)
 	}
 
 	bool notfinished = true;
-        Edge carray[numDomains + 1];
+	Edge carray[numDomains + 1];
 	while (notfinished) {
 		uint64_t result = function->applyFunctionOperator(numDomains, vals);
 		bool isInRange = ((FunctionOperator *)func->getFunction())->isInRangeFunction(result);
diff --git a/src/Backend/satfunctableencoder.cc b/src/Backend/satfunctableencoder.cc
index 9e6087e..da89550 100644
--- a/src/Backend/satfunctableencoder.cc
+++ b/src/Backend/satfunctableencoder.cc
@@ -25,7 +25,7 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
 	bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
 	if (generateNegation)
 		polarity = negatePolarity(polarity);
-	if (undefStatus ==SATC_FLAGFORCEUNDEFINED)
+	if (undefStatus == SATC_FLAGFORCEUNDEFINED)
 		polarity = P_BOTHTRUEFALSE;
 
 	Edge constraints[size];
@@ -51,7 +51,7 @@ Edge SATEncoder::encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *con
 		case SATC_FLAGFORCEUNDEFINED: {
 			row = constraintAND(cnf, inputNum, carray);
 			uint pSize = constraint->parents.getSize();
-			if(!edgeIsVarConst(row) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter)){
+			if (!edgeIsVarConst(row) && pSize > (uint)solver->getTuner()->getTunable(PROXYVARIABLE, &proxyparameter)) {
 				Edge proxy = constraintNewVar(cnf);
 				generateProxy(cnf, row, proxy, P_BOTHTRUEFALSE);
 				Edge undefConst = encodeConstraintSATEncoder(constraint->undefStatus);
@@ -102,8 +102,8 @@ Edge SATEncoder::encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint
 
 	if (generateNegation)
 		polarity = negatePolarity(polarity);
-	
-        ASSERT(numDomains != 0);
+
+	ASSERT(numDomains != 0);
 	VectorEdge *clauses = allocDefVectorEdge();
 
 	uint indices[numDomains];	//setup indices
@@ -214,20 +214,20 @@ void SATEncoder::encodeEnumEntriesTableElemFuncSATEncoder(ElementFunction *func)
 		Edge output = getElementValueConstraint(func, P_TRUE, entry->output);
 		switch (undefStatus ) {
 		case SATC_IGNOREBEHAVIOR: {
-                        if(inputNum == 0){
-                                addConstraintCNF(cnf, output);
-                        }else{
-                                addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
-                        }
+			if (inputNum == 0) {
+				addConstraintCNF(cnf, output);
+			} else {
+				addConstraintCNF(cnf, constraintIMPLIES(cnf,constraintAND(cnf, inputNum, carray), output));
+			}
 			break;
 		}
 		case SATC_FLAGFORCEUNDEFINED: {
 			Edge undefConst = encodeConstraintSATEncoder(func->overflowstatus);
-                        if(inputNum ==0){
-                                addConstraintCNF(cnf, constraintAND2(cnf, output, constraintNegate(undefConst)));
-                        }else{
-                                addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
-                        }
+			if (inputNum == 0) {
+				addConstraintCNF(cnf, constraintAND2(cnf, output, constraintNegate(undefConst)));
+			} else {
+				addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, inputNum, carray), constraintAND2(cnf, output, constraintNegate(undefConst))));
+			}
 			break;
 		}
 		default:
@@ -243,7 +243,7 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
 	model_print("Enumeration Table functions ...\n");
 #endif
 	ASSERT(elemFunc->getFunction()->type == TABLEFUNC);
-	
+
 	//First encode children
 	Array<Element *> *elements = &elemFunc->inputs;
 	for (uint i = 0; i < elements->getSize(); i++) {
@@ -288,11 +288,11 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
 		switch (function->undefBehavior) {
 		case SATC_UNDEFINEDSETSFLAG: {
 			if (isInRange) {
-                                if(numDomains == 0){
-                                        addConstraintCNF(cnf,carray[numDomains]);
-                                }else{
-                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
-                                }
+				if (numDomains == 0) {
+					addConstraintCNF(cnf,carray[numDomains]);
+				} else {
+					addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), carray[numDomains]));
+				}
 			} else {
 				Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
 				addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
@@ -302,15 +302,15 @@ void SATEncoder::encodeEnumTableElemFunctionSATEncoder(ElementFunction *elemFunc
 		case SATC_FLAGIFFUNDEFINED: {
 			Edge undefConstraint = encodeConstraintSATEncoder(elemFunc->overflowstatus);
 			if (isInRange) {
-                                if(numDomains == 0){
-                                        addConstraintCNF(cnf, constraintAND2(cnf,carray[numDomains], constraintNegate(undefConstraint)) );
-                                }else{
-                                        Edge freshvar = constraintNewVar(cnf);
-                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
-                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
-                                        addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
-                                }
-				
+				if (numDomains == 0) {
+					addConstraintCNF(cnf, constraintAND2(cnf,carray[numDomains], constraintNegate(undefConstraint)) );
+				} else {
+					Edge freshvar = constraintNewVar(cnf);
+					addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), freshvar ));
+					addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, constraintNegate(undefConstraint) ));
+					addConstraintCNF(cnf, constraintIMPLIES(cnf, freshvar, carray[numDomains]));
+				}
+
 			} else {
 				addConstraintCNF(cnf, constraintIMPLIES(cnf, constraintAND(cnf, numDomains, carray), undefConstraint));
 			}
diff --git a/src/Collections/corestructs.cc b/src/Collections/corestructs.cc
index 9d9e36b..28d2faf 100644
--- a/src/Collections/corestructs.cc
+++ b/src/Collections/corestructs.cc
@@ -2,7 +2,7 @@
 #include "corestructs.h"
 #include "boolean.h"
 
-void BooleanEdge::print(){
+void BooleanEdge::print() {
 	if (isNegated())
 		model_print("!");
 	getBoolean()->print();
diff --git a/src/Collections/hashset.h b/src/Collections/hashset.h
index 009c047..86cbce9 100644
--- a/src/Collections/hashset.h
+++ b/src/Collections/hashset.h
@@ -18,10 +18,10 @@ struct Linknode {
 	Linknode<_Key> *next;
 };
 
-template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function) (_Key), bool (*equals) (_Key, _Key)>
+template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function)(_Key), bool (*equals)(_Key, _Key)>
 class Hashset;
 
-template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function) (_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals) (_Key, _Key) = defaultEquals<_Key> >
+template<typename _Key, typename _KeyInt, int _Shift, unsigned int (*hash_function)(_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = defaultEquals<_Key> >
 class SetIterator {
 public:
 	SetIterator(Linknode<_Key> *_curr, Hashset <_Key, _KeyInt, _Shift, hash_function, equals> *_set) :
@@ -76,7 +76,7 @@ private:
 	Hashset <_Key, _KeyInt, _Shift, hash_function, equals> *set;
 };
 
-template<typename _Key, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function) (_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals) (_Key, _Key) = defaultEquals<_Key> >
+template<typename _Key, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function)(_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = defaultEquals<_Key> >
 class Hashset {
 public:
 	Hashset(unsigned int initialcapacity = 16, double factor = 0.5) :
diff --git a/src/Collections/hashtable.h b/src/Collections/hashtable.h
index 0a50bb9..fdcb59f 100644
--- a/src/Collections/hashtable.h
+++ b/src/Collections/hashtable.h
@@ -57,7 +57,7 @@ inline bool defaultEquals(_Key key1, _Key key2) {
  *                 manipulation and storage.
  * @tparam _Shift  Logical shift to apply to all keys. Default 0.
  */
-template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function) (_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals) (_Key, _Key) = defaultEquals<_Key> >
+template<typename _Key, typename _Val, typename _KeyInt, int _Shift = 0, unsigned int (*hash_function)(_Key) = defaultHashFunction<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = defaultEquals<_Key> >
 class Hashtable {
 public:
 	/**
diff --git a/src/Collections/qsort.cc b/src/Collections/qsort.cc
index d384220..f4e7ec9 100644
--- a/src/Collections/qsort.cc
+++ b/src/Collections/qsort.cc
@@ -76,19 +76,19 @@
  * arithmetic gets lost in the time required for comparison function calls.
  */
 #define SWAP(a, b, count, size, tmp) { \
-		count = size;	\
+		count = size; \
 		do { \
-			tmp = *a;	\
+			tmp = *a; \
 			*a++ = *b; \
-			*b++ = tmp;	\
+			*b++ = tmp; \
 		} while (--count); \
 }
 
 /* Copy one block of size size to another. */
-#define COPY(a, b, count, size, tmp1, tmp2) {	\
-		count = size;	\
-		tmp1 = a;	\
-		tmp2 = b;	\
+#define COPY(a, b, count, size, tmp1, tmp2) { \
+		count = size; \
+		tmp1 = a; \
+		tmp2 = b; \
 		do { \
 			*tmp1++ = *tmp2++; \
 		} while (--count); \
@@ -102,18 +102,18 @@
  * j < nmemb, select largest of Ki, Kj and Kj+1.
  */
 #define CREATE(initval, nmemb, par_i, child_i, par, child, size, count, tmp) { \
-		for (par_i = initval; (child_i = par_i * 2) <= nmemb;	\
-				 par_i = child_i) {	\
+		for (par_i = initval; (child_i = par_i * 2) <= nmemb; \
+				 par_i = child_i) { \
 			child = base + child_i * size; \
-			if (child_i < nmemb && compar(child, child + size) < 0) {	\
+			if (child_i < nmemb && compar(child, child + size) < 0) { \
 				child += size; \
 				++child_i; \
-			}	\
+			} \
 			par = base + par_i * size; \
 			if (compar(child, par) <= 0) \
 				break; \
-			SWAP(par, child, count, size, tmp);	\
-		}	\
+			SWAP(par, child, count, size, tmp); \
+		} \
 }
 
 /*
@@ -133,27 +133,27 @@
  *
  * XXX Don't break the #define SELECT line, below.  Reiser cpp gets upset.
  */
-#define SELECT(par_i, child_i, nmemb, par, child, size, k, count, tmp1, tmp2) {	\
+#define SELECT(par_i, child_i, nmemb, par, child, size, k, count, tmp1, tmp2) { \
 		for (par_i = 1; (child_i = par_i * 2) <= nmemb; par_i = child_i) { \
 			child = base + child_i * size; \
-			if (child_i < nmemb && compar(child, child + size) < 0) {	\
+			if (child_i < nmemb && compar(child, child + size) < 0) { \
 				child += size; \
 				++child_i; \
-			}	\
+			} \
 			par = base + par_i * size; \
 			COPY(par, child, count, size, tmp1, tmp2); \
-		}	\
-		for (;; ) {	\
+		} \
+		for (;; ) { \
 			child_i = par_i; \
 			par_i = child_i / 2; \
 			child = base + child_i * size; \
 			par = base + par_i * size; \
-			if (child_i == 1 || compar(k, par) < 0) {	\
+			if (child_i == 1 || compar(k, par) < 0) { \
 				COPY(child, k, count, size, tmp1, tmp2); \
 				break; \
-			}	\
+			} \
 			COPY(child, par, count, size, tmp1, tmp2); \
-		}	\
+		} \
 }
 
 /*
@@ -236,18 +236,18 @@ static __inline void swapfunc(char *, char *, size_t, int);
 #define SWAPTYPE_INT  4
 #define SWAPTYPE_LONG 5
 
-#define TYPE_ALIGNED(TYPE, a, es)			\
+#define TYPE_ALIGNED(TYPE, a, es)     \
 	(((char *)a - (char *)0) % sizeof(TYPE) == 0 && es % sizeof(TYPE) == 0)
 
-#define swapcode(TYPE, parmi, parmj, n) {			\
-		size_t i = (n) / sizeof (TYPE);			\
-		TYPE *pi = (TYPE *) (parmi);			\
-		TYPE *pj = (TYPE *) (parmj);			\
-		do {						\
-			TYPE t = *pi;			 \
-			*pi++ = *pj;				\
-			*pj++ = t;				\
-		} while (--i > 0);				\
+#define swapcode(TYPE, parmi, parmj, n) {     \
+		size_t i = (n) / sizeof (TYPE);     \
+		TYPE *pi = (TYPE *) (parmi);      \
+		TYPE *pj = (TYPE *) (parmj);      \
+		do {            \
+			TYPE t = *pi;      \
+			*pi++ = *pj;        \
+			*pj++ = t;        \
+		} while (--i > 0);        \
 }
 
 static __inline void
@@ -268,23 +268,23 @@ swapfunc(char *a, char *b, size_t n, int swaptype)
 	}
 }
 
-#define swap(a, b)  do {				\
-		switch (swaptype) {				\
-		case SWAPTYPE_INT: {				\
-			int t = *(int *)(a);			\
-			*(int *)(a) = *(int *)(b);		\
-			*(int *)(b) = t;			\
-			break;					\
-		}						\
-		case SWAPTYPE_LONG: {				\
-			long t = *(long *)(a);			\
-			*(long *)(a) = *(long *)(b);		\
-			*(long *)(b) = t;			\
-			break;					\
-		}						\
-		default:					\
-			swapfunc(a, b, es, swaptype);		\
-		}						\
+#define swap(a, b)  do {        \
+		switch (swaptype) {       \
+		case SWAPTYPE_INT: {        \
+			int t = *(int *)(a);      \
+			*(int *)(a) = *(int *)(b);    \
+			*(int *)(b) = t;      \
+			break;          \
+		}           \
+		case SWAPTYPE_LONG: {       \
+			long t = *(long *)(a);      \
+			*(long *)(a) = *(long *)(b);    \
+			*(long *)(b) = t;     \
+			break;          \
+		}           \
+		default:          \
+			swapfunc(a, b, es, swaptype);   \
+		}           \
 } while (0)
 
 #define vecswap(a, b, n)  if ((n) > 0) swapfunc(a, b, n, swaptype)
diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index 3cf0010..6c53253 100644
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -2,112 +2,112 @@
 #define VECTOR_H
 #include <string.h>
 
-#define VectorDef(name, type)																						\
-	struct Vector ## name {																								\
-		uint size;																													\
-		uint capacity;																											\
-		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);	\
-	void pushVector ## name(Vector ## name * vector, type item);					 \
-	type lastVector ## name(Vector ## name * vector);											 \
-	void popVector ## name(Vector ## name * vector);											 \
-	type getVector ## name(Vector ## name * vector, uint index);					 \
-	void setExpandVector ## name(Vector ## name * vector, uint index, type item);	\
-	void setVector ## name(Vector ## name * vector, uint index, type item);	\
-	uint getSizeVector ## name(const Vector ## name * vector);									 \
-	void setSizeVector ## name(Vector ## name * vector, uint size);				 \
-	void deleteVector ## name(Vector ## name * vector);										 \
-	void clearVector ## name(Vector ## name * vector);										 \
-	void deleteVectorArray ## name(Vector ## name * vector);							 \
-	type *exposeArray ## name(Vector ## name * vector);									 \
+#define VectorDef(name, type)                                           \
+	struct Vector ## name {                                               \
+		uint size;                                                          \
+		uint capacity;                                                      \
+		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); \
+	void pushVector ## name(Vector ## name * vector, type item);           \
+	type lastVector ## name(Vector ## name * vector);                      \
+	void popVector ## name(Vector ## name * vector);                       \
+	type getVector ## name(Vector ## name * vector, uint index);           \
+	void setExpandVector ## name(Vector ## name * vector, uint index, type item); \
+	void setVector ## name(Vector ## name * vector, uint index, type item); \
+	uint getSizeVector ## name(const Vector ## name * vector);                   \
+	void setSizeVector ## name(Vector ## name * vector, uint size);        \
+	void deleteVector ## name(Vector ## name * vector);                    \
+	void clearVector ## name(Vector ## name * vector);                     \
+	void deleteVectorArray ## name(Vector ## name * vector);               \
+	type *exposeArray ## name(Vector ## name * vector);                  \
 	void initVector ## name(Vector ## name * vector, uint capacity); \
-	void initDefVector ## name(Vector ## name * vector);						\
+	void initDefVector ## name(Vector ## name * vector);            \
 	void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array);
 
-#define VectorImpl(name, type, defcap)																	\
-	Vector ## name * allocDefVector ## name() {														\
-		return allocVector ## name(defcap);																	\
-	}																																			\
-	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);								\
-		tmp->size = capacity;																									\
-		memcpy(tmp->array, array, capacity * sizeof(type));									\
-		return tmp;																													\
-	}																																			\
-	void popVector ## name(Vector ## name * vector) {											 \
-		vector->size--;																											\
-	}																																			\
-	type lastVector ## name(Vector ## name * vector) {										 \
-		return vector->array[vector->size - 1];																\
-	}																																			\
-	void setSizeVector ## name(Vector ## name * vector, uint size) {			 \
-		if (size <= vector->size) {																					\
-			vector->size = size;																								\
-			return;																														\
-		} else if (size > vector->capacity) {																\
-			vector->array = (type *)ourrealloc(vector->array, size * sizeof(type));	\
-			vector->capacity = size;																						\
-		}																																		\
+#define VectorImpl(name, type, defcap)                                  \
+	Vector ## name * allocDefVector ## name() {                           \
+		return allocVector ## name(defcap);                                 \
+	}                                                                     \
+	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);               \
+		tmp->size = capacity;                                                 \
+		memcpy(tmp->array, array, capacity * sizeof(type));                 \
+		return tmp;                                                         \
+	}                                                                     \
+	void popVector ## name(Vector ## name * vector) {                      \
+		vector->size--;                                                     \
+	}                                                                     \
+	type lastVector ## name(Vector ## name * vector) {                     \
+		return vector->array[vector->size - 1];                               \
+	}                                                                     \
+	void setSizeVector ## name(Vector ## name * vector, uint size) {       \
+		if (size <= vector->size) {                                         \
+			vector->size = size;                                                \
+			return;                                                           \
+		} else if (size > vector->capacity) {                               \
+			vector->array = (type *)ourrealloc(vector->array, size * sizeof(type)); \
+			vector->capacity = size;                                            \
+		}                                                                   \
 		bzero(&vector->array[vector->size], (size - vector->size) * sizeof(type)); \
-		vector->size = size;																									\
-	}																																			\
-	void pushVector ## name(Vector ## name * vector, type item) {					 \
-		if (vector->size >= vector->capacity) {															\
-			uint newcap = vector->capacity << 1;																\
-			vector->array = (type *)ourrealloc(vector->array, newcap * sizeof(type));	\
-			vector->capacity = newcap;																					\
-		}																																		\
-		vector->array[vector->size++] = item;																\
-	}																																			\
-	type getVector ## name(Vector ## name * vector, uint index) {					\
-		return vector->array[index];																				\
-	}																																			\
+		vector->size = size;                                                  \
+	}                                                                     \
+	void pushVector ## name(Vector ## name * vector, type item) {          \
+		if (vector->size >= vector->capacity) {                             \
+			uint newcap = vector->capacity << 1;                                \
+			vector->array = (type *)ourrealloc(vector->array, newcap * sizeof(type)); \
+			vector->capacity = newcap;                                          \
+		}                                                                   \
+		vector->array[vector->size++] = item;                               \
+	}                                                                     \
+	type getVector ## name(Vector ## name * vector, uint index) {         \
+		return vector->array[index];                                        \
+	}                                                                     \
 	void setExpandVector ## name(Vector ## name * vector, uint index, type item) { \
-		if (index >= vector->size)																						\
-			setSizeVector ## name(vector, index + 1);													\
-		setVector ## name(vector, index, item);															\
-	}																																			\
+		if (index >= vector->size)                                            \
+			setSizeVector ## name(vector, index + 1);                         \
+		setVector ## name(vector, index, item);                             \
+	}                                                                     \
 	void setVector ## name(Vector ## name * vector, uint index, type item) { \
-		vector->array[index] = item;																					\
-	}																																			\
-	uint getSizeVector ## name(const Vector ## name * vector) {						\
-		return vector->size;																								\
-	}																																			\
-	void deleteVector ## name(Vector ## name * vector) {										 \
-		ourfree(vector->array);																							\
-		ourfree(vector);																										\
-	}																																			\
-	void clearVector ## name(Vector ## name * vector) {											\
-		vector->size = 0;																											\
-	}																																			\
-	type *exposeArray ## name(Vector ## name * vector) {								 \
-		return vector->array;																								\
-	}																																			\
-	void deleteVectorArray ## name(Vector ## name * vector) {							 \
-		ourfree(vector->array);																							\
-	}																																			\
-	void initVector ## name(Vector ## name * vector, uint capacity) {	\
-		vector->size = 0;																											 \
-		vector->capacity = capacity;																							\
-		vector->array = (type *) ourmalloc(sizeof(type) * capacity);				\
-	}																																			\
-	void initDefVector ## name(Vector ## name * vector) {					\
-		initVector ## name(vector, defcap);													\
-	}																																			\
-	void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array) {	\
-		initVector ## name(vector, capacity);													 \
-		vector->size = capacity;																							\
-		memcpy(vector->array, array, capacity * sizeof(type));	\
+		vector->array[index] = item;                                          \
+	}                                                                     \
+	uint getSizeVector ## name(const Vector ## name * vector) {           \
+		return vector->size;                                                \
+	}                                                                     \
+	void deleteVector ## name(Vector ## name * vector) {                     \
+		ourfree(vector->array);                                             \
+		ourfree(vector);                                                    \
+	}                                                                     \
+	void clearVector ## name(Vector ## name * vector) {                     \
+		vector->size = 0;                                                     \
+	}                                                                     \
+	type *exposeArray ## name(Vector ## name * vector) {                 \
+		return vector->array;                                               \
+	}                                                                     \
+	void deleteVectorArray ## name(Vector ## name * vector) {              \
+		ourfree(vector->array);                                             \
+	}                                                                     \
+	void initVector ## name(Vector ## name * vector, uint capacity) { \
+		vector->size = 0;                                                      \
+		vector->capacity = capacity;                                              \
+		vector->array = (type *) ourmalloc(sizeof(type) * capacity);        \
+	}                                                                     \
+	void initDefVector ## name(Vector ## name * vector) {         \
+		initVector ## name(vector, defcap);                         \
+	}                                                                     \
+	void initVectorArray ## name(Vector ## name * vector, uint capacity, type * array) {  \
+		initVector ## name(vector, capacity);                          \
+		vector->size = capacity;                                              \
+		memcpy(vector->array, array, capacity * sizeof(type));  \
 	}
 #endif
diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index d153793..0740461 100644
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -33,7 +33,7 @@ public:
 	}
 	void print();
 
-        bool anyValue;
+	bool anyValue;
 	ElementEncodingType type;
 	Element *element;
 	Edge *variables;/* List Variables Used To Encode Element */
@@ -41,8 +41,8 @@ public:
 		struct {
 			uint64_t *encodingArray;	/* List the Variables in the appropriate order */
 			uint64_t *inUseArray;	/* Bitmap to track variables in use */
-			Edge * edgeArray;
-			Polarity * polarityArray;
+			Edge *edgeArray;
+			Polarity *polarityArray;
 			uint encArraySize;
 			ElemEnc encoding;
 		};
diff --git a/src/Test/anyvaluetest.cc b/src/Test/anyvaluetest.cc
index 952684a..1b101e3 100644
--- a/src/Test/anyvaluetest.cc
+++ b/src/Test/anyvaluetest.cc
@@ -11,13 +11,13 @@ int main(int numargs, char **argv) {
 	Element *e2 = solver->getElementVar(s2);
 	solver->mustHaveValue(e1);
 	solver->mustHaveValue(e2);
-	
+
 	Predicate *equals = solver->createPredicateOperator(SATC_EQUALS);
 	Element *inputs[] = {e1, e2};
 	BooleanEdge b = solver->applyPredicate(equals, inputs, 2);
 	b = solver->applyLogicalOperation(SATC_NOT, b);
 	solver->addConstraint(b);
-	
+
 	if (solver->solve() == 1)
 		printf("e1=%" PRIu64 "e2=%" PRIu64 "\n", solver->getElementValue(e1), solver->getElementValue(e2));
 	else
diff --git a/src/Test/buglongclause.cc b/src/Test/buglongclause.cc
index 14c217a..a3b5392 100644
--- a/src/Test/buglongclause.cc
+++ b/src/Test/buglongclause.cc
@@ -1,10 +1,10 @@
 #include "csolver.h"
 
 /**
- * !b1 AND 
+ * !b1 AND
  * !b2 OR b1 or (!b3 and b4) AND
  * b7 OR (!b1 AND (b5 or !b6))
- * 
+ *
  */
 int main(int numargs, char **argv) {
 	CSolver *solver = new CSolver();
@@ -41,10 +41,10 @@ int main(int numargs, char **argv) {
 	solver->printConstraints();
 	if (solver->solve() == 1)
 		printf("b1=%d\nb2=%d\nb3=%d\nb4=%d\nb5=%d\nb6=%d\nb7=%d\n",
-					solver->getBooleanValue(b1), solver->getBooleanValue(b2),
-					solver->getBooleanValue(b3), solver->getBooleanValue(b4),
-					solver->getBooleanValue(b5), solver->getBooleanValue(b6),
-					solver->getBooleanValue(b7));
+					 solver->getBooleanValue(b1), solver->getBooleanValue(b2),
+					 solver->getBooleanValue(b3), solver->getBooleanValue(b4),
+					 solver->getBooleanValue(b5), solver->getBooleanValue(b6),
+					 solver->getBooleanValue(b7));
 	else
 		printf("UNSAT\n");
 	delete solver;
diff --git a/src/Test/clonetest.cc b/src/Test/clonetest.cc
index 43954bd..067f7b8 100644
--- a/src/Test/clonetest.cc
+++ b/src/Test/clonetest.cc
@@ -7,44 +7,44 @@ int main(int argc, char **argv) {
 		printf("You should specify file names ...");
 		exit(-1);
 	}
-        //usleep(20000000);
+	//usleep(20000000);
 	for (int i = 1; i < argc; i++) {
 		CSolver *solver = CSolver::deserialize(argv[i]);
 		CSolver *copy = solver->clone();
-                CSolver *copy2 = solver->clone();
-                CSolver *copy3 = solver->clone();
-                CSolver *copy4 = solver->clone();
-                int value = copy->solve();
-                if (value == 1) {
+		CSolver *copy2 = solver->clone();
+		CSolver *copy3 = solver->clone();
+		CSolver *copy4 = solver->clone();
+		int value = copy->solve();
+		if (value == 1) {
 			printf("Copy %s is SAT\n", argv[i]);
 		} else {
 			printf("Copy %s is UNSAT\n", argv[i]);
 		}
-                value = copy2->solve();
-                if (value == 1) {
+		value = copy2->solve();
+		if (value == 1) {
 			printf("Copy2 %s is SAT\n", argv[i]);
 		} else {
 			printf("Copy2 %s is UNSAT\n", argv[i]);
 		}
-                value = copy3->solve();
-                if (value == 1) {
+		value = copy3->solve();
+		if (value == 1) {
 			printf("Copy3 %s is SAT\n", argv[i]);
 		} else {
 			printf("Copy3 %s is UNSAT\n", argv[i]);
 		}
-                value = copy4->solve();
-                if (value == 1) {
+		value = copy4->solve();
+		if (value == 1) {
 			printf("Copy4 %s is SAT\n", argv[i]);
 		} else {
 			printf("Copy4 %s is UNSAT\n", argv[i]);
 		}
-                value = solver->solve();
+		value = solver->solve();
 		if (value == 1) {
 			printf("Original %s is SAT\n", argv[i]);
 		} else {
 			printf("Original %s is UNSAT\n", argv[i]);
 		}
-                
+
 		delete solver;
 	}
 	return 1;
diff --git a/src/Test/deserializersolvetest.cc b/src/Test/deserializersolvetest.cc
index 2d7a852..bbb12e7 100644
--- a/src/Test/deserializersolvetest.cc
+++ b/src/Test/deserializersolvetest.cc
@@ -7,7 +7,7 @@ int main(int argc, char **argv) {
 		printf("You should specify file names ...");
 		exit(-1);
 	}
-        //usleep(20000000);
+	//usleep(20000000);
 	for (int i = 1; i < argc; i++) {
 		CSolver *solver = CSolver::deserialize(argv[i]);
 		int value = solver->solve();
diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc
index 0dbaf8d..c01bf14 100644
--- a/src/Translator/decomposeorderresolver.cc
+++ b/src/Translator/decomposeorderresolver.cc
@@ -25,12 +25,12 @@ DecomposeOrderResolver::~DecomposeOrderResolver() {
 
 void DecomposeOrderResolver::mustOrderEdge(uint64_t first, uint64_t second) {
 	DOREdge edge(first, second, 0, first, second);
-	DOREdge *oldedge=edges.get(&edge);
+	DOREdge *oldedge = edges.get(&edge);
 	if (oldedge != NULL) {
-		oldedge->mustbetrue=true;
+		oldedge->mustbetrue = true;
 	} else {
 		DOREdge *newedge = new DOREdge(first, second, 0, first, second);
-		newedge->mustbetrue=true;
+		newedge->mustbetrue = true;
 		edges.add(newedge);
 	}
 }
@@ -84,7 +84,7 @@ void DecomposeOrderResolver::buildGraph() {
 		DOREdge *doredge = iterator->next();
 		if (doredge->mustbetrue) {
 			graph->addEdge(doredge->origfirst, doredge->origsecond);
-			if (doredge->newfirst != doredge->origfirst || doredge->newsecond!=doredge->origsecond) {
+			if (doredge->newfirst != doredge->origfirst || doredge->newsecond != doredge->origsecond) {
 				graph->addEdge(doredge->newfirst, doredge->newsecond);
 			}
 		} else if (doredge->orderindex != 0) {
diff --git a/src/Translator/sattranslator.cc b/src/Translator/sattranslator.cc
index 8e2fcf1..f69bff7 100644
--- a/src/Translator/sattranslator.cc
+++ b/src/Translator/sattranslator.cc
@@ -39,12 +39,12 @@ uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elem
 	uint index = 0;
 	bool overflow = true;
 	for (uint i = 0; i < elemEnc->numVars; i++) {
-		if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] ))){
+		if (getValueSolver(This->getSATEncoder()->getCNF()->solver, getEdgeVar( elemEnc->variables[i] ))) {
 			index = i;
 			overflow = false;
 		}
 	}
-	if(overflow)
+	if (overflow)
 		model_print("WARNING: Element has undefined value!\n");
 	ASSERT(elemEnc->encArraySize > index && elemEnc->isinUseElement(index));
 	return elemEnc->encodingArray[index];
diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc
index 4a35fcd..3b5f8cc 100644
--- a/src/Tuner/autotuner.cc
+++ b/src/Tuner/autotuner.cc
@@ -18,14 +18,14 @@ void AutoTuner::addProblem(CSolver *solver) {
 long long AutoTuner::evaluate(CSolver *problem, SearchTuner *tuner) {
 	CSolver *copy = problem->clone();
 	copy->setTuner(tuner);
-        model_print("**********************\n");
+	model_print("**********************\n");
 	int sat = copy->solve();
-        if(result == UNSETVALUE)
-                result = sat;
-        else if(result != sat){
-                model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
-                copy->printConstraints();
-        }
+	if (result == UNSETVALUE)
+		result = sat;
+	else if (result != sat) {
+		model_print("&&&&&&&&&&&&&&&&&& Result has changed &&&&&&&&&&&&&\n");
+		copy->printConstraints();
+	}
 	//model_print("SAT %d\n", result);
 	long long elapsedTime = copy->getElapsedTime();
 //	long long encodeTime = copy->getEncodeTime();
diff --git a/src/Tuner/autotuner.h b/src/Tuner/autotuner.h
index 0346e42..fecba88 100644
--- a/src/Tuner/autotuner.h
+++ b/src/Tuner/autotuner.h
@@ -16,6 +16,6 @@ private:
 
 	Vector<CSolver *> solvers;
 	uint budget;
-        int result;
+	int result;
 };
 #endif
diff --git a/src/Tuner/tunable.cc b/src/Tuner/tunable.cc
index a57a601..6a74926 100644
--- a/src/Tuner/tunable.cc
+++ b/src/Tuner/tunable.cc
@@ -15,29 +15,29 @@ int DefaultTuner::getVarTunable(VarType vartype1, VarType vartype2, TunableParam
 	return descriptor->defaultValue;
 }
 
-const char* tunableParameterToString(Tunables tunable){
-        switch(tunable){
-                case DECOMPOSEORDER:
-                        return "DECOMPOSEORDER";
-                case MUSTREACHGLOBAL:
-                        return "MUSTREACHGLOBAL";
-                case MUSTREACHLOCAL:
-                        return "MUSTREACHLOCAL";
-                case MUSTREACHPRUNE:
-                        return "MUSTREACHPRUNE";
-                case OPTIMIZEORDERSTRUCTURE:
-                        return "OPTIMIZEORDERSTRUCTURE";
-                case ORDERINTEGERENCODING:
-                        return "ORDERINTEGERENCODING";
-                case PREPROCESS:
-                        return "PREPROCESS";
-                case NODEENCODING:
-                        return "NODEENCODING";
-                case EDGEENCODING:
-                        return "EDGEENCODING";
-                case MUSTEDGEPRUNE:
-                        return "MUSTEDGEPRUNE";
-                default:
-                        ASSERT(0);
-        }
+const char *tunableParameterToString(Tunables tunable) {
+	switch (tunable) {
+	case DECOMPOSEORDER:
+		return "DECOMPOSEORDER";
+	case MUSTREACHGLOBAL:
+		return "MUSTREACHGLOBAL";
+	case MUSTREACHLOCAL:
+		return "MUSTREACHLOCAL";
+	case MUSTREACHPRUNE:
+		return "MUSTREACHPRUNE";
+	case OPTIMIZEORDERSTRUCTURE:
+		return "OPTIMIZEORDERSTRUCTURE";
+	case ORDERINTEGERENCODING:
+		return "ORDERINTEGERENCODING";
+	case PREPROCESS:
+		return "PREPROCESS";
+	case NODEENCODING:
+		return "NODEENCODING";
+	case EDGEENCODING:
+		return "EDGEENCODING";
+	case MUSTEDGEPRUNE:
+		return "MUSTEDGEPRUNE";
+	default:
+		ASSERT(0);
+	}
 }
\ No newline at end of file
diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h
index 2d18a2d..9fd614a 100644
--- a/src/Tuner/tunable.h
+++ b/src/Tuner/tunable.h
@@ -43,5 +43,5 @@ static TunableDesc proxyparameter(1, 5, 2);
 enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE, ELEMENTOPT, ELEMENTOPTSETS, PROXYVARIABLE};
 typedef enum Tunables Tunables;
 
-const char* tunableParameterToString(Tunables tunable);
+const char *tunableParameterToString(Tunables tunable);
 #endif
diff --git a/src/ccsolver.cc b/src/ccsolver.cc
index 1c45480..f9ebdbb 100644
--- a/src/ccsolver.cc
+++ b/src/ccsolver.cc
@@ -1,150 +1,150 @@
 #include "csolver.h"
 #include "ccsolver.h"
 
-#define CCSOLVER(solver) ((CSolver*)solver)
+#define CCSOLVER(solver) ((CSolver *)solver)
 
-void* createCCSolver(){
-	return (void*) new CSolver();
+void *createCCSolver() {
+	return (void *) new CSolver();
 }
-void deleteCCSolver(void* solver){
+void deleteCCSolver(void *solver) {
 	delete CCSOLVER(solver);
 }
 
-void *createSet(void* solver,unsigned int type, long *elements, unsigned int num){
+void *createSet(void *solver,unsigned int type, long *elements, unsigned int num) {
 	return CCSOLVER(solver)->createSet((VarType) type, (uint64_t *)elements, (uint) num);
 }
 
-void *createRangeSet(void* solver,unsigned int type, long lowrange, long highrange){
+void *createRangeSet(void *solver,unsigned int type, long lowrange, long highrange) {
 	return CCSOLVER(solver)->createRangeSet((VarType) type, (uint64_t) lowrange, (uint64_t) highrange);
 }
 
-void *createRangeVar(void* solver,unsigned int type, long lowrange, long highrange){
+void *createRangeVar(void *solver,unsigned int type, long lowrange, long highrange) {
 	return CCSOLVER(solver)->createRangeVar((VarType) type, (uint64_t) lowrange, (uint64_t) highrange);
 }
 
-void *createMutableSet(void* solver,unsigned int type){
+void *createMutableSet(void *solver,unsigned int type) {
 	return CCSOLVER(solver)->createMutableSet((VarType) type);
 }
 
-void addItem(void* solver,void *set, long element){
-	CCSOLVER(solver)->addItem((MutableSet*) set, (uint64_t) element);
+void addItem(void *solver,void *set, long element) {
+	CCSOLVER(solver)->addItem((MutableSet *) set, (uint64_t) element);
 }
 
-void finalizeMutableSet(void* solver,void *set){
-	CCSOLVER(solver)->finalizeMutableSet((MutableSet*) set);
+void finalizeMutableSet(void *solver,void *set) {
+	CCSOLVER(solver)->finalizeMutableSet((MutableSet *) set);
 }
 
-void *getElementVar(void* solver,void *set){
-	return CCSOLVER(solver)->getElementVar((Set*) set);
+void *getElementVar(void *solver,void *set) {
+	return CCSOLVER(solver)->getElementVar((Set *) set);
 }
 
-void *getElementConst(void* solver,unsigned int type, long value){
+void *getElementConst(void *solver,unsigned int type, long value) {
 	return CCSOLVER(solver)->getElementConst((VarType) type, (uint64_t) value);
 }
 
-void *getElementRange (void* solver,void *element){
-	return CCSOLVER(solver)->getElementRange ((Element*) element);
+void *getElementRange (void *solver,void *element) {
+	return CCSOLVER(solver)->getElementRange ((Element *) element);
 }
 
-void* getBooleanVar(void* solver,unsigned int type){
+void *getBooleanVar(void *solver,unsigned int type) {
 	return CCSOLVER(solver)->getBooleanVar((VarType) type).getRaw();
 }
 
-void *createFunctionOperator(void* solver,unsigned int op, void *range,unsigned int overflowbehavior){
+void *createFunctionOperator(void *solver,unsigned int op, void *range,unsigned int overflowbehavior) {
 	return CCSOLVER(solver)->createFunctionOperator((ArithOp) op, (Set *)range, (OverFlowBehavior) overflowbehavior);
 }
 
-void *createPredicateOperator(void* solver,unsigned int op) {
+void *createPredicateOperator(void *solver,unsigned int op) {
 	return CCSOLVER(solver)->createPredicateOperator((CompOp) op);
 }
 
-void *createPredicateTable(void* solver,void *table, unsigned int behavior){
+void *createPredicateTable(void *solver,void *table, unsigned int behavior) {
 	return CCSOLVER(solver)->createPredicateTable((Table *)table, (UndefinedBehavior) behavior);
 }
 
-void *createTable(void* solver, void *range){
+void *createTable(void *solver, void *range) {
 	return CCSOLVER(solver)->createTable((Set *)range);
 }
 
-void *createTableForPredicate(void* solver) {
+void *createTableForPredicate(void *solver) {
 	return CCSOLVER(solver)->createTableForPredicate();
 }
 
-void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result){
+void addTableEntry(void *solver,void *table, void *inputs, unsigned int inputSize, long result) {
 	CCSOLVER(solver)->addTableEntry((Table *)table, (uint64_t *)inputs, (uint) inputSize, (uint64_t) result);
 }
 
-void *completeTable(void* solver,void *table, unsigned int behavior){
+void *completeTable(void *solver,void *table, unsigned int behavior) {
 	return CCSOLVER(solver)->completeTable((Table *) table, (UndefinedBehavior) behavior);
 }
 
-void *applyFunction(void* solver,void *function, void**array, unsigned int numArrays, void* overflowstatus){
-	return CCSOLVER(solver)->applyFunction((Function *)function, (Element **)array, (uint) numArrays, BooleanEdge ((Boolean*)overflowstatus));
+void *applyFunction(void *solver,void *function, void **array, unsigned int numArrays, void *overflowstatus) {
+	return CCSOLVER(solver)->applyFunction((Function *)function, (Element **)array, (uint) numArrays, BooleanEdge ((Boolean *)overflowstatus));
 }
 
-void* applyPredicateTable(void* solver,void *predicate, void **inputs, unsigned int numInputs, void* undefinedStatus){
-	return CCSOLVER(solver)->applyPredicateTable((Predicate *)predicate, (Element **)inputs, (uint) numInputs, BooleanEdge((Boolean*) undefinedStatus)).getRaw();
+void *applyPredicateTable(void *solver,void *predicate, void **inputs, unsigned int numInputs, void *undefinedStatus) {
+	return CCSOLVER(solver)->applyPredicateTable((Predicate *)predicate, (Element **)inputs, (uint) numInputs, BooleanEdge((Boolean *) undefinedStatus)).getRaw();
 }
 
-void* applyPredicate(void* solver,void *predicate, void **inputs, unsigned int numInputs){
+void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int numInputs) {
 	return CCSOLVER(solver)->applyPredicate((Predicate *)predicate, (Element **)inputs, (uint) numInputs).getRaw();
 }
 
-void* applyLogicalOperation(void* solver,unsigned int op, void *array, unsigned int asize){
+void *applyLogicalOperation(void *solver,unsigned int op, void *array, unsigned int asize) {
 	return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, (BooleanEdge *)array, (uint) asize).getRaw();
 }
 
-void* applyLogicalOperationTwo(void* solver,unsigned int op, void* arg1, void* arg2){
-	return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean*) arg1), BooleanEdge((Boolean*) arg2)).getRaw();
+void *applyLogicalOperationTwo(void *solver,unsigned int op, void *arg1, void *arg2) {
+	return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean *) arg1), BooleanEdge((Boolean *) arg2)).getRaw();
 }
 
-void* applyLogicalOperationOne(void* solver,unsigned int op, void* arg){
-	return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean*) arg)).getRaw();
+void *applyLogicalOperationOne(void *solver,unsigned int op, void *arg) {
+	return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean *) arg)).getRaw();
 }
 
-void addConstraint(void* solver,void* constraint){
-	CCSOLVER(solver)->addConstraint(BooleanEdge((Boolean*) constraint));
+void addConstraint(void *solver,void *constraint) {
+	CCSOLVER(solver)->addConstraint(BooleanEdge((Boolean *) constraint));
 }
 
-void *createOrder(void* solver,unsigned int type, void *set){
+void *createOrder(void *solver,unsigned int type, void *set) {
 	return CCSOLVER(solver)->createOrder((OrderType) type, (Set *)set);
 }
 
-void* orderConstraint(void* solver,void *order, long first, long second){
+void *orderConstraint(void *solver,void *order, long first, long second) {
 	return CCSOLVER(solver)->orderConstraint((Order *)order, (uint64_t) first, (uint64_t) second).getRaw();
 }
 
-int solve(void* solver){
+int solve(void *solver) {
 	return CCSOLVER(solver)->solve();
 }
 
-long getElementValue(void* solver,void *element){
+long getElementValue(void *solver,void *element) {
 	return (long) CCSOLVER(solver)->getElementValue((Element *)element);
 }
 
-int getBooleanValue(void* solver, void* boolean){
-	return CCSOLVER(solver)->getBooleanValue(BooleanEdge((Boolean*) boolean));
+int getBooleanValue(void *solver, void *boolean) {
+	return CCSOLVER(solver)->getBooleanValue(BooleanEdge((Boolean *) boolean));
 }
 
-int getOrderConstraintValue(void* solver,void *order, long first, long second){
+int getOrderConstraintValue(void *solver,void *order, long first, long second) {
 	return CCSOLVER(solver)->getOrderConstraintValue((Order *)order, (uint64_t) first, (uint64_t) second);
 }
 
-void printConstraints(void* solver){
+void printConstraints(void *solver) {
 	CCSOLVER(solver)->printConstraints();
 }
 
 
 
-void serialize(void* solver){
+void serialize(void *solver) {
 	CCSOLVER(solver)->serialize();
 }
 
 
-void mustHaveValue(void *solver, void *element){
-	CCSOLVER(solver)->mustHaveValue( (Element*) element);
+void mustHaveValue(void *solver, void *element) {
+	CCSOLVER(solver)->mustHaveValue( (Element *) element);
 }
 
-void* clone(void * solver){
+void *clone(void *solver) {
 	return CCSOLVER(solver)->clone();
 }
\ No newline at end of file
diff --git a/src/ccsolver.h b/src/ccsolver.h
index a17bd1c..c88214e 100644
--- a/src/ccsolver.h
+++ b/src/ccsolver.h
@@ -2,46 +2,46 @@
 #define __CCSOLVER_H
 
 
-typedef void* CCSolver;
+typedef void *CCSolver;
 #ifdef __cplusplus
 extern "C" {
 #endif
-void* createCCSolver();
-void deleteCCSolver(void* solver);
-void *createSet(void* solver,unsigned int type, long *elements, unsigned int num);
-void *createRangeSet(void* solver,unsigned int type, long lowrange, long highrange);
-void *createRangeVar(void* solver,unsigned int type, long lowrange, long highrange);
-void *createMutableSet(void* solver,unsigned int type);
-void addItem(void* solver,void *set, long element);
-void finalizeMutableSet(void* solver,void *set);
-void *getElementVar(void* solver,void *set);
-void *getElementConst(void* solver,unsigned int type, long value);
-void *getElementRange (void* solver,void *element);
-void* getBooleanVar(void* solver,unsigned int type);
-void *createFunctionOperator(void* solver,unsigned int op, void *range,unsigned int overflowbehavior);
-void *createPredicateOperator(void* solver,unsigned int op);
-void *createPredicateTable(void* solver,void *table, unsigned int behavior);
-void *createTable(void* solver, void *range);
-void *createTableForPredicate(void* solver);
-void addTableEntry(void* solver,void *table, void *inputs, unsigned int inputSize, long result);
-void *completeTable(void* solver,void *table, unsigned int behavior);
-void *applyFunction(void* solver,void *function, void**array, unsigned int numArrays, void* overflowstatus);
-void* applyPredicateTable(void* solver,void *predicate, void **inputs, unsigned int numInputs, void* undefinedStatus);
-void* applyPredicate(void* solver,void *predicate, void **inputs, unsigned int numInputs);
-void* applyLogicalOperation(void* solver,unsigned int op, void *array, unsigned int asize);
-void* applyLogicalOperationTwo(void* solver,unsigned int op, void* arg1, void* arg2);
-void* applyLogicalOperationOne(void* solver,unsigned int op, void* arg);
-void addConstraint(void* solver,void* constraint);
-void *createOrder(void* solver,unsigned int type, void *set);
-void* orderConstraint(void* solver,void *order, long first, long second);
-int solve(void* solver);
-long getElementValue(void* solver,void *element);
-int getBooleanValue(void* solver,void* boolean);
-int getOrderConstraintValue(void* solver,void *order, long first, long second);
-void printConstraints(void* solver);
-void serialize(void* solver);
+void *createCCSolver();
+void deleteCCSolver(void *solver);
+void *createSet(void *solver,unsigned int type, long *elements, unsigned int num);
+void *createRangeSet(void *solver,unsigned int type, long lowrange, long highrange);
+void *createRangeVar(void *solver,unsigned int type, long lowrange, long highrange);
+void *createMutableSet(void *solver,unsigned int type);
+void addItem(void *solver,void *set, long element);
+void finalizeMutableSet(void *solver,void *set);
+void *getElementVar(void *solver,void *set);
+void *getElementConst(void *solver,unsigned int type, long value);
+void *getElementRange (void *solver,void *element);
+void *getBooleanVar(void *solver,unsigned int type);
+void *createFunctionOperator(void *solver,unsigned int op, void *range,unsigned int overflowbehavior);
+void *createPredicateOperator(void *solver,unsigned int op);
+void *createPredicateTable(void *solver,void *table, unsigned int behavior);
+void *createTable(void *solver, void *range);
+void *createTableForPredicate(void *solver);
+void addTableEntry(void *solver,void *table, void *inputs, unsigned int inputSize, long result);
+void *completeTable(void *solver,void *table, unsigned int behavior);
+void *applyFunction(void *solver,void *function, void **array, unsigned int numArrays, void *overflowstatus);
+void *applyPredicateTable(void *solver,void *predicate, void **inputs, unsigned int numInputs, void *undefinedStatus);
+void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int numInputs);
+void *applyLogicalOperation(void *solver,unsigned int op, void *array, unsigned int asize);
+void *applyLogicalOperationTwo(void *solver,unsigned int op, void *arg1, void *arg2);
+void *applyLogicalOperationOne(void *solver,unsigned int op, void *arg);
+void addConstraint(void *solver,void *constraint);
+void *createOrder(void *solver,unsigned int type, void *set);
+void *orderConstraint(void *solver,void *order, long first, long second);
+int solve(void *solver);
+long getElementValue(void *solver,void *element);
+int getBooleanValue(void *solver,void *boolean);
+int getOrderConstraintValue(void *solver,void *order, long first, long second);
+void printConstraints(void *solver);
+void serialize(void *solver);
 void mustHaveValue(void *solver, void *element);
-void* clone(void * solver);
+void *clone(void *solver);
 #ifdef __cplusplus
 }
 #endif
diff --git a/src/common.h b/src/common.h
index 3a0eeaa..48b2a7e 100644
--- a/src/common.h
+++ b/src/common.h
@@ -55,9 +55,9 @@ void assert_hook(void);
 		if (!(expr)) { \
 			fprintf(stderr, "Error: assertion failed in %s at line %d\n", __FILE__, __LINE__); \
 			/* print_trace(); // Trace printing may cause dynamic memory allocation */ \
-			assert_hook();													 \
-			exit(EXIT_FAILURE);	\
-		}	\
+			assert_hook();                           \
+			exit(EXIT_FAILURE); \
+		} \
 	} while (0)
 #else
 #define ASSERT(expr) \
diff --git a/src/csolver.cc b/src/csolver.cc
index 44b29bb..07a6168 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -184,8 +184,8 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange
 	return set;
 }
 
-bool CSolver::itemExistInSet(Set *set, uint64_t item){
-        return set->exists(item);
+bool CSolver::itemExistInSet(Set *set, uint64_t item) {
+	return set->exists(item);
 }
 
 VarType CSolver::getSetVarType(Set *set) {
@@ -223,7 +223,7 @@ Element *CSolver::getElementVar(Set *set) {
 	return element;
 }
 
-void CSolver::mustHaveValue(Element *element){
+void CSolver::mustHaveValue(Element *element) {
 	element->getElementEncoding()->anyValue = true;
 }
 
diff --git a/src/csolver.h b/src/csolver.h
index c916c58..19ba3e1 100644
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -18,17 +18,17 @@ public:
 	/** This function creates a set from lowrange to highrange (inclusive). */
 
 	Set *createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange);
-        
-        bool itemExistInSet(Set *set, uint64_t item);
+
+	bool itemExistInSet(Set *set, uint64_t item);
 
 	VarType getSetVarType(Set *set);
 
 	Element *createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange);
 
 	/** This function creates a mutable set.
-         * Note: You should use addItem for adding new item to Mutable sets, and
-         * at the end, you should call finalizeMutableSet!
-         */
+	 * Note: You should use addItem for adding new item to Mutable sets, and
+	 * at the end, you should call finalizeMutableSet!
+	 */
 
 	MutableSet *createMutableSet(VarType type);
 
@@ -58,7 +58,7 @@ public:
 	Set *getElementRange (Element *element);
 
 	void mustHaveValue(Element *element);
-        
+
 	BooleanEdge getBooleanTrue();
 
 	BooleanEdge getBooleanFalse();
@@ -176,8 +176,8 @@ public:
 private:
 	void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
 	void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
-	void handleFunction(ElementFunction * ef, BooleanEdge child);
-	
+	void handleFunction(ElementFunction *ef, BooleanEdge child);
+
 	//These two functions are helpers if the client has a pointer to a
 	//Boolean object that we have since replaced
 	BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
diff --git a/src/mymemory.h b/src/mymemory.h
index b78eb54..9708936 100644
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -45,21 +45,21 @@ static inline void *ourcalloc(size_t count, size_t size) { return calloc(count,
 static inline void *ourrealloc(void *ptr, size_t size) { return realloc(ptr, size); }
 #endif
 
-#define CMEMALLOC														\
-	void *operator new(size_t size) {				\
-		return ourmalloc(size);								 \
-	}																									 \
-	void operator delete(void *p, size_t size) {			 \
-		ourfree(p);																			 \
-	}																									 \
-	void *operator new[](size_t size) {								\
-		return ourmalloc(size);													 \
-	}																										 \
-	void operator delete[](void *p, size_t size) {			 \
-		ourfree(p);																				 \
-	}																																			\
-	void *operator new(size_t size, void *p) {															/* placement new */	\
-		return p;																														\
+#define CMEMALLOC                           \
+	void *operator new(size_t size) {       \
+		return ourmalloc(size);                \
+	}                                                  \
+	void operator delete(void *p, size_t size) {       \
+		ourfree(p);                                      \
+	}                                                  \
+	void *operator new[](size_t size) {               \
+		return ourmalloc(size);                          \
+	}                                                    \
+	void operator delete[](void *p, size_t size) {       \
+		ourfree(p);                                        \
+	}                                                                     \
+	void *operator new(size_t size, void *p) {															/* placement new */ \
+		return p;                                                           \
 	}
 
 #endif/* _MY_MEMORY_H */