X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fconstraint.cc;h=d69e1946a7effc46cd90f3a79a428e0ee4d909de;hp=febccd13864bb4c30031e980555d2e404587eb34;hb=dd394251eb1578f17507f5da84791113e1e9cef7;hpb=f3afe6e2ef7e4c2bcd95000ea3e1e17f9e538789

diff --git a/src/Backend/constraint.cc b/src/Backend/constraint.cc
old mode 100644
new mode 100755
index febccd1..d69e194
--- a/src/Backend/constraint.cc
+++ b/src/Backend/constraint.cc
@@ -15,10 +15,10 @@ Edge E_False = {(Node *)(uintptr_t) (EDGE_IS_VAR_CONSTANT | NEGATE_EDGE)};
 Edge E_BOGUS = {(Node *)0xffff5673};
 Edge E_NULL = {(Node *)NULL};
 
-
 CNF *createCNF() {
 	CNF *cnf = (CNF *) ourmalloc(sizeof(CNF));
 	cnf->varcount = 1;
+	cnf->clausecount = 0;
 	cnf->solver = allocIncrementalSolver();
 	cnf->solveTime = 0;
 	cnf->encodeTime = 0;
@@ -37,6 +37,7 @@ void deleteCNF(CNF *cnf) {
 void resetCNF(CNF *cnf) {
 	resetSolver(cnf->solver);
 	cnf->varcount = 1;
+	cnf->clausecount = 0;
 	cnf->solveTime = 0;
 	cnf->encodeTime = 0;
 	cnf->unsat = false;
@@ -44,6 +45,7 @@ void resetCNF(CNF *cnf) {
 
 Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
 	Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
+	n->numVars = 0;
 	n->type = type;
 	n->numEdges = numEdges;
 	memcpy(n->edges, edges, sizeof(Edge) * numEdges);
@@ -52,6 +54,7 @@ Node *allocNode(NodeType type, uint numEdges, Edge *edges) {
 
 Node *allocBaseNode(NodeType type, uint numEdges) {
 	Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * numEdges);
+	n->numVars = 0;
 	n->type = type;
 	n->numEdges = numEdges;
 	return n;
@@ -59,6 +62,7 @@ Node *allocBaseNode(NodeType type, uint numEdges) {
 
 Node *allocResizeNode(uint capacity) {
 	Node *n = (Node *)ourmalloc(sizeof(Node) + sizeof(Edge) * capacity);
+	n->numVars = 0;
 	n->numEdges = 0;
 	n->capacity = capacity;
 	return n;
@@ -67,11 +71,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};
@@ -80,9 +84,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);
@@ -91,21 +95,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);
@@ -114,42 +118,46 @@ 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);
+		newnode->numVars = currnode->numVars;
 		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) {
 			//just swap
+			innode->numVars = currnode->numVars;
 			Node *tmp = innode;
 			innode = currnode;
 			*node = currnode = tmp;
 		} else {
 			Node *newnode = allocResizeNode( newsize << 1);
+			newnode->numVars = currnode->numVars;
 			newnode->numEdges = currnode->numEdges;
 			memcpy(newnode->edges, currnode->edges, newnode->numEdges * sizeof(Edge));
 			ourfree(currnode);
-			*node=newnode;
+			*node = newnode;
 			currnode = newnode;
 		}
 	} else {
 		if (inEdges > currEdges && newsize < innode->capacity) {
 			//just swap
+			innode->numVars = currnode->numVars;
 			Node *tmp = innode;
 			innode = currnode;
 			*node = currnode = tmp;
@@ -160,17 +168,18 @@ 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;
 	if (newsize >= currnode->capacity) {
 		Node *newnode = allocResizeNode( newsize << 1);
+		newnode->numVars = currnode->numVars;
 		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));
@@ -183,13 +192,24 @@ Edge createNode(NodeType type, uint numEdges, Edge *edges) {
 }
 
 Edge constraintOR(CNF *cnf, uint numEdges, Edge *edges) {
-	Edge edgearray[numEdges];
+	if (numEdges < 200000) {
+		Edge edgearray[numEdges];
 
-	for (uint i = 0; i < numEdges; i++) {
-		edgearray[i] = constraintNegate(edges[i]);
+		for (uint i = 0; i < numEdges; i++) {
+			edgearray[i] = constraintNegate(edges[i]);
+		}
+		Edge eand = constraintAND(cnf, numEdges, edgearray);
+		return constraintNegate(eand);
+	} else {
+		Edge * edgearray=(Edge *)ourmalloc(numEdges*sizeof(Edge));
+		
+		for (uint i = 0; i < numEdges; i++) {
+			edgearray[i] = constraintNegate(edges[i]);
+		}
+		Edge eand = constraintAND(cnf, numEdges, edgearray);
+		ourfree(edgearray);
+		return constraintNegate(eand);
 	}
-	Edge eand = constraintAND(cnf, numEdges, edgearray);
-	return constraintNegate(eand);
 }
 
 Edge constraintOR2(CNF *cnf, Edge left, Edge right) {
@@ -238,7 +258,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
@@ -258,22 +278,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;
@@ -368,7 +388,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;
@@ -381,16 +401,35 @@ Edge disjoinLit(Edge vec, Edge lit) {
 			nvec->edges[i] = (Edge) {clause};
 		}
 	}
+	nvec->numVars += nvecedges;
 	return vec;
 }
 
-Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
-	Node * result = allocResizeNode(1);
+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;
-	if (newvecedges == 1 || cnfedges ==1) {
+	uint newvecvars = nnewvec->numVars;
+	uint cnfvars = ncnfform->numVars;
+
+	if (cnfedges > 3 ||
+			((cnfedges * newvecvars + newvecedges * cnfvars) > (cnfedges + newvecedges + newvecvars + cnfvars))) {
+		Edge proxyVar = constraintNewVar(cnf);
+		if (newvecedges > cnfedges) {
+			outputCNFOR(cnf, newvec, constraintNegate(proxyVar));
+			freeEdgeCNF(newvec);
+			return disjoinLit(cnfform, proxyVar);
+		} else {
+			outputCNFOR(cnf, cnfform, constraintNegate(proxyVar));
+			freeEdgeCNF(cnfform);
+			return disjoinLit(newvec, proxyVar);
+		}
+	}
+
+
+
+	if (newvecedges == 1 || cnfedges == 1) {
 		if (cnfedges != 1) {
 			Node *tmp = nnewvec;
 			nnewvec = ncnfform;
@@ -401,7 +440,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;
@@ -414,8 +453,9 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
 					nnewvec->edges[i] = (Edge) {clause};
 				}
 			}
+			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;
@@ -428,32 +468,23 @@ Edge disjoinAndFree(CNF * cnf, Edge newvec, Edge cnfform) {
 					nnewvec->edges[i] = (Edge) {clause};
 				}
 			}
+			nnewvec->numVars += newvecedges;
 		}
-		freeEdgeCNF((Edge){ncnfform});
+		freeEdgeCNF((Edge) {ncnfform});
 		return (Edge) {nnewvec};
 	}
