From 3a2ee742f45374214c2c0aa98308f567566f74ae Mon Sep 17 00:00:00 2001 From: Stefan Schubert Date: Fri, 16 Nov 2007 08:27:24 +0000 Subject: [PATCH] logging --- src/solver.c | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/solver.c b/src/solver.c index 7bb44c6..b28d985 100644 --- a/src/solver.c +++ b/src/solver.c @@ -1233,6 +1233,9 @@ propagate(Solver *solv, int level) Id *decisionmap = solv->decisionmap; Id *watches = solv->watches + pool->nsolvables; + if (solv->pool->verbose > 3) + printf ("----- propagate -----\n"); + while (solv->propagate_index < solv->decisionq.count) { /* negate because our watches trigger if literal goes FALSE */ @@ -1326,6 +1329,9 @@ propagate(Solver *solv, int level) } } } + if (solv->pool->verbose > 3) + printf ("----- propagate end-----\n"); + return 0; /* all is well */ } @@ -1989,6 +1995,8 @@ run_solver(Solver *solv, int disablerules, int doweak) makewatches(solv); if (pool->verbose) printf("initial decisions: %d\n", solv->decisionq.count); + if (pool->verbose > 3) + printdecisions (solv); /* start SAT algorithm */ level = 1; @@ -2004,7 +2012,7 @@ run_solver(Solver *solv, int disablerules, int doweak) if (level == 1) { - if (pool->verbose) printf("propagating (%d %d)...\n", solv->propagate_index, solv->decisionq.count); + if (pool->verbose) printf("propagating (propagate_index: %d; size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count); if ((r = propagate(solv, level)) != 0) { if (analyze_unsolvable(solv, r, disablerules)) -- 2.7.4