more edits

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index f4130ebd0bf758c0404b60e3bf6798616b470433..801351dcf42d764bec29e84b2b2268177e878ad7 100644 (file)
--- 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 0f2fedf9aaf2fab58346a9c5750f5decb0e25889..559c05822732b6f694ef96ec973f80c1440c259e 100644 (file)
--- 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);