-	if ((newvecedges > 3 && cnfedges > 3) ||
-			(newvecedges > 10 && cnfedges >=2) ||
-			(newvecedges >= 2 && cnfedges > 10)) {
-		Edge proxyVar = constraintNewVar(cnf);
-		if (newvecedges > cnfedges) {
-			outputCNFOR(cnf, newvec, constraintNegate(proxyVar));
-			freeEdgeCNF(newvec);
-			return disjoinLit(cnfform, proxyVar);
-		} else {
-			outputCNFOR(cnf, cnfform, constraintNegate(proxyVar));
-			freeEdgeCNF(cnfform);
-			return disjoinLit(newvec, proxyVar);
-		}
-	}
-	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)) {
 				addEdgeToResizeNode(&result, cedge);
+				result->numVars += cSize;
 			} else if (!sameNodeOppSign(nedge, cedge)) {
 				Node *clause = allocResizeNode(cSize + nSize);
 				if (isNodeEdge(nedge)) {
@@ -466,7 +497,8 @@ 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
 		}
@@ -480,19 +512,22 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 	if (edgeIsVarConst(input)) {
 		Node *newvec = allocResizeNode(1);
 		addEdgeToResizeNode(&newvec, input);
+		newvec->numVars = 1;
 		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);
+				newvec->numVars += enumvars;
 			}
 			return (Edge) {newvec};
 		} else {
@@ -508,8 +543,10 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 			//free temporary nodes
 			ourfree(getNodePtrFromEdge(thencons));
 			ourfree(getNodePtrFromEdge(elsecons));
-			Node * result = thencnf.node_ptr;
+			Node *result = thencnf.node_ptr;
+			uint elsenumvars = elsecnf.node_ptr->numVars;
 			mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
+			result->numVars += elsenumvars;
 			return (Edge) {result};
 		}
 	} else {
@@ -518,7 +555,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);
@@ -534,7 +571,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);
@@ -547,231 +584,64 @@ Edge simplifyCNF(CNF *cnf, Edge input) {
 	}
 }
 
