From 39dfec97bcfc3292f72bd4489668cb64ba63e617 Mon Sep 17 00:00:00 2001 From: Michael Schroeder Date: Fri, 24 Jul 2009 20:04:10 +0200 Subject: [PATCH] - make installed packages pass much faster - disable classes of choice rules - add solver_printdecisionq() debug function --- src/rules.c | 39 ++++++++++++++++++++++++++++++++++++- src/solver.c | 58 +++++++++++++++++++++++++++++++++++++++++++------------ src/solver.h | 1 + src/solverdebug.c | 33 ++++++++++++++++++++++++++++++- src/solverdebug.h | 1 + 5 files changed, 118 insertions(+), 14 deletions(-) diff --git a/src/rules.c b/src/rules.c index 5a186da..0069e75 100644 --- a/src/rules.c +++ b/src/rules.c @@ -1788,6 +1788,7 @@ addchoicerules(Solver *solv) solv->choicerules_end = solv->nrules; return; } + solv->choicerules_ref = sat_calloc(solv->rpmrules_end, sizeof(Id)); queue_init(&q); for (rid = 1; rid < solv->rpmrules_end ; rid++) { @@ -1871,10 +1872,46 @@ addchoicerules(Solver *solv) d = q.count ? pool_queuetowhatprovides(pool, &q) : 0; solver_addrule(solv, r->p, d); queue_push(&solv->weakruleq, solv->nrules - 1); - /* solver_printrule(solv, SAT_DEBUG_RESULT, solv->rules + solv->nrules - 1); */ + solv->choicerules_ref[solv->nrules - 1 - solv->choicerules] = rid; +#if 0 + printf("OLD "); + solver_printrule(solv, SAT_DEBUG_RESULT, solv->rules + rid); + printf("WEAK CHOICE "); + solver_printrule(solv, SAT_DEBUG_RESULT, solv->rules + solv->nrules - 1); +#endif } queue_free(&q); solv->choicerules_end = solv->nrules; } +void +disablechoicerules(Solver *solv, Rule *r) +{ + Id rid, p, *pp; + Pool *pool = solv->pool; + Map m; + Rule *or; + + or = solv->rules + solv->choicerules_ref[(r - solv->rules) - solv->choicerules]; + map_init(&m, pool->nsolvables); + FOR_RULELITERALS(p, pp, or) + if (p > 0) + MAPSET(&m, p); + FOR_RULELITERALS(p, pp, r) + if (p > 0) + MAPCLR(&m, p); + for (rid = solv->choicerules; rid < solv->choicerules_end; rid++) + { + r = solv->rules + rid; + if (r->d < 0) + continue; + or = solv->rules + solv->choicerules_ref[(r - solv->rules) - solv->choicerules]; + FOR_RULELITERALS(p, pp, or) + if (p > 0 && MAPTST(&m, p)) + break; + if (p) + solver_disablerule(solv, r); + } +} + /* EOF */ diff --git a/src/solver.c b/src/solver.c index 206be13..98f8dd0 100644 --- a/src/solver.c +++ b/src/solver.c @@ -975,6 +975,7 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules) if (lastweak) { Id v; + extern void disablechoicerules(Solver *solv, Rule *r); /* disable last weak rule */ solv->problems.count = oldproblemcount; solv->learnt_pool.count = oldlearntpoolcount; @@ -984,6 +985,8 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules) v = lastweak; POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling "); solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, solv->rules + lastweak); + if (lastweak >= solv->choicerules && lastweak < solv->choicerules_end) + disablechoicerules(solv, solv->rules + lastweak); solver_disableproblem(solv, v); if (v < 0) solver_reenablepolicyrules(solv, -(v + 1)); @@ -1299,6 +1302,7 @@ solver_free(Solver *solv) sat_free(solv->obsoletes); sat_free(solv->obsoletes_data); sat_free(solv->multiversionupdaters); + sat_free(solv->choicerules_ref); sat_free(solv); } @@ -1324,6 +1328,7 @@ solver_run_sat(Solver *solv, int disablerules, int doweak) Pool *pool = solv->pool; Id p, *dp; int minimizationsteps; + int installedpos = solv->installed ? solv->installed->start : 0; IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION) { @@ -1340,7 +1345,7 @@ solver_run_sat(Solver *solv, int disablerules, int doweak) /* start SAT algorithm */ level = 1; systemlevel = level + 1; - POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n"); + POOL_DEBUG(SAT_DEBUG_SOLVER, "solving...\n"); queue_init(&dq); queue_init(&dqs); @@ -1362,7 +1367,6 @@ solver_run_sat(Solver *solv, int disablerules, int doweak) /* * propagate */ - if (level == 1) { POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d; size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count); @@ -1441,21 +1445,30 @@ solver_run_sat(Solver *solv, int disablerules, int doweak) Repo *installed = solv->installed; int pass; + POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving installed packages\n"); /* we use two passes if we need to update packages * to create a better user experience */ for (pass = solv->updatemap.size ? 0 : 1; pass < 2; pass++) { - FOR_REPO_SOLVABLES(installed, i, s) + int passlevel = level; + /* start with installedpos, the position that gave us problems last time */ + for (i = installedpos, n = installed->start; n < installed->end; i++, n++) { Rule *rr; Id d; + if (i == installed->end) + i = installed->start; + s = pool->solvables + i; + if (s->repo != installed) + continue; + + if (solv->decisionmap[i] > 0) + continue; /* XXX: noupdate check is probably no longer needed, as all jobs should * already be satisfied */ if (MAPTST(&solv->noupdate, i - installed->start)) continue; - if (solv->decisionmap[i] > 0) - continue; if (!pass && solv->updatemap.size && !MAPTST(&solv->updatemap, i - installed->start)) continue; /* updates first */ r = solv->rules + solv->updaterules + (i - installed->start); @@ -1517,7 +1530,15 @@ solver_run_sat(Solver *solv, int disablerules, int doweak) return; } if (level <= olevel) - break; + { + if (level < passlevel) + break; /* trouble */ + if (level < olevel) + n = installed->start; /* redo all */ + i--; + n--; + continue; + } } /* if still undecided keep package */ if (solv->decisionmap[i] == 0) @@ -1532,11 +1553,23 @@ solver_run_sat(Solver *solv, int disablerules, int doweak) return; } if (level <= olevel) - break; + { + if (level < passlevel) + break; /* trouble */ + if (level < olevel) + n = installed->start; /* redo all */ + i--; + n--; + continue; /* retry with learnt rule */ + } } } - if (i < installed->end) - break; + if (n < installed->end) + { + installedpos = i; /* retry problem solvable next time */ + break; /* ran into trouble */ + } + installedpos = installed->start; /* reset installedpos */ } systemlevel = level + 1; if (pass < 2) @@ -1551,10 +1584,8 @@ solver_run_sat(Solver *solv, int disablerules, int doweak) */ POOL_DEBUG(SAT_DEBUG_POLICY, "deciding unresolved rules\n"); - for (i = 1, n = 1; ; i++, n++) + for (i = 1, n = 1; n < solv->nrules; i++, n++) { - if (n == solv->nrules) - break; if (i == solv->nrules) i = 1; r = solv->rules + i; @@ -2005,6 +2036,9 @@ solver_run_sat(Solver *solv, int disablerules, int doweak) POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n"); queue_free(&dq); queue_free(&dqs); +#if 0 + solver_printdecisionq(solv, SAT_DEBUG_RESULT); +#endif } diff --git a/src/solver.h b/src/solver.h index 91a7664..5b3884e 100644 --- a/src/solver.h +++ b/src/solver.h @@ -76,6 +76,7 @@ typedef struct _Solver { Id choicerules; /* choice rules (always weak) */ Id choicerules_end; + Id *choicerules_ref; Id learntrules; /* learnt rules, (end == nrules) */ diff --git a/src/solverdebug.c b/src/solverdebug.c index ee43212..48cfaba 100644 --- a/src/solverdebug.c +++ b/src/solverdebug.c @@ -203,7 +203,7 @@ solver_printruleclass(Solver *solv, int type, Rule *r) if (p < solv->learntrules) if (MAPTST(&solv->weakrulemap, p)) POOL_DEBUG(type, "WEAK "); - if (p >= solv->learntrules) + if (solv->learntrules && p >= solv->learntrules) POOL_DEBUG(type, "LEARNT "); else if (p >= solv->choicerules && p < solv->choicerules_end) POOL_DEBUG(type, "CHOICE "); @@ -256,6 +256,37 @@ solver_printwatches(Solver *solv, int type) POOL_DEBUG(type, " solvable [%d] -- rule [%d]\n", counter, solv->watches[counter + pool->nsolvables]); } +void +solver_printdecisionq(Solver *solv, int type) +{ + Pool *pool = solv->pool; + int i; + Id p, why; + + POOL_DEBUG(type, "Decisions:\n"); + for (i = 0; i < solv->decisionq.count; i++) + { + p = solv->decisionq.elements[i]; + if (p > 0) + POOL_DEBUG(type, "%d %d install %s, ", i, solv->decisionmap[p], solvid2str(pool, p)); + else + POOL_DEBUG(type, "%d %d conflict %s, ", i, -solv->decisionmap[-p], solvid2str(pool, -p)); + why = solv->decisionq_why.elements[i]; + if (why > 0) + { + POOL_DEBUG(type, "forced by "); + solver_printruleclass(solv, type, solv->rules + why); + } + else if (why < 0) + { + POOL_DEBUG(type, "chosen from "); + solver_printruleclass(solv, type, solv->rules - why); + } + else + POOL_DEBUG(type, "picked for some unknown reason.\n"); + } +} + /* * printdecisions */ diff --git a/src/solverdebug.h b/src/solverdebug.h index 8b2feec..50fff6b 100644 --- a/src/solverdebug.h +++ b/src/solverdebug.h @@ -23,6 +23,7 @@ extern void solver_printrule(Solver *solv, int type, Rule *r); extern void solver_printruleclass(Solver *solv, int type, Rule *r); extern void solver_printproblem(Solver *solv, Id v); extern void solver_printwatches(Solver *solv, int type); +extern void solver_printdecisionq(Solver *solv, int type); extern void solver_printdecisions(Solver *solv); extern void solver_printtransaction(Solver *solv); extern void solver_printprobleminfo(Solver *solv, Id problem); -- 2.7.4