From e614433d3bf18a98e9f20e64d404af6662c8e069 Mon Sep 17 00:00:00 2001 From: Michael Schroeder Date: Mon, 12 Jan 2009 14:46:57 +0100 Subject: [PATCH] - add solver_findallproblemrules function - fix some comments --- src/solver.c | 30 ++++++++++++++++++++++++++---- src/solver.h | 2 ++ 2 files changed, 28 insertions(+), 4 deletions(-) diff --git a/src/solver.c b/src/solver.c index 39e7884..fd547d5 100644 --- a/src/solver.c +++ b/src/solver.c @@ -777,7 +777,7 @@ makeruledecisions(Solver *solv) * enable/disable learnt rules * * we have enabled or disabled some of our rules. We now reenable all - * of our learnt rules but the ones that were learnt from rules that + * of our learnt rules except the ones that were learnt from rules that * are now disabled. */ static void @@ -837,7 +837,7 @@ enableweakrules(Solver *solv) for (i = 1, r = solv->rules + i; i < solv->learntrules; i++, r++) { - if (r->d >= 0) /* skip non-direct literals */ + if (r->d >= 0) /* already enabled? */ continue; if (!MAPTST(&solv->weakrulemap, i)) continue; @@ -847,7 +847,7 @@ enableweakrules(Solver *solv) /* FIXME: bad code ahead, replace as soon as possible */ -/* FIXME: should probably look at SOLVER_INSTALL|SOLVABLE_ONE_OF */ +/* FIXME: maybe also look at SOLVER_INSTALL|SOLVABLE_ONE_OF */ /*------------------------------------------------------------------- * disable update rules @@ -2269,7 +2269,7 @@ setpropagatelearn(Solver *solv, int level, Id decision, int disablerules, Id rul POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l); level = l; revert(solv, level); - r = addrule(solv, p, d); /* p requires d */ + r = addrule(solv, p, d); assert(r); assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules); queue_push(&solv->learnt_why, why); @@ -4025,6 +4025,28 @@ solver_findproblemrule(Solver *solv, Id problem) assert(0); } +static void +findallproblemrules_internal(Solver *solv, Id idx, Queue *rules) +{ + Id rid; + while ((rid = solv->learnt_pool.elements[idx++]) != 0) + { + if (rid >= solv->learntrules) + { + findallproblemrules_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], rules); + continue; + } + queue_pushunique(rules, rid); + } +} + +void +solver_findallproblemrules(Solver *solv, Id problem, Queue *rules) +{ + queue_empty(rules); + findallproblemrules_internal(solv, solv->problems.elements[problem - 1], rules); +} + /*------------------------------------------------------------------- * diff --git a/src/solver.h b/src/solver.h index d3757eb..b8f0c38 100644 --- a/src/solver.h +++ b/src/solver.h @@ -274,6 +274,8 @@ extern Id solver_next_problem(Solver *solv, Id problem); extern Id solver_next_solution(Solver *solv, Id problem, Id solution); extern Id solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp); extern Id solver_findproblemrule(Solver *solv, Id problem); +extern void solver_findallproblemrules(Solver *solv, Id problem, Queue *rules); + extern SolverProbleminfo solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp); /* XXX: why is this not static? */ -- 2.7.4