-/*
-Edge simplifyCNF(CNF *cnf, Edge input) {
-	if (edgeIsVarConst(input)) {
-		Node *newvec = allocResizeNode(1);
-		addEdgeToResizeNode(&newvec, input);
-		return (Edge) {newvec};
-	}
-	bool negated = isNegEdge(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++) {
-				Edge e = simplifyCNF(cnf, node->edges[i]);
-				mergeFreeNodeToResizeNode(&newvec, e.node_ptr);
-			}
-			return (Edge) {newvec};
-		} else {
-			Edge cond = node->edges[0];
-			Edge thenedge = node->edges[1];
-			Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
-			Edge thenedges[] = {cond, constraintNegate(thenedge)};
-			Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
-			Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
-			Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
-			Edge thencnf = simplifyCNF(cnf, thencons);
-			Edge elsecnf = simplifyCNF(cnf, elsecons);
-			//free temporary nodes
-			ourfree(getNodePtrFromEdge(thencons));
-			ourfree(getNodePtrFromEdge(elsecons));
-			Node * result = thencnf.node_ptr;
-			mergeFreeNodeToResizeNode(&result, elsecnf.node_ptr);
-			return (Edge) {result};
-		}
-	} else {
-		if (type == NodeType_AND) {
-			//OR Case
-			uint numEdges = node->numEdges;
-			
-			for(uint i = 0; i < numEdges; i++) {
-				Edge e = node->edges[i];
-				bool enegate = isNegEdge(e);
-				if (!edgeIsVarConst(e)) {
-					Node * enode = getNodePtrFromEdge(e);
-					NodeType etype = enode->type;
-					if (enegate) {
-						if (etype == NodeType_AND) {
-							//OR of AND Case
-							uint eNumEdges = enode->numEdges;
-							Node * newnode = allocResizeNode(0);
-							Node * clause = allocBaseNode(NodeType_AND, numEdges);
-							memcpy(clause->edges, node->edges, sizeof(Edge) * i);
-							if ((i + 1) < numEdges) {
-								memcpy(&clause->edges[i+1], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
-							}
-										 
-							for(uint j = 0; j < eNumEdges; j++) {
-								clause->edges[i] = constraintNegate(enode->edges[j]);
-								Edge simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
-								mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
-							}
-							ourfree(clause);
-							return (Edge) {newnode};
-						} else {
-							//OR of IFF or ITE
-							Edge cond = enode->edges[0];
-							Edge thenedge = enode->edges[1];
-							Edge elseedge = (enode->type == NodeType_IFF) ? constraintNegate(thenedge) : enode->edges[2];
-							Edge thenedges[] = {cond, constraintNegate(thenedge)};
-							Edge thencons = constraintNegate(createNode(NodeType_AND, 2, thenedges));
-							Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
-							Edge elsecons = constraintNegate(createNode(NodeType_AND, 2, elseedges));
-
-							//OR of AND Case
-							Node * newnode = allocResizeNode(0);
-							Node * clause = allocBaseNode(NodeType_AND, numEdges);
-							memcpy(clause->edges, node->edges, sizeof(Edge) * i);
-							if ((i + 1) < numEdges) {
-								memcpy(&clause->edges[i+1], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
-							}
-
-							clause->edges[i] = constraintNegate(thencons);
-							Edge simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
-							mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
-							
-							clause->edges[i] = constraintNegate(elsecons);
-							simplify = simplifyCNF(cnf, constraintNegate((Edge){clause}));
-							mergeFreeNodeToResizeNode(&newnode, simplify.node_ptr);
-
-							//free temporary nodes
-							ourfree(getNodePtrFromEdge(thencons));
-							ourfree(getNodePtrFromEdge(elsecons));
-							ourfree(clause);
-							return (Edge) {newnode};
-						}
-					} else {
-						if (etype == NodeType_AND) {
-							//OR of OR Case
-							uint eNumEdges = enode->numEdges;
-							Node * clause = allocBaseNode(NodeType_AND, eNumEdges + numEdges - 1);
-							memcpy(clause->edges, node->edges, sizeof(Edge) * i);
-							if ((i + 1) < numEdges) {
-								memcpy(&clause->edges[i], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
-							}
-							memcpy(&clause->edges[numEdges-1], enode->edges, sizeof(Edge) * eNumEdges);
-							Edge eclause = {clause};
-							Edge result = simplifyCNF(cnf, constraintNegate(eclause));
-							ourfree(clause);
-							return result;
-						} else {
-							//OR of !(IFF or ITE)
-							Edge cond = node->edges[0];
-							Edge thenedge = node->edges[1];
-							Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
-							Edge thenedges[] = {cond, constraintNegate(thenedge)};
-							Edge thencons = createNode(NodeType_AND, 2, thenedges);
-							Edge elseedges[] = {constraintNegate(cond), constraintNegate(elseedge)};
-							Edge elsecons = createNode(NodeType_AND, 2, elseedges);
-
-
-							Node * clause = allocBaseNode(NodeType_AND, numEdges + 1);
-							memcpy(clause->edges, node->edges, sizeof(Edge) * i);
-							if ((i + 1) < numEdges) {
-								memcpy(&clause->edges[i], &node->edges[i+1], sizeof(Edge) * (numEdges - i - 1));
-							}
-							clause->edges[numEdges-1] = constraintNegate(thencons);
-							clause->edges[numEdges] = constraintNegate(elsecons);
-							Edge result = simplifyCNF(cnf, constraintNegate((Edge) {clause}));
-							//free temporary nodes
-							ourfree(getNodePtrFromEdge(thencons));
-							ourfree(getNodePtrFromEdge(elsecons));
-							ourfree(clause);
-							return result;
-						}
-					}
-				}
-			}
-			
-			Node *newvec = allocResizeNode(numEdges);
-			for(uint i=0; i < numEdges; i++) {
-				addEdgeToResizeNode(&newvec, constraintNegate(node->edges[i]));
-			}
-			Node * result = allocResizeNode(1);
-			addEdgeToResizeNode(&result, (Edge){newvec});
-			return (Edge) {result};
-		} else {
-			Edge cond = node->edges[0];
-			Edge thenedge = node->edges[1];
-			Edge elseedge = (type == NodeType_IFF) ? constraintNegate(thenedge) : node->edges[2];
-
-
-			Edge thenedges[] = {cond, constraintNegate(thenedge)};
-			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);
-			//free temporary nodes
-			ourfree(getNodePtrFromEdge(thencons));
-			ourfree(getNodePtrFromEdge(elsecons));
-			ourfree(getNodePtrFromEdge(combined));
-			return result;
-		}
-	}
+void addClause(CNF *cnf, uint numliterals, int *literals) {
+	cnf->clausecount++;
+	addArrayClauseLiteral(cnf->solver, numliterals, literals);
 }
-*/
+
 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);
