Extend test case to call solver

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index a6d9dcc3abf58fbae01ba4d4774a675e222cae56..340cdd0b3ed8735d4f6a38f3ff7b081a82f45168 100644 (file)
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -19,7 +19,8 @@ CNF * createCNF() {
        cnf->enableMatching=true;
        allocInlineDefVectorEdge(& cnf->constraints);
        allocInlineDefVectorEdge(& cnf->args);
- return cnf;
+       cnf->solver=allocIncrementalSolver();
+       return cnf;
 }
 
 void deleteCNF(CNF * cnf) {
@@ -30,6 +31,7 @@ void deleteCNF(CNF * cnf) {
        }
        deleteVectorArrayEdge(& cnf->constraints);
        deleteVectorArrayEdge(& cnf->args);
+       deleteIncrementalSolver(cnf->solver);
        ourfree(cnf->node_array);
        ourfree(cnf);
 }
@@ -275,6 +277,13 @@ Edge constraintNewVar(CNF *cnf) {
        return e;
 }
 
+void solveCNF(CNF *cnf) {
+       countPass(cnf);
+       convertPass(cnf, false);
+       solve(cnf->solver);
+}
+
+
 void countPass(CNF *cnf) {
        uint numConstraints=getSizeVectorEdge(&cnf->constraints);
        VectorEdge *ve=allocDefVectorEdge();

diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index aff2c35b63baec4474ade034030352c02b30e60b..95ee530ab880f9f2b2f3b9b04ae37e31d5a6d480 100644 (file)
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -191,7 +191,7 @@ Edge constraintNewVar(CNF *cnf);
 void countPass(CNF *cnf);
 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
 void addConstraint(CNF *cnf, Edge constraint);
-
+void solveCNF(CNF *cnf);
 
 
 void convertPass(CNF *cnf, bool backtrackLit);

diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index 68e2104cc38b0b1de55d89f54a6e562212f29420..82f926de0b4cdfe63bc2f761f6868fa7add3c6d0 100644 (file)
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -12,5 +12,6 @@ int main(int numargs, char ** argv) {
        Edge iff3=constraintIFF(cnf, v3, nv1);
        Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
        addConstraint(cnf, cand);
+       solveCNF(cnf);
        deleteCNF(cnf);
 }