From d9d7d7c2506ddf5536ed275e700f9fa7cbb18b1c Mon Sep 17 00:00:00 2001 From: Michael Schroeder Date: Thu, 2 Nov 2017 16:21:38 +0100 Subject: [PATCH] Refactor problem handling --- src/problems.c | 144 ++++++++++++++++++++-- src/problems.h | 4 + src/solver.c | 329 ++++++++++++------------------------------------- 3 files changed, 217 insertions(+), 260 deletions(-) diff --git a/src/problems.c b/src/problems.c index 2b5ef53a..f60671cf 100644 --- a/src/problems.c +++ b/src/problems.c @@ -24,6 +24,140 @@ #include "evr.h" #include "solverdebug.h" +/* turn a problem rule into a problem id by normalizing it */ +static Id +solver_ruletoproblem(Solver *solv, Id rid) +{ + if (rid >= solv->jobrules && rid < solv->jobrules_end) + rid = -(solv->ruletojob.elements[rid - solv->jobrules] + 1); + else if (rid >= solv->bestrules && rid < solv->bestrules_up && solv->bestrules_pkg[rid - solv->bestrules] < 0) + rid = -(solv->ruletojob.elements[-solv->bestrules_pkg[rid - solv->bestrules] - solv->jobrules] + 1); + else if (rid > solv->infarchrules && rid < solv->infarchrules_end) + { + Pool *pool = solv->pool; + Id name = pool->solvables[-solv->rules[rid].p].name; + while (rid > solv->infarchrules && pool->solvables[-solv->rules[rid - 1].p].name == name) + rid--; + } + else if (rid > solv->duprules && rid < solv->duprules_end) + { + Pool *pool = solv->pool; + Id name = pool->solvables[-solv->rules[rid].p].name; + while (rid > solv->duprules && pool->solvables[-solv->rules[rid - 1].p].name == name) + rid--; + } + return rid; +} + +/* when the solver runs into a problem, it needs to disable all + * involved non-pkg rules and record the rules for solution + * generation. + */ +void +solver_recordproblem(Solver *solv, Id rid) +{ + Id v = solver_ruletoproblem(solv, rid); + /* return if problem already countains our rule */ + if (solv->problems.count) + { + int i; + for (i = solv->problems.count - 1; i >= 0; i--) + if (solv->problems.elements[i] == 0) /* end of last problem reached? */ + break; + else if (solv->problems.elements[i] == v) + return; + } + queue_push(&solv->problems, v); +} + +/* this is called when a problem is solved by disabling a rule. + * It calls disableproblem and then re-enables policy rules */ +void +solver_fixproblem(Solver *solv, Id rid) +{ + Id v = solver_ruletoproblem(solv, rid); + solver_disableproblem(solv, v); + if (v < 0) + solver_reenablepolicyrules(solv, -v); +} + +/* try to fix a problem by auto-uninstalling packages */ +Id +solver_autouninstall(Solver *solv, Id *problem) +{ + Pool *pool = solv->pool; + int i; + int lastfeature = 0, lastupdate = 0; + Id v; + Id extraflags = -1; + Map *m = 0; + + if (!solv->allowuninstall && !solv->allowuninstall_all) + { + if (!solv->allowuninstallmap.size) + return 0; /* why did we get called? */ + m = &solv->allowuninstallmap; + } + for (i = 0; (v = problem[i]) != 0; i++) + { + if (v < 0) + extraflags &= solv->job.elements[-v - 1]; + if (v >= solv->updaterules && v < solv->updaterules_end) + { + Rule *r; + if (m && !MAPTST(m, v - solv->updaterules)) + continue; + /* check if identical to feature rule, we don't like that (except for orphans) */ + r = solv->rules + solv->featurerules + (v - solv->updaterules); + if (!r->p) + { + /* update rule == feature rule */ + if (v > lastfeature) + lastfeature = v; + /* prefer orphaned packages in dup mode */ + if (solv->keep_orphans) + { + r = solv->rules + v; + if (!r->d && !r->w2 && r->p == (solv->installed->start + (v - solv->updaterules))) + { + lastfeature = v; + lastupdate = 0; + break; + } + } + continue; + } + if (v > lastupdate) + lastupdate = v; + } + } + if (!lastupdate && !lastfeature) + return 0; + v = lastupdate ? lastupdate : lastfeature; + POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "allowuninstall disabling "); + solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, solv->rules + v); + /* should really be solver_fixproblem, but we know v is an update/feature rule */ + solver_disableproblem(solv, v); + if (extraflags != -1 && (extraflags & SOLVER_CLEANDEPS) != 0 && solv->cleandepsmap.size) + { + /* add the package to the updatepkgs list, this will automatically turn + * on cleandeps mode */ + Id p = solv->rules[v].p; + if (!solv->cleandeps_updatepkgs) + { + solv->cleandeps_updatepkgs = solv_calloc(1, sizeof(Queue)); + queue_init(solv->cleandeps_updatepkgs); + } + if (p > 0) + { + int oldupdatepkgscnt = solv->cleandeps_updatepkgs->count; + queue_pushunique(solv->cleandeps_updatepkgs, p); + if (solv->cleandeps_updatepkgs->count != oldupdatepkgscnt) + solver_disablepolicyrules(solv); + } + } + return v; +} /**********************************************************************************/ @@ -61,16 +195,6 @@ solver_disableproblem(Solver *solv, Id v) return; } solver_disablerule(solv, solv->rules + v); -#if 0 - /* XXX: doesn't work */ - if (v >= solv->updaterules && v < solv->updaterules_end) - { - /* enable feature rule if we disabled the update rule */ - r = solv->rules + (v - solv->updaterules + solv->featurerules); - if (r->p) - solver_enablerule(solv, r); - } -#endif return; } v = -(v + 1); diff --git a/src/problems.h b/src/problems.h index e5b2279f..395b71c1 100644 --- a/src/problems.h +++ b/src/problems.h @@ -28,6 +28,10 @@ struct _Solver; #define SOLVER_SOLUTION_BEST (-3) #define SOLVER_SOLUTION_POOLJOB (-4) +void solver_recordproblem(struct _Solver *solv, Id rid); +void solver_fixproblem(struct _Solver *solv, Id rid); +Id solver_autouninstall(struct _Solver *solv, Id *problem); + void solver_disableproblem(struct _Solver *solv, Id v); void solver_enableproblem(struct _Solver *solv, Id v); int solver_prepare_solutions(struct _Solver *solv); diff --git a/src/solver.c b/src/solver.c index 1339a5bb..6129cf21 100644 --- a/src/solver.c +++ b/src/solver.c @@ -31,82 +31,6 @@ #define RULES_BLOCK 63 -static Id -autouninstall(Solver *solv, Id *problem) -{ - Pool *pool = solv->pool; - int i; - int lastfeature = 0, lastupdate = 0; - Id v; - Id extraflags = -1; - Map *m = 0; - - if (!solv->allowuninstall && !solv->allowuninstall_all) - { - if (!solv->allowuninstallmap.size) - return 0; /* why did we get called? */ - m = &solv->allowuninstallmap; - } - for (i = 0; (v = problem[i]) != 0; i++) - { - if (v < 0) - extraflags &= solv->job.elements[-v - 1]; - if (v >= solv->updaterules && v < solv->updaterules_end) - { - Rule *r; - if (m && !MAPTST(m, v - solv->updaterules)) - continue; - /* check if identical to feature rule, we don't like that (except for orphans) */ - r = solv->rules + solv->featurerules + (v - solv->updaterules); - if (!r->p) - { - /* update rule == feature rule */ - if (v > lastfeature) - lastfeature = v; - /* prefer orphaned packages in dup mode */ - if (solv->keep_orphans) - { - r = solv->rules + v; - if (!r->d && !r->w2 && r->p == (solv->installed->start + (v - solv->updaterules))) - { - lastfeature = v; - lastupdate = 0; - break; - } - } - continue; - } - if (v > lastupdate) - lastupdate = v; - } - } - if (!lastupdate && !lastfeature) - return 0; - v = lastupdate ? lastupdate : lastfeature; - POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "allowuninstall disabling "); - solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, solv->rules + v); - solver_disableproblem(solv, v); - if (extraflags != -1 && (extraflags & SOLVER_CLEANDEPS) != 0 && solv->cleandepsmap.size) - { - /* add the package to the updatepkgs list, this will automatically turn - * on cleandeps mode */ - Id p = solv->rules[v].p; - if (!solv->cleandeps_updatepkgs) - { - solv->cleandeps_updatepkgs = solv_calloc(1, sizeof(Queue)); - queue_init(solv->cleandeps_updatepkgs); - } - if (p > 0) - { - int oldupdatepkgscnt = solv->cleandeps_updatepkgs->count; - queue_pushunique(solv->cleandeps_updatepkgs, p); - if (solv->cleandeps_updatepkgs->count != oldupdatepkgscnt) - solver_disablepolicyrules(solv); - } - } - return v; -} - /************************************************************************/ /* @@ -164,17 +88,18 @@ enabledisablelearntrules(Solver *solv) * If we find a conflict, disable rules and add them to problem queue. */ -static void -makeruledecisions(Solver *solv) +static int +makeruledecisions(Solver *solv, int disablerules) { Pool *pool = solv->pool; - int i, ri, ii; + int i, ri, ii, ori; Rule *r, *rr; Id v, vv; int decisionstart; int record_proof = 1; int oldproblemcount; int havedisabled = 0; + int doautouninstall; /* The system solvable is always installed first */ assert(solv->decisionq.count == 0); @@ -260,8 +185,7 @@ makeruledecisions(Solver *solv) } POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ASSERTION ----------------------\n"); - IF_POOLDEBUG (SOLV_DEBUG_UNSOLVABLE) - solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, solv->rules + ri); + assert(ri >= solv->pkgrules_end); /* must not have a conflict in the pkg rules! */ /* * find the decision which is the "opposite" of the rule @@ -271,142 +195,94 @@ makeruledecisions(Solver *solv) break; assert(i < solv->decisionq.count); /* assert that we found it */ oldproblemcount = solv->problems.count; + queue_push(&solv->problems, 0); - /* - * conflict with system solvable ? - */ if (v == -SYSTEMSOLVABLE) + ori = 0; + else { - if (record_proof) - { - queue_push(&solv->problems, solv->learnt_pool.count); - queue_push(&solv->learnt_pool, ri); - queue_push(&solv->learnt_pool, 0); - } - else - queue_push(&solv->problems, 0); - POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "conflict with system solvable, disabling rule #%d\n", ri); - if (ri >= solv->jobrules && ri < solv->jobrules_end) - v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1); - else if (ri >= solv->bestrules && ri < solv->bestrules_up && solv->bestrules_pkg[ri - solv->bestrules] < 0) - v = -(solv->ruletojob.elements[-solv->bestrules_pkg[ri - solv->bestrules] - solv->jobrules] + 1); - else - v = ri; - queue_push(&solv->problems, v); - queue_push(&solv->problems, 0); - if (v >= solv->featurerules && v < solv->updaterules_end) - { - if (solv->allowuninstall || solv->allowuninstall_all || solv->allowuninstallmap.size) - if (autouninstall(solv, solv->problems.elements + oldproblemcount + 1) != 0) - { - solv->problems.count = oldproblemcount; - havedisabled = 1; - break; /* start over */ - } - } - solver_disableproblem(solv, v); - havedisabled = 1; - break; /* start over */ + ori = solv->decisionq_why.elements[i]; /* the conflicting rule */ + assert(ori > 0); } - assert(solv->decisionq_why.elements[i] > 0); - IF_POOLDEBUG (SOLV_DEBUG_UNSOLVABLE) - solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, solv->rules + solv->decisionq_why.elements[i]); - /* - * conflict with a pkg rule ? + * conflict with system solvable or pkg rule? */ - if (solv->decisionq_why.elements[i] < solv->pkgrules_end) + doautouninstall = 0; + if (ori < solv->pkgrules_end) { - if (record_proof) + assert(v > 0 || v == -SYSTEMSOLVABLE); + IF_POOLDEBUG (SOLV_DEBUG_UNSOLVABLE) { - queue_push(&solv->problems, solv->learnt_pool.count); - queue_push(&solv->learnt_pool, ri); - queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]); - queue_push(&solv->learnt_pool, 0); + if (ori) + POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "conflict with pkg rule, disabling rule #%d\n", ri); + else + POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "conflict with system solvable, disabling rule #%d\n", ri); + solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, solv->rules + ri); + if (ori) + solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, solv->rules + ori); } - else - queue_push(&solv->problems, 0); - assert(v > 0 || v == -SYSTEMSOLVABLE); - POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "conflict with pkg rule, disabling rule #%d\n", ri); - if (ri >= solv->jobrules && ri < solv->jobrules_end) - v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1); - else if (ri >= solv->bestrules && ri < solv->bestrules_up && solv->bestrules_pkg[ri - solv->bestrules] < 0) - v = -(solv->ruletojob.elements[-solv->bestrules_pkg[ri - solv->bestrules] - solv->jobrules] + 1); - else - v = ri; - queue_push(&solv->problems, v); - queue_push(&solv->problems, 0); - if (v >= solv->featurerules && v < solv->updaterules_end) + solver_recordproblem(solv, ri); + if (ri >= solv->featurerules && ri < solv->updaterules_end) + doautouninstall = 1; + } + else + { + POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "conflicting update/job assertions over literal %d\n", vv); + /* + * push all of our rules (can only be feature or job rules) + * asserting this literal on the problem stack + */ + for (i = solv->pkgrules_end, rr = solv->rules + i; i < solv->learntrules; i++, rr++) { - if (solv->allowuninstall || solv->allowuninstall_all || solv->allowuninstallmap.size) - if (autouninstall(solv, solv->problems.elements + oldproblemcount + 1) != 0) - { - solv->problems.count = oldproblemcount; - havedisabled = 1; - break; /* start over */ - } + if (rr->d < 0 /* disabled */ + || rr->w2) /* or no assertion */ + continue; + if (rr->p != vv /* not affecting the literal */ + && rr->p != -vv) + continue; + if (solv->weakrulemap.size && MAPTST(&solv->weakrulemap, i)) /* weak: silently ignore */ + continue; + + POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, " - disabling rule #%d\n", i); + solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, solv->rules + i); + solver_recordproblem(solv, i); + if (i >= solv->featurerules && i < solv->updaterules_end) + doautouninstall = 1; } - solver_disableproblem(solv, v); - havedisabled = 1; - break; /* start over */ } + queue_push(&solv->problems, 0); - /* - * conflict with another job or update/feature rule - */ + if (doautouninstall) + { + if (solv->allowuninstall || solv->allowuninstall_all || solv->allowuninstallmap.size) + if (solver_autouninstall(solv, solv->problems.elements + oldproblemcount + 1) != 0) + { + solv->problems.count = oldproblemcount; + havedisabled = 1; + break; /* start over */ + } + } - /* record proof */ + /* record the proof if requested */ if (record_proof) { - queue_push(&solv->problems, solv->learnt_pool.count); + solv->problems.elements[oldproblemcount] = solv->learnt_pool.count; queue_push(&solv->learnt_pool, ri); - queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]); + if (ori) + queue_push(&solv->learnt_pool, ori); queue_push(&solv->learnt_pool, 0); } - else - queue_push(&solv->problems, 0); - - POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "conflicting update/job assertions over literal %d\n", vv); - /* - * push all of our rules (can only be feature or job rules) - * asserting this literal on the problem stack - */ - for (i = solv->featurerules, rr = solv->rules + i; i < solv->learntrules; i++, rr++) + if (!disablerules) { - if (rr->d < 0 /* disabled */ - || rr->w2) /* or no assertion */ - continue; - if (rr->p != vv /* not affecting the literal */ - && rr->p != -vv) - continue; - if (solv->weakrulemap.size && MAPTST(&solv->weakrulemap, i)) /* weak: silently ignore */ - continue; - - POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, " - disabling rule #%d\n", i); - solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, solv->rules + i); - - if (i >= solv->jobrules && i < solv->jobrules_end) - v = -(solv->ruletojob.elements[i - solv->jobrules] + 1); - else if (i >= solv->bestrules && i < solv->bestrules_up && solv->bestrules_pkg[i - solv->bestrules] < 0) - v = -(solv->ruletojob.elements[-solv->bestrules_pkg[i - solv->bestrules] - solv->jobrules] + 1); - else - v = i; - queue_push(&solv->problems, v); + POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "UNSOLVABLE\n"); + return -1; } - queue_push(&solv->problems, 0); - - if (solv->allowuninstall || solv->allowuninstall_all || solv->allowuninstallmap.size) - if (autouninstall(solv, solv->problems.elements + oldproblemcount + 1) != 0) - { - solv->problems.count = oldproblemcount; - havedisabled = 1; - break; /* start over */ - } - + /* disable all problem rules */ for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++) solver_disableproblem(solv, solv->problems.elements[i]); + havedisabled = 1; break; /* start over */ } @@ -451,23 +327,15 @@ makeruledecisions(Solver *solv) continue; POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "assertion conflict, but I am weak, disabling "); - solver_printrule(solv, SOLV_DEBUG_UNSOLVABLE, r); - - if (ri >= solv->jobrules && ri < solv->jobrules_end) - v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1); - else if (ri >= solv->bestrules && ri < solv->bestrules_up && solv->bestrules_pkg[ri - solv->bestrules] < 0) - v = -(solv->ruletojob.elements[-solv->bestrules_pkg[ri - solv->bestrules] - solv->jobrules] + 1); - else - v = ri; - solver_disableproblem(solv, v); - if (v < 0) - solver_reenablepolicyrules(solv, -v); + solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, r); + solver_fixproblem(solv, ri); havedisabled = 1; break; /* start over */ } if (ii == solv->ruleassertions.count) break; /* finished! */ } + return 1; } @@ -1022,38 +890,9 @@ analyze_unsolvable_rule(Solver *solv, Rule *r, Queue *weakq, Map *rseen) } if (solv->weakrulemap.size && MAPTST(&solv->weakrulemap, why) && weakq) queue_push(weakq, why); - /* do not add pkg rules to problem */ - if (why < solv->pkgrules_end) - return; - /* turn rule into problem */ - if (why >= solv->jobrules && why < solv->jobrules_end) - why = -(solv->ruletojob.elements[why - solv->jobrules] + 1); - else if (why >= solv->bestrules && why < solv->bestrules_up && solv->bestrules_pkg[why - solv->bestrules] < 0) - why = -(solv->ruletojob.elements[-solv->bestrules_pkg[why - solv->bestrules] - solv->jobrules] + 1); - /* normalize dup/infarch rules */ - if (why > solv->infarchrules && why < solv->infarchrules_end) - { - Id name = pool->solvables[-solv->rules[why].p].name; - while (why > solv->infarchrules && pool->solvables[-solv->rules[why - 1].p].name == name) - why--; - } - if (why > solv->duprules && why < solv->duprules_end) - { - Id name = pool->solvables[-solv->rules[why].p].name; - while (why > solv->duprules && pool->solvables[-solv->rules[why - 1].p].name == name) - why--; - } - - /* return if problem already countains our rule */ - if (solv->problems.count) - { - for (i = solv->problems.count - 1; i >= 0; i--) - if (solv->problems.elements[i] == 0) /* end of last problem reached? */ - break; - else if (solv->problems.elements[i] == why) - return; - } - queue_push(&solv->problems, why); + /* add non-pkg rules to problem and disable */ + if (why >= solv->pkgrules_end) + solver_recordproblem(solv, why); } @@ -1160,24 +999,18 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules) return 0; } queue_free(&weakq); - if (lastweak >= solv->jobrules && lastweak < solv->jobrules_end) - v = -(solv->ruletojob.elements[lastweak - solv->jobrules] + 1); - else - v = lastweak; POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "disabling "); solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, solv->rules + lastweak); if (lastweak >= solv->choicerules && lastweak < solv->choicerules_end) solver_disablechoicerules(solv, solv->rules + lastweak); - solver_disableproblem(solv, v); - if (v < 0) - solver_reenablepolicyrules(solv, -v); + solver_fixproblem(solv, lastweak); solver_reset(solv); return 0; } queue_free(&weakq); if (solv->allowuninstall || solv->allowuninstall_all || solv->allowuninstallmap.size) - if (autouninstall(solv, solv->problems.elements + oldproblemcount + 1) != 0) + if (solver_autouninstall(solv, solv->problems.elements + oldproblemcount + 1) != 0) { solv->problems.count = oldproblemcount; solv->learnt_pool.count = oldlearntpoolcount; @@ -2683,13 +2516,9 @@ solver_run_sat(Solver *solv, int disablerules, int doweak) { if (level < 0) break; - makeruledecisions(solv); - level = 1; - if (!disablerules && solv->problems.count) - { - level = -1; - break; - } + level = makeruledecisions(solv, disablerules); + if (level < 0) + break; POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "initial propagate (propagate_index: %d; size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count); if ((r = propagate(solv, level)) != 0) { -- 2.47.2