+			addClause(cnf, 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);
 			}
 			array[cnumEdges - 1] = orvar;
-			addArrayClauseLiteral(cnf->solver, cnumEdges, array);
+			addClause(cnf, cnumEdges, array);
 		}
 	}
 }
 
-
 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);
+			addClause(cnf, 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);
 			}
-			addArrayClauseLiteral(cnf->solver, cnumEdges, array);
+			addClause(cnf, cnumEdges, array);
 		}
 	}
 }
@@ -812,7 +682,7 @@ void addConstraintCNF(CNF *cnf, Edge constraint) {
 	printCNF(constraint);
 	model_print("\n******************************\n");
 #endif
-	
+
 	Edge cnfform = simplifyCNF(cnf, constraint);
 	freeEdgeRec(constraint);
 	outputCNF(cnf, cnfform);
@@ -829,12 +699,13 @@ int solveCNF(CNF *cnf) {
 	long long startTime = getTimeNano();
 	finishedClauses(cnf->solver);
 	long long startSolve = getTimeNano();
+	model_print("#Clauses = %u\t#Vars = %u\n", cnf->clausecount, cnf->varcount);
 	int result = cnf->unsat ? IS_UNSAT : solve(cnf->solver);
 	long long finishTime = getTimeNano();
 	cnf->encodeTime = startSolve - startTime;
 	model_print("CNF Encode time: %f\n", cnf->encodeTime / 1000000000.0);
 	cnf->solveTime = finishTime - startSolve;
-	model_print("Solve time: %f\n", cnf->solveTime / 1000000000.0);
+	model_print("SAT Solving time: %f\n", cnf->solveTime / 1000000000.0);
 	return result;
 }
 
@@ -932,6 +803,10 @@ 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....
+}
+
 Edge generateEquivNVConstraint(CNF *cnf, uint numvars, Edge *var1, Edge *var2) {
 	if (numvars == 0)
 		return E_True;