From 0d23f25215c2f649ef910c1937ec7edd264b6d84 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Sat, 8 Jul 2017 00:14:06 -0700
Subject: [PATCH] more edits

---
 src/Backend/nodeedge.c | 25 ++++++++++++++-----------
 src/Backend/nodeedge.h |  3 ++-
 2 files changed, 16 insertions(+), 12 deletions(-)

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index f4130eb..801351d 100644
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -18,6 +18,7 @@ CNF * createCNF() {
 	cnf->maxsize=(uint)(((double)cnf->capacity)*LOAD_FACTOR);
 	cnf->enableMatching=true;
 	allocInlineDefVectorEdge(& cnf->constraints);
+	allocInlineDefVectorEdge(& cnf->args);
  return cnf;
 }
 
@@ -28,6 +29,7 @@ void deleteCNF(CNF * cnf) {
 			ourfree(n);
 	}
 	deleteVectorArrayEdge(& cnf->constraints);
+	deleteVectorArrayEdge(& cnf->args);
 	ourfree(cnf->node_array);
 	ourfree(cnf);
 }
@@ -562,8 +564,8 @@ void outputCNF(CNF *cnf, CNFExpr *exp) {
 	
 }
 
-CNFExpr* fillArgs(Edge e, bool isNeg, Edge * largestEdge, VectorEdge * args) {
-	args.clear();
+CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
+	clearVectorEdge(&cnf->args);
 
 	*largestEdge = (void*) NULL;
 	CNFExpr* largest = NULL;
@@ -573,7 +575,7 @@ CNFExpr* fillArgs(Edge e, bool isNeg, Edge * largestEdge, VectorEdge * args) {
 		Node * narg = getNodePtrFromEdge(arg);
 		
 		if (arg.isVar()) {
-			args.push(arg);
+			pushVectorEdge(&cnf->args, arg);
 			continue;
 		}
 		
@@ -589,14 +591,14 @@ CNFExpr* fillArgs(Edge e, bool isNeg, Edge * largestEdge, VectorEdge * args) {
 					* largestEdge = arg;
 					continue;
 				} else if (argExp->litSize > largest->litSize) {
-					args.push(* largestEdge);
+					pushVectorEdge(&cnf->args, *largestEdge);
 					largest = argExp;
 					* largestEdge = arg;
 					continue;
 				}
 			}
 		}
-		args.push(arg);
+		pushVectorEdge(&cnf->args, arg);
 	}
 	
 	if (largest != NULL) {
@@ -609,12 +611,13 @@ CNFExpr* fillArgs(Edge e, bool isNeg, Edge * largestEdge, VectorEdge * args) {
 
 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
 	Edge largestEdge;
-	CNFExpr* accum = fillArgs(e, false, largestEdge);
+	
+	CNFExpr* accum = fillArgs(cnf, e, false, &largestEdge);
 	if (accum == NULL) accum = allocCNFExprBool(true);
 	
-	int i = _args.size();
+	int i = getSizeVectorEdge(&cnf->args);
 	while (i != 0) {
-		Edge arg(_args[--i]);
+		Edge arg = getVectorEdge(&cnf->args, --i);
 		if (arg.isVar()) {
 			accum->conjoin(atomLit(arg));
 		} else {
@@ -637,7 +640,7 @@ CNFExpr * produceConjunction(CNF * cnf, Edge e) {
 
 CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
 	Edge largestEdge;
-	CNFExpr* accum = fillArgs(e, true, largestEdge);
+	CNFExpr* accum = fillArgs(cnf, e, true, &largestEdge);
 	if (accum == NULL)
 		accum = allocCNFExprBool(false);
 	
@@ -655,9 +658,9 @@ CNFExpr* produceDisjunction(CNF *cnf, Edge e) {
 	if (accum->clauseSize() > CLAUSE_MAX)
 		accum = allocCNFExprLiteral(introProxy(cnf, largestEdge, accum, isNegEdge(largestEdge)));
 	
-	int i = _args.size();
+	int i = getSizeVectorEdge(&cnf->args);
 	while (i != 0) {
-		Edge arg(_args[--i]);
+		Edge arg=getVectorEdge(&cnf->args, --i);
 		Node *narg=getNodePtrFromEdge(arg);
 		if (arg.isVar()) {
 			accum->disjoin(atomLit(arg));
diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index 0f2fedf..559c058 100644
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -62,6 +62,7 @@ struct CNF {
 	Node ** node_array;
 	IncrementalSolver * solver;
 	VectorEdge constraints;
+	VectorEdge args;
 };
 
 typedef struct CNF CNF;
@@ -190,7 +191,7 @@ CNFExpr * produceConjunction(CNF * cnf, Edge e);
 CNFExpr* produceDisjunction(CNF *cnf, Edge e);
 bool propagate(CNF *cnf, CNFExpr * dest, CNFExpr * src, bool negate);
 void saveCNF(CNF *cnf, CNFExpr* exp, Edge e, bool sign);
-CNFExpr* fillArgs(Edge e, bool isNeg, Edge * largestEdge, VectorEdge * args);
+CNFExpr* fillArgs(CNF * cnf, Edge e, bool isNeg, Edge * largestEdge);
 
 
 
-- 
2.34.1