2 * Copyright (c) 2007-2009, Novell Inc.
4 * This program is licensed under the BSD license, read LICENSE.BSD
5 * for further information
24 #include "solverdebug.h"
27 /**********************************************************************************/
29 /* a problem is an item on the solver's problem list. It can either be >0, in that
30 * case it is a update/infarch/dup rule, or it can be <0, which makes it refer to a job
31 * consisting of multiple job rules.
35 solver_disableproblem(Solver *solv, Id v)
43 if (v >= solv->infarchrules && v < solv->infarchrules_end)
45 Pool *pool = solv->pool;
46 Id name = pool->solvables[-solv->rules[v].p].name;
47 while (v > solv->infarchrules && pool->solvables[-solv->rules[v - 1].p].name == name)
49 for (; v < solv->infarchrules_end && pool->solvables[-solv->rules[v].p].name == name; v++)
50 solver_disablerule(solv, solv->rules + v);
53 if (v >= solv->duprules && v < solv->duprules_end)
55 Pool *pool = solv->pool;
56 Id name = pool->solvables[-solv->rules[v].p].name;
57 while (v > solv->duprules && pool->solvables[-solv->rules[v - 1].p].name == name)
59 for (; v < solv->duprules_end && pool->solvables[-solv->rules[v].p].name == name; v++)
60 solver_disablerule(solv, solv->rules + v);
63 solver_disablerule(solv, solv->rules + v);
65 /* XXX: doesn't work */
66 if (v >= solv->updaterules && v < solv->updaterules_end)
68 /* enable feature rule if we disabled the update rule */
69 r = solv->rules + (v - solv->updaterules + solv->featurerules);
71 solver_enablerule(solv, r);
77 jp = solv->ruletojob.elements;
78 for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++, jp++)
80 solver_disablerule(solv, r);
83 /*-------------------------------------------------------------------
88 solver_enableproblem(Solver *solv, Id v)
96 if (v >= solv->infarchrules && v < solv->infarchrules_end)
98 Pool *pool = solv->pool;
99 Id name = pool->solvables[-solv->rules[v].p].name;
100 while (v > solv->infarchrules && pool->solvables[-solv->rules[v - 1].p].name == name)
102 for (; v < solv->infarchrules_end && pool->solvables[-solv->rules[v].p].name == name; v++)
103 solver_enablerule(solv, solv->rules + v);
106 if (v >= solv->duprules && v < solv->duprules_end)
108 Pool *pool = solv->pool;
109 Id name = pool->solvables[-solv->rules[v].p].name;
110 while (v > solv->duprules && pool->solvables[-solv->rules[v - 1].p].name == name)
112 for (; v < solv->duprules_end && pool->solvables[-solv->rules[v].p].name == name; v++)
113 solver_enablerule(solv, solv->rules + v);
116 if (v >= solv->featurerules && v < solv->featurerules_end)
118 /* do not enable feature rule if update rule is enabled */
119 r = solv->rules + (v - solv->featurerules + solv->updaterules);
123 solver_enablerule(solv, solv->rules + v);
124 if (v >= solv->updaterules && v < solv->updaterules_end)
126 /* disable feature rule when enabling update rule */
127 r = solv->rules + (v - solv->updaterules + solv->featurerules);
129 solver_disablerule(solv, r);
134 jp = solv->ruletojob.elements;
135 for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++, jp++)
137 solver_enablerule(solv, r);
141 /*-------------------------------------------------------------------
144 * Reenable all disabled weak rules (marked in weakrulemap)
149 enableweakrules(Solver *solv)
154 for (i = 1, r = solv->rules + i; i < solv->learntrules; i++, r++)
156 if (r->d >= 0) /* already enabled? */
158 if (!MAPTST(&solv->weakrulemap, i))
160 solver_enablerule(solv, r);
165 /*-------------------------------------------------------------------
169 * at this point, all rules that led to conflicts are disabled.
170 * we re-enable all rules of a problem set but rule "sug", then
171 * continue to disable more rules until there as again a solution.
174 /* FIXME: think about conflicting assertions */
177 refine_suggestion(Solver *solv, Id *problem, Id sug, Queue *refined, int essentialok)
179 Pool *pool = solv->pool;
185 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
187 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
188 for (i = 0; problem[i]; i++)
190 if (problem[i] == sug)
191 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
192 solver_printproblem(solv, problem[i]);
195 queue_empty(refined);
196 if (!essentialok && sug < 0 && (solv->job.elements[-sug - 1] & SOLVER_ESSENTIAL) != 0)
198 queue_init(&disabled);
199 queue_push(refined, sug);
201 /* re-enable all problem rules with the exception of "sug"(gestion) */
204 for (i = 0; problem[i]; i++)
205 if (problem[i] != sug)
206 solver_enableproblem(solv, problem[i]);
209 solver_reenablepolicyrules(solv, -(sug + 1));
210 else if (sug >= solv->updaterules && sug < solv->updaterules_end)
212 /* enable feature rule */
213 Rule *r = solv->rules + solv->featurerules + (sug - solv->updaterules);
215 solver_enablerule(solv, r);
218 enableweakrules(solv);
222 int njob, nfeature, nupdate;
223 queue_empty(&solv->problems);
226 if (!solv->problems.count)
227 solver_run_sat(solv, 0, 0);
229 if (!solv->problems.count)
231 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
232 IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
233 solver_printdecisions(solv);
234 break; /* great, no more problems */
236 disabledcnt = disabled.count;
237 /* start with 1 to skip over proof index */
238 njob = nfeature = nupdate = 0;
239 for (i = 1; i < solv->problems.count - 1; i++)
241 /* ignore solutions in refined */
242 v = solv->problems.elements[i];
244 break; /* end of problem reached */
245 for (j = 0; problem[j]; j++)
246 if (problem[j] != sug && problem[j] == v)
250 if (v >= solv->featurerules && v < solv->featurerules_end)
256 if (!essentialok && (solv->job.elements[-v -1] & SOLVER_ESSENTIAL) != 0)
257 continue; /* not that one! */
260 queue_push(&disabled, v);
262 if (disabled.count == disabledcnt)
264 /* no solution found, this was an invalid suggestion! */
265 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
269 if (!njob && nupdate && nfeature)
271 /* got only update rules, filter out feature rules */
272 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "throwing away feature rules\n");
273 for (i = j = disabledcnt; i < disabled.count; i++)
275 v = disabled.elements[i];
276 if (v < solv->featurerules || v >= solv->featurerules_end)
277 disabled.elements[j++] = v;
282 if (disabled.count == disabledcnt + 1)
284 /* just one suggestion, add it to refined list */
285 v = disabled.elements[disabledcnt];
287 queue_push(refined, v); /* do not record feature rules */
288 solver_disableproblem(solv, v);
289 if (v >= solv->updaterules && v < solv->updaterules_end)
291 Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
293 solver_enablerule(solv, r); /* enable corresponding feature rule */
296 solver_reenablepolicyrules(solv, -(v + 1));
300 /* more than one solution, disable all */
301 /* do not push anything on refine list, as we do not know which solution to choose */
302 /* thus, the user will get another problem if he selects this solution, where he
303 * can choose the right one */
304 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
306 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
307 for (i = disabledcnt; i < disabled.count; i++)
308 solver_printproblem(solv, disabled.elements[i]);
310 for (i = disabledcnt; i < disabled.count; i++)
312 v = disabled.elements[i];
313 solver_disableproblem(solv, v);
314 if (v >= solv->updaterules && v < solv->updaterules_end)
316 Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
318 solver_enablerule(solv, r);
323 /* all done, get us back into the same state as before */
324 /* enable refined rules again */
325 for (i = 0; i < disabled.count; i++)
326 solver_enableproblem(solv, disabled.elements[i]);
327 queue_free(&disabled);
328 /* reset policy rules */
329 for (i = 0; problem[i]; i++)
330 solver_enableproblem(solv, problem[i]);
331 solver_disablepolicyrules(solv);
332 /* disable problem rules again */
333 for (i = 0; problem[i]; i++)
334 solver_disableproblem(solv, problem[i]);
335 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
339 /*-------------------------------------------------------------------
340 * sorting helper for problems
342 * bring update rules before job rules
343 * make essential job rules last
347 problems_sortcmp(const void *ap, const void *bp, void *dp)
350 Id a = *(Id *)ap, b = *(Id *)bp;
357 int af = job->elements[-a - 1] & SOLVER_ESSENTIAL;
358 int bf = job->elements[-b - 1] & SOLVER_ESSENTIAL;
367 * convert a solution rule into a job modifier
370 convertsolution(Solver *solv, Id why, Queue *solutionq)
372 Pool *pool = solv->pool;
375 queue_push(solutionq, 0);
376 queue_push(solutionq, -why);
379 if (why >= solv->infarchrules && why < solv->infarchrules_end)
382 /* infarch rule, find replacement */
383 assert(solv->rules[why].p < 0);
384 name = pool->solvables[-solv->rules[why].p].name;
385 while (why > solv->infarchrules && pool->solvables[-solv->rules[why - 1].p].name == name)
388 for (; why < solv->infarchrules_end && pool->solvables[-solv->rules[why].p].name == name; why++)
389 if (solv->decisionmap[-solv->rules[why].p] > 0)
391 p = -solv->rules[why].p;
395 return; /* false alarm */
396 queue_push(solutionq, SOLVER_SOLUTION_INFARCH);
397 queue_push(solutionq, p);
400 if (why >= solv->duprules && why < solv->duprules_end)
403 /* dist upgrade rule, find replacement */
404 assert(solv->rules[why].p < 0);
405 name = pool->solvables[-solv->rules[why].p].name;
406 while (why > solv->duprules && pool->solvables[-solv->rules[why - 1].p].name == name)
409 for (; why < solv->duprules_end && pool->solvables[-solv->rules[why].p].name == name; why++)
410 if (solv->decisionmap[-solv->rules[why].p] > 0)
412 p = -solv->rules[why].p;
416 return; /* false alarm */
417 queue_push(solutionq, SOLVER_SOLUTION_DISTUPGRADE);
418 queue_push(solutionq, p);
421 if (why >= solv->updaterules && why < solv->updaterules_end)
423 /* update rule, find replacement package */
427 assert(why >= solv->updaterules && why < solv->updaterules_end);
428 /* check if this is a false positive, i.e. the update rule is fulfilled */
429 rr = solv->rules + why;
430 FOR_RULELITERALS(p, dp, rr)
431 if (p > 0 && solv->decisionmap[p] > 0)
434 return; /* false alarm */
436 p = solv->installed->start + (why - solv->updaterules);
437 rr = solv->rules + solv->featurerules + (why - solv->updaterules);
439 rr = solv->rules + why;
440 if (solv->distupgrade && solv->rules[why].p != p && solv->decisionmap[p] > 0)
442 /* distupgrade case, allow to keep old package */
443 queue_push(solutionq, p);
444 queue_push(solutionq, p);
447 if (solv->decisionmap[p] > 0)
448 return; /* false alarm, turned out we can keep the package */
451 int mvrp = 0; /* multi-version replacement */
452 FOR_RULELITERALS(rp, dp, rr)
454 if (rp > 0 && solv->decisionmap[rp] > 0 && pool->solvables[rp].repo != solv->installed)
457 if (!(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, rp)))
463 /* found only multi-version replacements */
464 /* have to split solution into two parts */
465 queue_push(solutionq, p);
466 queue_push(solutionq, mvrp);
469 queue_push(solutionq, p);
470 queue_push(solutionq, rp);
476 * convert problem data into a form usable for refining.
477 * Returns the number of problems.
480 solver_prepare_solutions(Solver *solv)
482 int i, j = 1, idx = 1;
484 if (!solv->problems.count)
486 queue_push(&solv->solutions, 0);
487 queue_push(&solv->solutions, -1); /* unrefined */
488 for (i = 1; i < solv->problems.count; i++)
490 Id p = solv->problems.elements[i];
491 queue_push(&solv->solutions, p);
494 solv->problems.elements[j++] = idx;
495 if (i + 1 >= solv->problems.count)
497 solv->problems.elements[j++] = solv->problems.elements[++i]; /* copy proofidx */
498 idx = solv->solutions.count;
499 queue_push(&solv->solutions, -1);
501 solv->problems.count = j;
506 * refine the simple solution rule list provided by
507 * the solver into multiple lists of job modifiers.
510 create_solutions(Solver *solv, int probnr, int solidx)
512 Pool *pool = solv->pool;
514 Queue problem, solution, problems_save;
521 recocount = solv->recommendations.count;
522 solv->recommendations.count = 0; /* so that revert() doesn't mess with it later */
524 /* save decisionq, decisionq_why, decisionmap */
525 for (i = 0; i < solv->decisionq.count; i++)
527 Id p = solv->decisionq.elements[i];
528 queue_push(&redoq, p);
529 queue_push(&redoq, solv->decisionq_why.elements[i]);
530 queue_push(&redoq, solv->decisionmap[p > 0 ? p : -p]);
532 /* save problems queue */
533 problems_save = solv->problems;
534 memset(&solv->problems, 0, sizeof(solv->problems));
536 /* extract problem from queue */
537 queue_init(&problem);
538 for (i = solidx + 1; i < solv->solutions.count; i++)
540 Id v = solv->solutions.elements[i];
543 queue_push(&problem, v);
545 if (problem.count > 1)
546 sat_sort(problem.elements, problem.count, sizeof(Id), problems_sortcmp, &solv->job);
547 queue_push(&problem, 0); /* mark end for refine_suggestion */
550 for (i = 0; i < problem.count; i++)
551 printf("PP %d %d\n", i, problem.elements[i]);
554 /* refine each solution element */
557 queue_init(&solution);
558 for (i = 0; i < problem.count; i++)
560 int solstart = solv->solutions.count;
561 refine_suggestion(solv, problem.elements, problem.elements[i], &solution, essentialok);
562 queue_push(&solv->solutions, 0); /* reserve room for number of elements */
563 for (j = 0; j < solution.count; j++)
564 convertsolution(solv, solution.elements[j], &solv->solutions);
565 if (solv->solutions.count == solstart + 1)
567 solv->solutions.count--;
568 if (!essentialok && i + 1 == problem.count && !nsol)
570 /* nothing found, start over */
576 /* patch in number of solution elements */
577 solv->solutions.elements[solstart] = (solv->solutions.count - (solstart + 1)) / 2;
578 queue_push(&solv->solutions, 0); /* add end marker */
579 queue_push(&solv->solutions, 0); /* add end marker */
580 solv->solutions.elements[solidx + 1 + nsol++] = solstart;
582 solv->solutions.elements[solidx + 1 + nsol] = 0; /* end marker */
583 solv->solutions.elements[solidx] = nsol;
584 queue_free(&problem);
585 queue_free(&solution);
587 /* restore decisions */
588 memset(solv->decisionmap, 0, pool->nsolvables * sizeof(Id));
589 queue_empty(&solv->decisionq);
590 queue_empty(&solv->decisionq_why);
591 for (i = 0; i < redoq.count; i += 3)
593 Id p = redoq.elements[i];
594 queue_push(&solv->decisionq, p);
595 queue_push(&solv->decisionq_why, redoq.elements[i + 1]);
596 solv->decisionmap[p > 0 ? p : -p] = redoq.elements[i + 2];
598 solv->recommendations.count = recocount;
600 /* restore problems */
601 queue_free(&solv->problems);
602 solv->problems = problems_save;
603 POOL_DEBUG(SAT_DEBUG_STATS, "create_solutions for problem #%d took %d ms\n", probnr, sat_timems(now));
607 /**************************************************************************/
610 solver_problem_count(Solver *solv)
612 return solv->problems.count / 2;
616 solver_next_problem(Solver *solv, Id problem)
619 return solv->problems.count ? 1 : 0;
620 return (problem + 1) * 2 - 1 < solv->problems.count ? problem + 1 : 0;
624 solver_solution_count(Solver *solv, Id problem)
626 Id solidx = solv->problems.elements[problem * 2 - 1];
627 if (solv->solutions.elements[solidx] < 0)
628 create_solutions(solv, problem, solidx);
629 return solv->solutions.elements[solidx];
633 solver_next_solution(Solver *solv, Id problem, Id solution)
635 Id solidx = solv->problems.elements[problem * 2 - 1];
636 if (solv->solutions.elements[solidx] < 0)
637 create_solutions(solv, problem, solidx);
638 return solv->solutions.elements[solidx + solution + 1] ? solution + 1 : 0;
642 solver_solutionelement_count(Solver *solv, Id problem, Id solution)
644 Id solidx = solv->problems.elements[problem * 2 - 1];
645 solidx = solv->solutions.elements[solidx + solution];
646 return solv->solutions.elements[solidx];
651 * return the next item of the proposed solution
652 * here are the possibilities for p / rp and what
653 * the solver expects the application to do:
655 * -------------------------------------------------------
656 * SOLVER_SOLUTION_INFARCH pkgid
657 * -> add (SOLVER_INSTALL|SOLVER_SOLVABLE, rp) to the job
658 * SOLVER_SOLUTION_DISTUPGRADE pkgid
659 * -> add (SOLVER_INSTALL|SOLVER_SOLVABLE, rp) to the job
660 * SOLVER_SOLUTION_JOB jobidx
661 * -> remove job (jobidx - 1, jobidx) from job queue
663 * -> add (SOLVER_ERASE|SOLVER_SOLVABLE, p) to the job
664 * pkgid (> 0) pkgid (> 0)
665 * -> add (SOLVER_INSTALL|SOLVER_SOLVABLE, rp) to the job
666 * (this will replace package p)
668 * Thus, the solver will either ask the application to remove
669 * a specific job from the job queue, or ask to add an install/erase
675 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
677 Id solidx = solv->problems.elements[problem * 2 - 1];
678 solidx = solv->solutions.elements[solidx + solution];
681 solidx += 1 + element * 2;
682 if (!solv->solutions.elements[solidx] && !solv->solutions.elements[solidx + 1])
684 *p = solv->solutions.elements[solidx];
685 *rp = solv->solutions.elements[solidx + 1];
689 /*-------------------------------------------------------------------
695 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
698 Id lreqr, lconr, lsysr, ljobr;
702 lreqr = lconr = lsysr = ljobr = 0;
703 while ((rid = solv->learnt_pool.elements[idx++]) != 0)
706 if (rid >= solv->learntrules)
707 findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
708 else if ((rid >= solv->jobrules && rid < solv->jobrules_end) || (rid >= solv->infarchrules && rid < solv->infarchrules_end) || (rid >= solv->duprules && rid < solv->duprules_end))
713 else if (rid >= solv->updaterules && rid < solv->updaterules_end)
720 assert(rid < solv->rpmrules_end);
721 r = solv->rules + rid;
722 d = r->d < 0 ? -r->d - 1 : r->d;
730 if (!d && r->w2 == 0 && !reqassert)
732 if (*reqrp > 0 && r->p < -1)
734 Id op = -solv->rules[*reqrp].p;
735 if (op > 1 && solv->pool->solvables[op].arch != solv->pool->solvables[-r->p].arch)
736 continue; /* different arch, skip */
738 /* prefer assertions */
744 else if (solv->installed && r->p < 0 && solv->pool->solvables[-r->p].repo == solv->installed && !reqassert)
746 /* prefer rules of installed packages */
752 if (!*reqrp && lreqr)
754 if (!*conrp && lconr)
756 if (!*jobrp && ljobr)
758 if (!*sysrp && lsysr)
765 * search for a rule that describes the problem to the
766 * user. Actually a pretty hopeless task that may leave the user
767 * puzzled. To get all of the needed information use
768 * solver_findallproblemrules() instead.
772 solver_findproblemrule(Solver *solv, Id problem)
774 Id reqr, conr, sysr, jobr;
775 Id idx = solv->problems.elements[2 * problem - 2];
776 reqr = conr = sysr = jobr = 0;
777 findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
779 return reqr; /* some requires */
781 return conr; /* some conflict */
783 return sysr; /* an update rule */
785 return jobr; /* a user request */
789 /*-------------------------------------------------------------------*/
792 findallproblemrules_internal(Solver *solv, Id idx, Queue *rules)
795 while ((rid = solv->learnt_pool.elements[idx++]) != 0)
797 if (rid >= solv->learntrules)
799 findallproblemrules_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], rules);
802 queue_pushunique(rules, rid);
807 * find all problem rule
809 * return all rules that lead to the problem. This gives the user
810 * all of the information to understand the problem, but the result
811 * can be a large number of rules.
815 solver_findallproblemrules(Solver *solv, Id problem, Queue *rules)
818 findallproblemrules_internal(solv, solv->problems.elements[2 * problem - 2], rules);
821 /* obsolete function */
823 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
825 return solver_ruleinfo(solv, rid, sourcep, targetp, depp);