2 * Copyright (c) 2007, Novell Inc.
4 * This program is licensed under the BSD license, read LICENSE.BSD
5 * for further information
11 * SAT based dependency solver
29 #define RULES_BLOCK 63
33 solver_splitprovides(Solver *solv, Id dep)
35 Pool *pool = solv->pool;
40 if (!solv->dosplitprovides || !solv->installed)
44 rd = GETRELDEP(pool, dep);
45 if (rd->flags != REL_WITH)
47 FOR_PROVIDES(p, pp, dep)
49 s = pool->solvables + p;
50 if (s->repo == solv->installed && s->name == rd->name)
57 solver_dep_installed(Solver *solv, Id dep)
60 Pool *pool = solv->pool;
65 Reldep *rd = GETRELDEP(pool, dep);
66 if (rd->flags == REL_AND)
68 if (!solver_dep_installed(solv, rd->name))
70 return solver_dep_installed(solv, rd->evr);
72 if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
73 return solver_dep_installed(solv, rd->evr);
75 FOR_PROVIDES(p, pp, dep)
77 if (p == SYSTEMSOLVABLE || (solv->installed && pool->solvables[p].repo == solv->installed))
85 /* this mirrors solver_dep_fulfilled but uses map m instead of the decisionmap */
87 dep_possible(Solver *solv, Id dep, Map *m)
89 Pool *pool = solv->pool;
94 Reldep *rd = GETRELDEP(pool, dep);
95 if (rd->flags == REL_AND)
97 if (!dep_possible(solv, rd->name, m))
99 return dep_possible(solv, rd->evr, m);
101 if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_SPLITPROVIDES)
102 return solver_splitprovides(solv, rd->evr);
103 if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
104 return solver_dep_installed(solv, rd->evr);
106 FOR_PROVIDES(p, pp, dep)
114 /*-----------------------------------------------------------------*/
121 printruleelement(Solver *solv, int type, Rule *r, Id v)
123 Pool *pool = solv->pool;
127 s = pool->solvables + -v;
128 POOL_DEBUG(type, " !%s [%d]", solvable2str(pool, s), -v);
132 s = pool->solvables + v;
133 POOL_DEBUG(type, " %s [%d]", solvable2str(pool, s), v);
138 POOL_DEBUG(type, " (w1)");
140 POOL_DEBUG(type, " (w2)");
142 if (solv->decisionmap[s - pool->solvables] > 0)
143 POOL_DEBUG(type, " Install.level%d", solv->decisionmap[s - pool->solvables]);
144 if (solv->decisionmap[s - pool->solvables] < 0)
145 POOL_DEBUG(type, " Conflict.level%d", -solv->decisionmap[s - pool->solvables]);
146 POOL_DEBUG(type, "\n");
155 printrule(Solver *solv, int type, Rule *r)
157 Pool *pool = solv->pool;
161 if (r >= solv->rules && r < solv->rules + solv->nrules) /* r is a solver rule */
162 POOL_DEBUG(type, "Rule #%d:", (int)(r - solv->rules));
164 POOL_DEBUG(type, "Rule:"); /* r is any rule */
166 POOL_DEBUG(type, " (disabled)");
167 POOL_DEBUG(type, "\n");
171 /* print direct literal */
173 else if (r->d == ID_NULL)
177 /* binary rule --> print w2 as second literal */
181 /* every other which is in d */
182 v = solv->pool->whatprovidesdata[r->d + i - 1];
185 printruleelement(solv, type, r, v);
187 POOL_DEBUG(type, " next rules: %d %d\n", r->n1, r->n2);
191 printruleclass(Solver *solv, int type, Rule *r)
193 Pool *pool = solv->pool;
194 Id p = r - solv->rules;
196 if (p < solv->learntrules)
197 if (MAPTST(&solv->weakrulemap, p))
198 POOL_DEBUG(type, "WEAK ");
199 if (p >= solv->learntrules)
200 POOL_DEBUG(type, "LEARNT ");
201 else if (p >= solv->featurerules)
202 POOL_DEBUG(type, "FEATURE ");
203 else if (p >= solv->updaterules)
204 POOL_DEBUG(type, "UPDATE ");
205 else if (p >= solv->jobrules)
206 POOL_DEBUG(type, "JOB ");
207 printrule(solv, type, r);
211 /*-----------------------------------------------------------------*/
217 static Pool *unifyrules_sortcmp_data;
220 * compare rules for unification sort
224 unifyrules_sortcmp(const void *ap, const void *bp)
226 Pool *pool = unifyrules_sortcmp_data;
227 Rule *a = (Rule *)ap;
228 Rule *b = (Rule *)bp;
234 return x; /* p differs */
237 if (a->d == 0 && b->d == 0)
238 return a->w2 - b->w2; /* assertion: return w2 diff */
240 if (a->d == 0) /* a is assertion, b not */
242 x = a->w2 - pool->whatprovidesdata[b->d];
246 if (b->d == 0) /* b is assertion, a not */
248 x = pool->whatprovidesdata[a->d] - b->w2;
252 /* compare whatprovidesdata */
253 ad = pool->whatprovidesdata + a->d;
254 bd = pool->whatprovidesdata + b->d;
256 if ((x = *ad++ - *bd++) != 0)
267 unifyrules(Solver *solv)
269 Pool *pool = solv->pool;
273 if (solv->nrules <= 1) /* nothing to unify */
276 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- unifyrules -----\n");
278 /* sort rules first */
279 unifyrules_sortcmp_data = solv->pool;
280 qsort(solv->rules + 1, solv->nrules - 1, sizeof(Rule), unifyrules_sortcmp);
287 for (i = j = 1, ir = solv->rules + i; i < solv->nrules; i++, ir++)
289 if (jr && !unifyrules_sortcmp(ir, jr))
290 continue; /* prune! */
291 jr = solv->rules + j++; /* keep! */
296 /* reduced count from nrules to j rules */
297 POOL_DEBUG(SAT_DEBUG_STATS, "pruned rules from %d to %d\n", solv->nrules, j);
299 /* adapt rule buffer */
301 solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
302 IF_POOLDEBUG (SAT_DEBUG_STATS)
309 for (i = 1; i < solv->nrules; i++)
316 dp = solv->pool->whatprovidesdata + r->d;
321 POOL_DEBUG(SAT_DEBUG_STATS, " binary: %d\n", binr);
322 POOL_DEBUG(SAT_DEBUG_STATS, " normal: %d, %d literals\n", solv->nrules - 1 - binr, lits);
324 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- unifyrules end -----\n");
334 hashrule(Solver *solv, Id p, Id d, int n)
336 unsigned int x = (unsigned int)p;
340 return (x * 37) ^ (unsigned int)d;
341 dp = solv->pool->whatprovidesdata + d;
343 x = (x * 37) ^ (unsigned int)*dp++;
351 * p = direct literal; always < 0 for installed rpm rules
352 * d, if < 0 direct literal, if > 0 offset into whatprovides, if == 0 rule is assertion (look at p only)
355 * A requires b, b provided by B1,B2,B3 => (-A|B1|B2|B3)
357 * p < 0 : pkg id of A
358 * d > 0 : Offset in whatprovidesdata (list of providers of b)
360 * A conflicts b, b provided by B1,B2,B3 => (-A|-B1), (-A|-B2), (-A|-B3)
361 * p < 0 : pkg id of A
362 * d < 0 : Id of solvable (e.g. B1)
364 * d == 0: unary rule, assertion => (A) or (-A)
366 * Install: p > 0, d = 0 (A) user requested install
367 * Remove: p < 0, d = 0 (-A) user requested remove
368 * Requires: p < 0, d > 0 (-A|B1|B2|...) d: <list of providers for requirement of p>
369 * Updates: p > 0, d > 0 (A|B1|B2|...) d: <list of updates for solvable p>
370 * Conflicts: p < 0, d < 0 (-A|-B) either p (conflict issuer) or d (conflict provider) (binary rule)
371 * ? p > 0, d < 0 (A|-B)
372 * No-op ?: p = 0, d = 0 (null) (used as policy rule placeholder)
376 * Direct assertion (no watch needed)( if d <0 ) --> d = 0, w1 = p, w2 = 0
377 * Binary rule: p = first literal, d = 0, w2 = second literal, w1 = p
378 * every other : w1 = p, w2 = whatprovidesdata[d];
379 * Disabled rule: w1 = 0
381 * always returns a rule for non-rpm rules
385 addrule(Solver *solv, Id p, Id d)
387 Pool *pool = solv->pool;
391 int n = 0; /* number of literals in rule - 1
392 0 = direct assertion (single literal)
396 /* it often happenes that requires lead to adding the same rpm rule
397 * multiple times, so we prune those duplicates right away to make
398 * the work for unifyrules a bit easier */
400 if (solv->nrules && !solv->jobrules)
402 r = solv->rules + solv->nrules - 1; /* get the last added rule */
403 if (r->p == p && r->d == d && d != 0) /* identical and not user requested */
409 /* always a binary rule */
411 return 0; /* ignore self conflict */
416 for (dp = pool->whatprovidesdata + d; *dp; dp++, n++)
418 return 0; /* rule is self-fulfilling */
420 d = dp[-1]; /* take single literal */
424 if (n == 0 && !solv->jobrules)
426 /* this is a rpm rule assertion, we do not have to allocate it */
427 /* it can be identified by a level of 1 and a zero reason */
428 /* we must not drop those rules from the decisionq when rewinding! */
430 assert(solv->decisionmap[-p] == 0 || solv->decisionmap[-p] == -1);
431 if (solv->decisionmap[-p])
432 return 0; /* already got that one */
433 queue_push(&solv->decisionq, p);
434 queue_push(&solv->decisionq_why, 0);
435 solv->decisionmap[-p] = -1;
442 /* smallest literal first so we can find dups */
446 n = 1; /* re-set n, was used as temp var */
449 /* check if the last added rule is exactly the same as what we're looking for. */
450 if (r && n == 1 && !r->d && r->p == p && r->w2 == d)
451 return r; /* binary rule */
453 if (r && n > 1 && r->d && r->p == p)
455 /* Rule where d is an offset in whatprovidesdata */
459 dp2 = pool->whatprovidesdata + r->d;
460 for (dp = pool->whatprovidesdata + d; *dp; dp++, dp2++)
471 /* extend rule buffer */
472 solv->rules = sat_extend(solv->rules, solv->nrules, 1, sizeof(Rule), RULES_BLOCK);
473 r = solv->rules + solv->nrules++; /* point to rule space */
478 /* direct assertion, no watch needed */
494 r->w2 = pool->whatprovidesdata[d];
499 IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
501 POOL_DEBUG(SAT_DEBUG_RULE_CREATION, " Add rule: ");
502 printrule(solv, SAT_DEBUG_RULE_CREATION, r);
509 disablerule(Solver *solv, Rule *r)
515 enablerule(Solver *solv, Rule *r)
517 if (r->d == 0 || r->w2 != r->p)
520 r->w1 = solv->pool->whatprovidesdata[r->d];
524 /**********************************************************************************/
526 /* a problem is an item on the solver's problem list. It can either be >0, in that
527 * case it is a update rule, or it can be <0, which makes it refer to a job
528 * consisting of multiple job rules.
532 disableproblem(Solver *solv, Id v)
540 disablerule(solv, solv->rules + v);
544 jp = solv->ruletojob.elements;
545 for (i = solv->jobrules, r = solv->rules + i; i < solv->updaterules; i++, r++, jp++)
547 disablerule(solv, r);
551 enableproblem(Solver *solv, Id v)
559 if (v >= solv->featurerules && v < solv->learntrules)
561 /* do not enable feature rule is update rule is enabled */
562 r = solv->rules + v - (solv->installed->end - solv->installed->start);
566 enablerule(solv, solv->rules + v);
567 if (v >= solv->updaterules && v < solv->featurerules)
569 r = solv->rules + v + (solv->installed->end - solv->installed->start);
571 disablerule(solv, r);
576 jp = solv->ruletojob.elements;
577 for (i = solv->jobrules, r = solv->rules + i; i < solv->updaterules; i++, r++, jp++)
583 printproblem(Solver *solv, Id v)
585 Pool *pool = solv->pool;
591 printruleclass(solv, SAT_DEBUG_SOLUTIONS, solv->rules + v);
595 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "JOB %d\n", v);
596 jp = solv->ruletojob.elements;
597 for (i = solv->jobrules, r = solv->rules + i; i < solv->updaterules; i++, r++, jp++)
600 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "- ");
601 printrule(solv, SAT_DEBUG_SOLUTIONS, r);
603 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "ENDJOB\n");
609 /************************************************************************/
611 /* go through update and job rules and add direct assertions
612 * to the decisionqueue. If we find a conflict, disable rules and
613 * add them to problem queue.
616 makeruledecisions(Solver *solv)
618 Pool *pool = solv->pool;
624 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions ; size decisionq: %d -----\n",solv->decisionq.count);
626 decisionstart = solv->decisionq.count;
627 /* rpm rules don't have assertions, so we can start with the job
628 * rules (rpm assertions are not resulting in a rule, but cause a
629 * immediate decision) */
630 /* nowadays they can be weak, so start with rule 1 */
631 for (ri = 1, r = solv->rules + ri; ri < solv->nrules; ri++, r++)
633 if (!r->w1 || r->w2) /* disabled or no assertion */
635 /* do weak rules in phase 2 */
636 if (ri < solv->learntrules && MAPTST(&solv->weakrulemap, ri))
640 if (!solv->decisionmap[vv])
642 queue_push(&solv->decisionq, v);
643 queue_push(&solv->decisionq_why, r - solv->rules);
644 solv->decisionmap[vv] = v > 0 ? 1 : -1;
645 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
647 Solvable *s = solv->pool->solvables + vv;
649 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "conflicting %s (assertion)\n", solvable2str(solv->pool, s));
651 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "installing %s (assertion)\n", solvable2str(solv->pool, s));
655 if (v > 0 && solv->decisionmap[vv] > 0)
657 if (v < 0 && solv->decisionmap[vv] < 0)
659 /* found a conflict! */
660 if (ri >= solv->learntrules)
662 /* conflict with a learnt rule */
663 /* can happen when packages cannot be installed for
664 * multiple reasons. */
665 /* we disable the learnt rule in this case */
666 disablerule(solv, r);
669 /* only job and update rules left in the decisionq */
670 /* find the decision which is the "opposite" of the jobrule */
671 for (i = 0; i < solv->decisionq.count; i++)
672 if (solv->decisionq.elements[i] == -v)
674 assert(i < solv->decisionq.count);
675 if (v == -SYSTEMSOLVABLE) {
676 /* conflict with system solvable */
677 queue_push(&solv->problems, solv->learnt_pool.count);
678 queue_push(&solv->learnt_pool, ri);
679 queue_push(&solv->learnt_pool, 0);
680 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with system solvable, disabling rule #%d\n", ri);
681 if (ri < solv->updaterules)
682 v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
685 queue_push(&solv->problems, v);
686 queue_push(&solv->problems, 0);
687 disableproblem(solv, v);
690 assert(solv->decisionq_why.elements[i]);
691 if (solv->decisionq_why.elements[i] < solv->jobrules)
693 /* conflict with rpm rule assertion */
694 queue_push(&solv->problems, solv->learnt_pool.count);
695 queue_push(&solv->learnt_pool, ri);
696 queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]);
697 queue_push(&solv->learnt_pool, 0);
698 assert(v > 0 || v == -SYSTEMSOLVABLE);
699 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with rpm rule, disabling rule #%d\n", ri);
700 if (ri < solv->updaterules)
701 v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
704 queue_push(&solv->problems, v);
705 queue_push(&solv->problems, 0);
706 disableproblem(solv, v);
710 /* conflict with another job or update rule */
712 queue_push(&solv->problems, solv->learnt_pool.count);
713 queue_push(&solv->learnt_pool, ri);
714 queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]);
715 queue_push(&solv->learnt_pool, 0);
717 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflicting update/job assertions over literal %d\n", vv);
719 /* push all of our rules asserting this literal on the problem stack */
720 for (i = solv->jobrules, rr = solv->rules + i; i < solv->nrules; i++, rr++)
722 if (!rr->w1 || rr->w2)
724 if (rr->p != vv && rr->p != -vv)
726 if (i >= solv->learntrules)
728 if (MAPTST(&solv->weakrulemap, i))
730 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, " - disabling rule #%d\n", i);
732 if (i < solv->updaterules)
733 v = -(solv->ruletojob.elements[i - solv->jobrules] + 1);
734 queue_push(&solv->problems, v);
735 disableproblem(solv, v);
737 queue_push(&solv->problems, 0);
740 while (solv->decisionq.count > decisionstart)
742 v = solv->decisionq.elements[--solv->decisionq.count];
743 --solv->decisionq_why.count;
745 solv->decisionmap[vv] = 0;
747 ri = solv->jobrules - 1;
748 r = solv->rules + ri;
751 /* phase 2: now do the weak assertions */
752 for (ri = 1, r = solv->rules + ri; ri < solv->learntrules; ri++, r++)
754 if (!r->w1 || r->w2) /* disabled or no assertion */
756 if (!MAPTST(&solv->weakrulemap, ri))
760 if (!solv->decisionmap[vv])
762 queue_push(&solv->decisionq, v);
763 queue_push(&solv->decisionq_why, r - solv->rules);
764 solv->decisionmap[vv] = v > 0 ? 1 : -1;
765 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
767 Solvable *s = solv->pool->solvables + vv;
769 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "conflicting %s (weak assertion)\n", solvable2str(solv->pool, s));
771 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "installing %s (weak assertion)\n", solvable2str(solv->pool, s));
775 if (v > 0 && solv->decisionmap[vv] > 0)
777 if (v < 0 && solv->decisionmap[vv] < 0)
779 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "assertion conflict, but I am weak, disabling ");
780 printrule(solv, SAT_DEBUG_UNSOLVABLE, r);
781 disablerule(solv, r);
784 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions end; size decisionq: %d -----\n",solv->decisionq.count);
788 * we have enabled or disabled some of our rules. We now reenable all
789 * of our learnt rules but the ones that were learnt from rules that
793 enabledisablelearntrules(Solver *solv)
795 Pool *pool = solv->pool;
800 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "enabledisablelearntrules called\n");
801 for (i = solv->learntrules, r = solv->rules + i; i < solv->nrules; i++, r++)
803 whyp = solv->learnt_pool.elements + solv->learnt_why.elements[i - solv->learntrules];
804 while ((why = *whyp++) != 0)
806 assert(why > 0 && why < i);
807 if (!solv->rules[why].w1)
810 /* why != 0: we found a disabled rule, disable the learnt rule */
813 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
815 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "disabling ");
816 printruleclass(solv, SAT_DEBUG_SOLUTIONS, r);
818 disablerule(solv, r);
820 else if (!why && !r->w1)
822 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
824 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "re-enabling ");
825 printruleclass(solv, SAT_DEBUG_SOLUTIONS, r);
833 enableweakrules(Solver *solv)
838 for (i = solv->jobrules, r = solv->rules + i; i < solv->learntrules; i++, r++)
842 if (!MAPTST(&solv->weakrulemap, i))
849 /* FIXME: bad code ahead, replace as soon as possible */
850 /* FIXME: should probably look at SOLVER_INSTALL_SOLVABLE_ONE_OF */
853 disableupdaterules(Solver *solv, Queue *job, int jobidx)
855 Pool *pool = solv->pool;
857 Id name, how, what, p, *pp;
863 installed = solv->installed;
869 how = job->elements[jobidx] & ~SOLVER_WEAK;
872 case SOLVER_INSTALL_SOLVABLE:
873 case SOLVER_ERASE_SOLVABLE:
874 case SOLVER_ERASE_SOLVABLE_NAME:
875 case SOLVER_ERASE_SOLVABLE_PROVIDES:
881 /* go through all enabled job rules */
882 MAPZERO(&solv->noupdate);
883 for (i = solv->jobrules; i < solv->updaterules; i++)
886 if (!r->w1) /* disabled? */
888 j = solv->ruletojob.elements[i - solv->jobrules];
892 how = job->elements[j] & ~SOLVER_WEAK;
893 what = job->elements[j + 1];
896 case SOLVER_INSTALL_SOLVABLE: /* install specific solvable */
897 s = pool->solvables + what;
898 FOR_PROVIDES(p, pp, s->name)
900 if (pool->solvables[p].name != s->name)
902 if (pool->solvables[p].repo == installed)
903 MAPSET(&solv->noupdate, p - installed->start);
906 case SOLVER_ERASE_SOLVABLE:
907 s = pool->solvables + what;
908 if (s->repo == installed)
909 MAPSET(&solv->noupdate, what - installed->start);
911 case SOLVER_ERASE_SOLVABLE_NAME: /* remove by capability */
912 case SOLVER_ERASE_SOLVABLE_PROVIDES:
913 name = (how == SOLVER_ERASE_SOLVABLE_NAME) ? what : 0;
914 while (ISRELDEP(name))
916 Reldep *rd = GETRELDEP(pool, name);
919 FOR_PROVIDES(p, pp, what)
921 if (name && pool->solvables[p].name != name)
923 if (pool->solvables[p].repo == installed)
924 MAPSET(&solv->noupdate, p - installed->start);
932 /* fixup update rule status */
933 if (solv->allowuninstall)
934 return; /* no update rules at all */
938 /* we just disabled job #jobidx. enable all update rules
939 * that aren't disabled by the remaining job rules */
940 how = job->elements[jobidx] & ~SOLVER_WEAK;
941 what = job->elements[jobidx + 1];
944 case SOLVER_INSTALL_SOLVABLE:
945 s = pool->solvables + what;
946 FOR_PROVIDES(p, pp, s->name)
948 if (pool->solvables[p].name != s->name)
950 if (pool->solvables[p].repo != installed)
952 if (MAPTST(&solv->noupdate, p - installed->start))
954 r = solv->rules + solv->updaterules + (p - installed->start);
958 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
960 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "@@@ re-enabling ");
961 printrule(solv, SAT_DEBUG_SOLUTIONS, r);
965 case SOLVER_ERASE_SOLVABLE:
966 s = pool->solvables + what;
967 if (s->repo != installed)
969 if (MAPTST(&solv->noupdate, what - installed->start))
971 r = solv->rules + solv->updaterules + (what - installed->start);
975 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
977 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "@@@ re-enabling ");
978 printrule(solv, SAT_DEBUG_SOLUTIONS, r);
981 case SOLVER_ERASE_SOLVABLE_NAME: /* remove by capability */
982 case SOLVER_ERASE_SOLVABLE_PROVIDES:
983 name = (how == SOLVER_ERASE_SOLVABLE_NAME) ? what : 0;
984 while (ISRELDEP(name))
986 Reldep *rd = GETRELDEP(pool, name);
989 FOR_PROVIDES(p, pp, what)
991 if (name && pool->solvables[p].name != name)
993 if (pool->solvables[p].repo != installed)
995 if (MAPTST(&solv->noupdate, p - installed->start))
997 r = solv->rules + solv->updaterules + (p - installed->start);
1000 enablerule(solv, r);
1001 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
1003 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "@@@ re-enabling ");
1004 printrule(solv, SAT_DEBUG_SOLUTIONS, r);
1014 for (i = 0; i < installed->nsolvables; i++)
1016 r = solv->rules + solv->updaterules + i;
1017 if (r->w1 && MAPTST(&solv->noupdate, i))
1018 disablerule(solv, r); /* was enabled, need to disable */
1019 r = solv->rules + solv->featurerules + i;
1020 if (r->w1 && MAPTST(&solv->noupdate, i))
1021 disablerule(solv, r); /* was enabled, need to disable */
1027 addpatchatomrequires(Solver *solv, Solvable *s, Id *dp, Queue *q, Map *m)
1029 Pool *pool = solv->pool;
1030 Id fre, *frep, p, *pp, ndp;
1036 queue_init_buffer(&fq, qbuf, sizeof(qbuf)/sizeof(*qbuf));
1037 queue_push(&fq, -(s - pool->solvables));
1039 queue_push(&fq, *dp);
1040 ndp = pool_queuetowhatprovides(pool, &fq);
1041 frep = s->repo->idarraydata + s->freshens;
1042 while ((fre = *frep++) != 0)
1044 FOR_PROVIDES(p, pp, fre)
1046 ps = pool->solvables + p;
1047 addrule(solv, -p, ndp);
1055 for (i = 1; i < fq.count; i++)
1068 * add (install) rules for solvable
1069 * for unfulfilled requirements, conflicts, obsoletes,....
1070 * add a negative assertion for solvables that are not installable
1074 addrpmrulesforsolvable(Solver *solv, Solvable *s, Map *m)
1076 Pool *pool = solv->pool;
1077 Repo *installed = solv->installed;
1092 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforsolvable -----\n");
1094 queue_init_buffer(&q, qbuf, sizeof(qbuf)/sizeof(*qbuf));
1095 queue_push(&q, s - pool->solvables); /* push solvable Id */
1101 * s: Pointer to solvable
1104 n = queue_shift(&q);
1105 if (MAPTST(m, n)) /* continue if already done */
1109 s = pool->solvables + n; /* s = Solvable in question */
1112 if (installed /* Installed system available */
1113 && !solv->fixsystem /* NOT repair errors in rpm dependency graph */
1114 && s->repo == installed) /* solvable is installed? */
1116 dontfix = 1; /* dont care about broken rpm deps */
1119 if (!dontfix && s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
1121 POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "package %s [%d] is not installable\n", solvable2str(pool, s), (Id)(s - pool->solvables));
1122 addrule(solv, -n, 0); /* uninstallable */
1126 if (s->freshens && !s->supplements)
1128 const char *name = id2str(pool, s->name);
1129 if (name[0] == 'a' && !strncmp(name, "atom:", 5))
1133 /*-----------------------------------------
1134 * check requires of s
1139 reqp = s->repo->idarraydata + s->requires;
1140 while ((req = *reqp++) != 0) /* go throw all requires */
1142 if (req == SOLVABLE_PREREQMARKER) /* skip the marker */
1145 dp = pool_whatprovides(pool, req);
1147 if (*dp == SYSTEMSOLVABLE) /* always installed */
1153 addpatchatomrequires(solv, s, dp, &q, m);
1159 /* the strategy here is to not insist on dependencies
1160 * that are already broken. so if we find one provider
1161 * that was already installed, we know that the
1162 * dependency was not broken before so we enforce it */
1163 for (i = 0; (p = dp[i]) != 0; i++) /* for all providers */
1165 if (pool->solvables[p].repo == installed)
1166 break; /* provider was installed */
1168 if (!p) /* previously broken dependency */
1170 POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "ignoring broken requires %s of installed package %s\n", dep2str(pool, req), solvable2str(pool, s));
1177 /* nothing provides req! */
1178 POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "package %s [%d] is not installable (%s)\n", solvable2str(pool, s), (Id)(s - pool->solvables), dep2str(pool, req));
1179 addrule(solv, -n, 0); /* mark requestor as uninstallable */
1183 IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
1185 POOL_DEBUG(SAT_DEBUG_RULE_CREATION," %s requires %s\n", solvable2str(pool, s), dep2str(pool, req));
1186 for (i = 0; dp[i]; i++)
1187 POOL_DEBUG(SAT_DEBUG_RULE_CREATION, " provided by %s\n", solvable2str(pool, pool->solvables + dp[i]));
1190 /* add 'requires' dependency */
1191 /* rule: (-requestor|provider1|provider2|...|providerN) */
1192 addrule(solv, -n, dp - pool->whatprovidesdata);
1194 /* descend the dependency tree */
1195 for (; *dp; dp++) /* loop through all providers */
1197 if (!MAPTST(m, *dp))
1198 queue_push(&q, *dp);
1201 } /* while, requirements of n */
1203 } /* if, requirements */
1205 /* that's all we check for src packages */
1206 if (s->arch == ARCH_SRC || s->arch == ARCH_NOSRC)
1209 /*-----------------------------------------
1210 * check conflicts of s
1215 conp = s->repo->idarraydata + s->conflicts;
1216 while ((con = *conp++) != 0)
1218 FOR_PROVIDES(p, pp, con)
1220 /* dontfix: dont care about conflicts with already installed packs */
1221 if (dontfix && pool->solvables[p].repo == installed)
1223 if (p == n && !solv->allowselfconflicts)
1224 p = 0; /* make it a negative assertion */
1225 /* rule: -n|-p: either solvable _or_ provider of conflict */
1226 addrule(solv, -n, -p);
1231 /*-----------------------------------------
1232 * check obsoletes if not installed
1234 if (!installed || pool->solvables[n].repo != installed)
1235 { /* not installed */
1238 obsp = s->repo->idarraydata + s->obsoletes;
1239 while ((obs = *obsp++) != 0)
1241 FOR_PROVIDES(p, pp, obs)
1242 addrule(solv, -n, -p);
1245 FOR_PROVIDES(p, pp, s->name)
1247 if (s->name == pool->solvables[p].name)
1248 addrule(solv, -n, -p);
1252 /*-----------------------------------------
1253 * add recommends to the rule list
1257 recp = s->repo->idarraydata + s->recommends;
1258 while ((rec = *recp++) != 0)
1260 FOR_PROVIDES(p, pp, rec)
1267 sugp = s->repo->idarraydata + s->suggests;
1268 while ((sug = *sugp++) != 0)
1270 FOR_PROVIDES(p, pp, sug)
1277 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforsolvable end -----\n");
1281 addrpmrulesforweak(Solver *solv, Map *m)
1283 Pool *pool = solv->pool;
1288 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforweak -----\n");
1289 for (i = n = 1; n < pool->nsolvables; i++, n++)
1291 if (i == pool->nsolvables)
1295 s = pool->solvables + i;
1296 if (!pool_installable(pool, s))
1301 supp = s->repo->idarraydata + s->supplements;
1302 while ((sup = *supp++) != ID_NULL)
1303 if (dep_possible(solv, sup, m))
1306 if (!sup && s->freshens)
1308 supp = s->repo->idarraydata + s->freshens;
1309 while ((sup = *supp++) != ID_NULL)
1310 if (dep_possible(solv, sup, m))
1313 if (!sup && s->enhances)
1315 supp = s->repo->idarraydata + s->enhances;
1316 while ((sup = *supp++) != ID_NULL)
1317 if (dep_possible(solv, sup, m))
1322 addrpmrulesforsolvable(solv, s, m);
1325 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforweak end -----\n");
1329 addrpmrulesforupdaters(Solver *solv, Solvable *s, Map *m, int allowall)
1331 Pool *pool = solv->pool;
1336 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforupdaters -----\n");
1338 queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1339 policy_findupdatepackages(solv, s, &qs, allowall);
1340 if (!MAPTST(m, s - pool->solvables)) /* add rule for s if not already done */
1341 addrpmrulesforsolvable(solv, s, m);
1342 for (i = 0; i < qs.count; i++)
1343 if (!MAPTST(m, qs.elements[i]))
1344 addrpmrulesforsolvable(solv, pool->solvables + qs.elements[i], m);
1347 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforupdaters -----\n");
1351 * add rule for update
1352 * (A|A1|A2|A3...) An = update candidates for A
1354 * s = (installed) solvable
1358 addupdaterule(Solver *solv, Solvable *s, int allowall)
1360 /* installed packages get a special upgrade allowed rule */
1361 Pool *pool = solv->pool;
1366 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addupdaterule -----\n");
1368 queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1369 policy_findupdatepackages(solv, s, &qs, allowall);
1370 if (qs.count == 0) /* no updaters found */
1373 d = pool_queuetowhatprovides(pool, &qs); /* intern computed queue */
1375 addrule(solv, s - pool->solvables, d); /* allow update of s */
1376 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addupdaterule end -----\n");
1380 /*-----------------------------------------------------------------*/
1389 printWatches(Solver *solv, int type)
1391 Pool *pool = solv->pool;
1394 POOL_DEBUG(type, "Watches: \n");
1395 for (counter = -(pool->nsolvables - 1); counter < pool->nsolvables; counter++)
1396 POOL_DEBUG(type, " solvable [%d] -- rule [%d]\n", counter, solv->watches[counter + pool->nsolvables]);
1402 * initial setup for all watches
1406 makewatches(Solver *solv)
1410 int nsolvables = solv->pool->nsolvables;
1412 sat_free(solv->watches);
1413 /* lower half for removals, upper half for installs */
1414 solv->watches = sat_calloc(2 * nsolvables, sizeof(Id));
1416 /* do it reverse so rpm rules get triggered first (XXX: obsolete?) */
1417 for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
1419 for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
1422 if (!r->w1 /* rule is disabled */
1423 || !r->w2) /* rule is assertion */
1426 /* see addwatches(solv, r) */
1427 r->n1 = solv->watches[nsolvables + r->w1];
1428 solv->watches[nsolvables + r->w1] = r - solv->rules;
1430 r->n2 = solv->watches[nsolvables + r->w2];
1431 solv->watches[nsolvables + r->w2] = r - solv->rules;
1437 * add watches (for rule)
1441 addwatches(Solver *solv, Rule *r)
1443 int nsolvables = solv->pool->nsolvables;
1445 r->n1 = solv->watches[nsolvables + r->w1];
1446 solv->watches[nsolvables + r->w1] = r - solv->rules;
1448 r->n2 = solv->watches[nsolvables + r->w2];
1449 solv->watches[nsolvables + r->w2] = r - solv->rules;
1453 /*-----------------------------------------------------------------*/
1454 /* rule propagation */
1456 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
1457 #define DECISIONMAP_FALSE(p) ((p) > 0 ? (decisionmap[p] < 0) : (decisionmap[-p] > 0))
1462 * propagate decision to all rules
1463 * return : 0 = everything is OK
1464 * watched rule = there is a conflict
1468 propagate(Solver *solv, int level)
1470 Pool *pool = solv->pool;
1475 Id *decisionmap = solv->decisionmap;
1476 Id *watches = solv->watches + pool->nsolvables;
1478 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate -----\n");
1480 while (solv->propagate_index < solv->decisionq.count)
1482 /* negate because our watches trigger if literal goes FALSE */
1483 pkg = -solv->decisionq.elements[solv->propagate_index++];
1484 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1486 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagate for decision %d level %d\n", -pkg, level);
1487 printruleelement(solv, SAT_DEBUG_PROPAGATE, 0, -pkg);
1489 printWatches(solv, SAT_DEBUG_SCHUBI);
1492 for (rp = watches + pkg; *rp; rp = nrp)
1494 r = solv->rules + *rp;
1496 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1498 POOL_DEBUG(SAT_DEBUG_PROPAGATE," watch triggered ");
1499 printrule(solv, SAT_DEBUG_PROPAGATE, r);
1504 ow = r->w2; /* regard the second watchpoint to come to a solution */
1509 ow = r->w1; /* regard the first watchpoint to come to a solution */
1512 /* if clause is TRUE, nothing to do */
1513 if (DECISIONMAP_TRUE(ow))
1518 /* not a binary clause, check if we need to move our watch */
1519 /* search for a literal that is not ow and not false */
1520 /* (true is also ok, in that case the rule is fulfilled) */
1521 if (r->p && r->p != ow && !DECISIONMAP_TRUE(-r->p))
1524 for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
1525 if (p != ow && !DECISIONMAP_TRUE(-p))
1529 /* p is free to watch, move watch to p */
1530 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1533 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " -> move w%d to %s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables + p));
1535 POOL_DEBUG(SAT_DEBUG_PROPAGATE," -> move w%d to !%s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables - p));
1549 watches[p] = r - solv->rules;
1553 /* unit clause found, set other watch to TRUE */
1554 if (DECISIONMAP_TRUE(-ow))
1555 return r; /* eek, a conflict! */
1556 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1558 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " unit ");
1559 printrule(solv, SAT_DEBUG_PROPAGATE, r);
1562 decisionmap[ow] = level;
1564 decisionmap[-ow] = -level;
1565 queue_push(&solv->decisionq, ow);
1566 queue_push(&solv->decisionq_why, r - solv->rules);
1567 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1569 Solvable *s = pool->solvables + (ow > 0 ? ow : -ow);
1571 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " -> decided to install %s\n", solvable2str(pool, s));
1573 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " -> decided to conflict %s\n", solvable2str(pool, s));
1577 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate end-----\n");
1579 return 0; /* all is well */
1583 /*-----------------------------------------------------------------*/
1592 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp)
1594 Pool *pool = solv->pool;
1597 Map seen; /* global? */
1600 int num = 0, l1num = 0;
1601 int learnt_why = solv->learnt_pool.count;
1602 Id *decisionmap = solv->decisionmap;
1606 POOL_DEBUG(SAT_DEBUG_ANALYZE, "ANALYZE at %d ----------------------\n", level);
1607 map_init(&seen, pool->nsolvables);
1608 idx = solv->decisionq.count;
1611 IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1612 printruleclass(solv, SAT_DEBUG_ANALYZE, c);
1613 queue_push(&solv->learnt_pool, c - solv->rules);
1614 dp = c->d ? pool->whatprovidesdata + c->d : 0;
1615 /* go through all literals of the rule */
1627 if (DECISIONMAP_TRUE(v)) /* the one true literal */
1629 vv = v > 0 ? v : -v;
1630 if (MAPTST(&seen, vv))
1632 l = solv->decisionmap[vv];
1637 l1num++; /* need to do this one in level1 pass */
1638 else if (l == level)
1639 num++; /* need to do this one as well */
1642 queue_push(&r, v); /* not level1 or conflict level, add to new rule */
1648 if (!num && !--l1num)
1649 break; /* all level 1 literals done */
1653 v = solv->decisionq.elements[--idx];
1654 vv = v > 0 ? v : -v;
1655 if (MAPTST(&seen, vv))
1659 if (num && --num == 0)
1661 *pr = -v; /* so that v doesn't get lost */
1664 POOL_DEBUG(SAT_DEBUG_ANALYZE, "got %d involved level 1 decisions\n", l1num);
1665 for (i = 0; i < r.count; i++)
1666 MAPCLR(&seen, r.elements[i]);
1667 /* only level 1 marks left */
1671 why = solv->decisionq_why.elements[idx];
1672 if (!why) /* just in case, maye for SYSTEMSOLVABLE */
1674 c = solv->rules + why;
1680 else if (r.count == 1 && r.elements[0] < 0)
1681 *dr = r.elements[0];
1683 *dr = pool_queuetowhatprovides(pool, &r);
1684 IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1686 POOL_DEBUG(SAT_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level);
1687 printruleelement(solv, SAT_DEBUG_ANALYZE, 0, *pr);
1688 for (i = 0; i < r.count; i++)
1689 printruleelement(solv, SAT_DEBUG_ANALYZE, 0, r.elements[i]);
1691 /* push end marker on learnt reasons stack */
1692 queue_push(&solv->learnt_pool, 0);
1701 * reset the solver decisions to right after the rpm rules.
1702 * called after rules have been enabled/disabled
1706 reset_solver(Solver *solv)
1708 Pool *pool = solv->pool;
1712 /* rewind decisions to direct rpm rule assertions */
1713 for (i = solv->decisionq.count - 1; i >= solv->directdecisions; i--)
1715 v = solv->decisionq.elements[i];
1716 solv->decisionmap[v > 0 ? v : -v] = 0;
1719 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions done reduced from %d to %d\n", solv->decisionq.count, solv->directdecisions);
1721 solv->decisionq_why.count = solv->directdecisions;
1722 solv->decisionq.count = solv->directdecisions;
1723 solv->recommends_index = -1;
1724 solv->propagate_index = 0;
1726 /* adapt learnt rule status to new set of enabled/disabled rules */
1727 enabledisablelearntrules(solv);
1729 /* redo all job/update decisions */
1730 makeruledecisions(solv);
1731 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count);
1733 /* recreate watch chains */
1739 * analyze_unsolvable_rule
1743 analyze_unsolvable_rule(Solver *solv, Rule *r, Id *lastweakp)
1745 Pool *pool = solv->pool;
1747 Id why = r - solv->rules;
1749 IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE)
1750 printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
1751 if (solv->learntrules && why >= solv->learntrules)
1753 for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1754 if (solv->learnt_pool.elements[i] > 0)
1755 analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], lastweakp);
1758 if (MAPTST(&solv->weakrulemap, why))
1759 if (!*lastweakp || why > *lastweakp)
1761 /* do not add rpm rules to problem */
1762 if (why < solv->jobrules)
1764 /* turn rule into problem */
1765 if (why >= solv->jobrules && why < solv->updaterules)
1766 why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
1767 /* return if problem already countains our rule */
1768 if (solv->problems.count)
1770 for (i = solv->problems.count - 1; i >= 0; i--)
1771 if (solv->problems.elements[i] == 0) /* end of last problem reached? */
1773 else if (solv->problems.elements[i] == why)
1776 queue_push(&solv->problems, why);
1781 * analyze_unsolvable
1783 * return: 1 - disabled some rules, try again
1788 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
1790 Pool *pool = solv->pool;
1792 Map seen; /* global to speed things up? */
1795 Id *decisionmap = solv->decisionmap;
1796 int oldproblemcount;
1797 int oldlearntpoolcount;
1800 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n");
1801 oldproblemcount = solv->problems.count;
1802 oldlearntpoolcount = solv->learnt_pool.count;
1804 /* make room for proof index */
1805 /* must update it later, as analyze_unsolvable_rule would confuse
1806 * it with a rule index if we put the real value in already */
1807 queue_push(&solv->problems, 0);
1810 map_init(&seen, pool->nsolvables);
1811 queue_push(&solv->learnt_pool, r - solv->rules);
1813 analyze_unsolvable_rule(solv, r, &lastweak);
1814 dp = r->d ? pool->whatprovidesdata + r->d : 0;
1825 if (DECISIONMAP_TRUE(v)) /* the one true literal */
1827 vv = v > 0 ? v : -v;
1828 l = solv->decisionmap[vv];
1833 idx = solv->decisionq.count;
1836 v = solv->decisionq.elements[--idx];
1837 vv = v > 0 ? v : -v;
1838 if (!MAPTST(&seen, vv))
1840 why = solv->decisionq_why.elements[idx];
1841 queue_push(&solv->learnt_pool, why);
1842 r = solv->rules + why;
1843 analyze_unsolvable_rule(solv, r, &lastweak);
1844 dp = r->d ? pool->whatprovidesdata + r->d : 0;
1855 if (DECISIONMAP_TRUE(v)) /* the one true literal */
1857 vv = v > 0 ? v : -v;
1858 l = solv->decisionmap[vv];
1865 queue_push(&solv->problems, 0); /* mark end of this problem */
1869 /* disable last weak rule */
1870 solv->problems.count = oldproblemcount;
1871 solv->learnt_pool.count = oldlearntpoolcount;
1872 r = solv->rules + lastweak;
1873 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling ");
1874 printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
1875 disablerule(solv, r);
1881 queue_push(&solv->learnt_pool, 0);
1882 solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
1886 for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
1887 disableproblem(solv, solv->problems.elements[i]);
1888 /* XXX: might want to enable all weak rules again */
1892 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "UNSOLVABLE\n");
1897 /*-----------------------------------------------------------------*/
1898 /* Decision revert */
1902 * revert decision at level
1906 revert(Solver *solv, int level)
1908 Pool *pool = solv->pool;
1910 while (solv->decisionq.count)
1912 v = solv->decisionq.elements[solv->decisionq.count - 1];
1913 vv = v > 0 ? v : -v;
1914 if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1916 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1917 if (v > 0 && solv->recommendations.count && v == solv->recommendations.elements[solv->recommendations.count - 1])
1918 solv->recommendations.count--;
1919 solv->decisionmap[vv] = 0;
1920 solv->decisionq.count--;
1921 solv->decisionq_why.count--;
1922 solv->propagate_index = solv->decisionq.count;
1924 while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
1926 solv->branches.count--;
1927 while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
1928 solv->branches.count--;
1930 solv->recommends_index = -1;
1935 * watch2onhighest - put watch2 on literal with highest level
1939 watch2onhighest(Solver *solv, Rule *r)
1945 return; /* binary rule, both watches are set */
1946 dp = solv->pool->whatprovidesdata + r->d;
1947 while ((v = *dp++) != 0)
1949 l = solv->decisionmap[v < 0 ? -v : v];
1964 * add free decision to decisionq, increase level and
1965 * propagate decision, return if no conflict.
1966 * in conflict case, analyze conflict rule, add resulting
1967 * rule to learnt rule set, make decision from learnt
1968 * rule (always unit) and re-propagate.
1970 * returns the new solver level or 0 if unsolvable
1975 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
1977 Pool *pool = solv->pool;
1986 solv->decisionmap[decision] = level;
1988 solv->decisionmap[-decision] = -level;
1989 queue_push(&solv->decisionq, decision);
1990 queue_push(&solv->decisionq_why, 0);
1994 r = propagate(solv, level);
1998 return analyze_unsolvable(solv, r, disablerules);
1999 POOL_DEBUG(SAT_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules));
2000 l = analyze(solv, level, r, &p, &d, &why); /* learnt rule in p and d */
2001 assert(l > 0 && l < level);
2002 POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l);
2004 revert(solv, level);
2005 r = addrule(solv, p, d); /* p requires d */
2007 assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules);
2008 queue_push(&solv->learnt_why, why);
2011 /* at least 2 literals, needs watches */
2012 watch2onhighest(solv, r);
2013 addwatches(solv, r);
2015 solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
2016 queue_push(&solv->decisionq, p);
2017 queue_push(&solv->decisionq_why, r - solv->rules);
2018 IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
2020 POOL_DEBUG(SAT_DEBUG_ANALYZE, "decision: ");
2021 printruleelement(solv, SAT_DEBUG_ANALYZE, 0, p);
2022 POOL_DEBUG(SAT_DEBUG_ANALYZE, "new rule: ");
2023 printrule(solv, SAT_DEBUG_ANALYZE, r);
2031 * install best package from the queue. We add an extra package, inst, if
2032 * provided. See comment in weak install section.
2034 * returns the new solver level or 0 if unsolvable
2038 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
2040 Pool *pool = solv->pool;
2044 if (dq->count > 1 || inst)
2045 policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
2050 /* choose the supplemented one */
2051 for (i = 0; i < dq->count; i++)
2052 if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
2056 for (i = 1; i < dq->count; i++)
2057 queue_push(&solv->branches, dq->elements[i]);
2058 queue_push(&solv->branches, -level);
2062 p = dq->elements[i];
2064 POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvable2str(pool, pool->solvables + p));
2066 return setpropagatelearn(solv, level, p, disablerules);
2070 /*-----------------------------------------------------------------*/
2071 /* Main solver interface */
2076 * create solver structure
2078 * pool: all available solvables
2079 * installed: installed Solvables
2082 * Upon solving, rules are created to flag the Solvables
2083 * of the 'installed' Repo as installed.
2087 solver_create(Pool *pool, Repo *installed)
2090 solv = (Solver *)sat_calloc(1, sizeof(Solver));
2092 solv->installed = installed;
2094 queue_init(&solv->ruletojob);
2095 queue_init(&solv->decisionq);
2096 queue_init(&solv->decisionq_why);
2097 queue_init(&solv->problems);
2098 queue_init(&solv->suggestions);
2099 queue_init(&solv->recommendations);
2100 queue_init(&solv->learnt_why);
2101 queue_init(&solv->learnt_pool);
2102 queue_init(&solv->branches);
2103 queue_init(&solv->covenantq);
2104 queue_init(&solv->weakruleq);
2106 map_init(&solv->recommendsmap, pool->nsolvables);
2107 map_init(&solv->suggestsmap, pool->nsolvables);
2108 map_init(&solv->noupdate, installed ? installed->end - installed->start : 0);
2109 solv->recommends_index = 0;
2111 solv->decisionmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
2113 solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
2114 memset(solv->rules, 0, sizeof(Rule));
2125 solver_free(Solver *solv)
2127 queue_free(&solv->ruletojob);
2128 queue_free(&solv->decisionq);
2129 queue_free(&solv->decisionq_why);
2130 queue_free(&solv->learnt_why);
2131 queue_free(&solv->learnt_pool);
2132 queue_free(&solv->problems);
2133 queue_free(&solv->suggestions);
2134 queue_free(&solv->recommendations);
2135 queue_free(&solv->branches);
2136 queue_free(&solv->covenantq);
2137 queue_free(&solv->weakruleq);
2139 map_free(&solv->recommendsmap);
2140 map_free(&solv->suggestsmap);
2141 map_free(&solv->noupdate);
2142 map_free(&solv->weakrulemap);
2144 sat_free(solv->decisionmap);
2145 sat_free(solv->rules);
2146 sat_free(solv->watches);
2147 sat_free(solv->obsoletes);
2148 sat_free(solv->obsoletes_data);
2153 /*-------------------------------------------------------*/
2158 * all rules have been set up, now actually run the solver
2163 run_solver(Solver *solv, int disablerules, int doweak)
2171 Pool *pool = solv->pool;
2174 IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
2176 POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
2177 for (i = 1; i < solv->nrules; i++)
2178 printruleclass(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
2181 POOL_DEBUG(SAT_DEBUG_STATS, "initial decisions: %d\n", solv->decisionq.count);
2183 IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2184 printdecisions(solv);
2186 /* start SAT algorithm */
2188 systemlevel = level + 1;
2189 POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n");
2194 * here's the main loop:
2195 * 1) propagate new decisions (only needed for level 1)
2196 * 2) try to keep installed packages
2197 * 3) fulfill all unresolved rules
2198 * 4) install recommended packages
2199 * 5) minimalize solution if we had choices
2200 * if we encounter a problem, we rewind to a safe level and restart
2212 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d; size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
2213 if ((r = propagate(solv, level)) != 0)
2215 if (analyze_unsolvable(solv, r, disablerules))
2223 * installed packages
2226 if (level < systemlevel && solv->installed && solv->installed->nsolvables)
2228 if (!solv->updatesystem)
2230 /* try to keep as many packages as possible */
2231 POOL_DEBUG(SAT_DEBUG_STATS, "installing old packages\n");
2232 for (i = solv->installed->start; i < solv->installed->end; i++)
2234 s = pool->solvables + i;
2235 if (s->repo != solv->installed)
2237 if (solv->decisionmap[i] != 0)
2239 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "keeping %s\n", solvable2str(pool, s));
2241 level = setpropagatelearn(solv, level, i, disablerules);
2247 if (level <= olevel)
2250 if (i < solv->installed->end)
2253 POOL_DEBUG(SAT_DEBUG_STATS, "resolving update/feature rules\n");
2254 for (i = solv->installed->start, r = solv->rules + solv->updaterules; i < solv->installed->end; i++, r++)
2257 s = pool->solvables + i;
2258 if (s->repo != solv->installed)
2260 if (solv->decisionmap[i] > 0)
2262 /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2263 if (MAPTST(&solv->noupdate, i - solv->installed->start))
2266 if (!solv->allowuninstall)
2270 rr += solv->installed->end - solv->installed->start;
2273 rr = solv->rules + solv->featurerules + (i - solv->installed->start);
2276 if (!rr->w2 || solv->decisionmap[rr->w2] > 0)
2278 if (solv->decisionmap[rr->w2] == 0)
2279 queue_push(&dq, rr->w2);
2283 dp = pool->whatprovidesdata + rr->d;
2284 while ((p = *dp++) != 0)
2286 if (solv->decisionmap[p] > 0)
2288 if (solv->decisionmap[p] == 0)
2294 if (!dq.count && solv->decisionmap[i] != 0)
2297 /* FIXME: i is handled a bit different because we do not want
2298 * to have it pruned just because it is not recommened.
2299 * we should not prune installed packages instead */
2300 level = selectandinstall(solv, level, &dq, (solv->decisionmap[i] ? 0 : i), disablerules);
2306 if (level <= olevel)
2309 if (i < solv->installed->end)
2311 systemlevel = level;
2318 POOL_DEBUG(SAT_DEBUG_STATS, "deciding unresolved rules\n");
2319 for (i = 1, n = 1; ; i++, n++)
2321 if (n == solv->nrules)
2323 if (i == solv->nrules)
2325 r = solv->rules + i;
2326 if (!r->w1) /* ignore disabled rules */
2331 /* binary or unary rule */
2332 /* need two positive undecided literals */
2333 if (r->p < 0 || r->w2 <= 0)
2335 if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2337 queue_push(&dq, r->p);
2338 queue_push(&dq, r->w2);
2343 * all negative literals are installed
2344 * no positive literal is installed
2345 * i.e. the rule is not fulfilled and we
2346 * just need to decide on the positive literals
2350 if (solv->decisionmap[-r->p] <= 0)
2355 if (solv->decisionmap[r->p] > 0)
2357 if (solv->decisionmap[r->p] == 0)
2358 queue_push(&dq, r->p);
2360 dp = pool->whatprovidesdata + r->d;
2361 while ((p = *dp++) != 0)
2365 if (solv->decisionmap[-p] <= 0)
2370 if (solv->decisionmap[p] > 0)
2372 if (solv->decisionmap[p] == 0)
2379 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
2381 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
2382 printruleclass(solv, SAT_DEBUG_PROPAGATE, r);
2384 /* dq.count < 2 cannot happen as this means that
2385 * the rule is unit */
2386 assert(dq.count > 1);
2389 level = selectandinstall(solv, level, &dq, 0, disablerules);
2395 if (level < systemlevel)
2398 } /* for(), decide */
2400 if (n != solv->nrules) /* continue if level < systemlevel */
2407 POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended packages\n");
2409 for (i = 1; i < pool->nsolvables; i++)
2411 if (solv->decisionmap[i] < 0)
2413 if (solv->decisionmap[i] > 0)
2415 Id *recp, rec, *pp, p;
2416 s = pool->solvables + i;
2417 /* installed, check for recommends */
2418 /* XXX need to special case AND ? */
2421 recp = s->repo->idarraydata + s->recommends;
2422 while ((rec = *recp++) != 0)
2425 FOR_PROVIDES(p, pp, rec)
2427 if (solv->decisionmap[p] > 0)
2432 else if (solv->decisionmap[p] == 0)
2434 queue_pushunique(&dq, p);
2442 s = pool->solvables + i;
2443 if (!s->supplements && !s->freshens)
2445 if (!pool_installable(pool, s))
2447 if (solver_is_supplementing(solv, s))
2448 queue_pushunique(&dq, i);
2454 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2456 POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2457 queue_push(&solv->recommendations, p);
2458 level = setpropagatelearn(solv, level, p, 0);
2463 if (solv->solution_callback)
2465 solv->solution_callback(solv, solv->solution_callback_data);
2466 if (solv->branches.count)
2468 int i = solv->branches.count - 1;
2469 int l = -solv->branches.elements[i];
2471 if (solv->branches.elements[i - 1] < 0)
2473 p = solv->branches.elements[i];
2474 POOL_DEBUG(SAT_DEBUG_STATS, "branching with %s\n", solvable2str(pool, pool->solvables + p));
2476 for (j = i + 1; j < solv->branches.count; j++)
2477 queue_push(&dq, solv->branches.elements[j]);
2478 solv->branches.count = i;
2480 revert(solv, level);
2482 for (j = 0; j < dq.count; j++)
2483 queue_push(&solv->branches, dq.elements[j]);
2485 level = setpropagatelearn(solv, level, p, disablerules);
2493 /* all branches done, we're finally finished */
2497 /* minimization step */
2498 if (solv->branches.count)
2500 int l = 0, lasti = -1, lastl = -1;
2502 for (i = solv->branches.count - 1; i >= 0; i--)
2504 p = solv->branches.elements[i];
2507 else if (p > 0 && solv->decisionmap[p] > l + 1)
2515 /* kill old solvable so that we do not loop */
2516 p = solv->branches.elements[lasti];
2517 solv->branches.elements[lasti] = 0;
2518 POOL_DEBUG(SAT_DEBUG_STATS, "minimizing %d -> %d with %s\n", solv->decisionmap[p], l, solvable2str(pool, pool->solvables + p));
2521 revert(solv, level);
2523 level = setpropagatelearn(solv, level, p, disablerules);
2534 POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
2541 * at this point, all rules that led to conflicts are disabled.
2542 * we re-enable all rules of a problem set but rule "sug", then
2543 * continue to disable more rules until there as again a solution.
2546 /* FIXME: think about conflicting assertions */
2549 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2551 Pool *pool = solv->pool;
2557 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2559 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
2560 for (i = 0; problem[i]; i++)
2562 if (problem[i] == sug)
2563 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
2564 printproblem(solv, problem[i]);
2567 queue_init(&disabled);
2568 queue_empty(refined);
2569 queue_push(refined, sug);
2571 /* re-enable all problem rules with the exception of "sug"(gestion) */
2575 for (i = 0; problem[i]; i++)
2576 if (problem[i] != sug)
2577 enableproblem(solv, problem[i]);
2580 disableupdaterules(solv, job, -(sug + 1));
2584 int njob, nfeature, nupdate;
2585 queue_empty(&solv->problems);
2586 enableweakrules(solv);
2587 revert(solv, 1); /* XXX no longer needed? */
2590 if (!solv->problems.count)
2591 run_solver(solv, 0, 0);
2593 if (!solv->problems.count)
2595 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
2596 IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2597 printdecisions(solv);
2598 break; /* great, no more problems */
2600 disabledcnt = disabled.count;
2601 /* start with 1 to skip over proof index */
2602 njob = nfeature = nupdate = 0;
2603 for (i = 1; i < solv->problems.count - 1; i++)
2605 /* ignore solutions in refined */
2606 v = solv->problems.elements[i];
2608 break; /* end of problem reached */
2609 for (j = 0; problem[j]; j++)
2610 if (problem[j] != sug && problem[j] == v)
2614 if (v >= solv->featurerules && v < solv->learntrules)
2620 queue_push(&disabled, v);
2622 if (disabled.count == disabledcnt)
2624 /* no solution found, this was an invalid suggestion! */
2625 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
2629 if (!njob && nupdate && nfeature)
2631 /* got only update rules, filter out feature rules */
2632 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "throwing away feature rules\n");
2633 for (i = j = disabledcnt; i < disabled.count; i++)
2635 v = disabled.elements[i];
2636 if (v < solv->featurerules || v >= solv->learntrules)
2637 disabled.elements[j++] = v;
2642 if (disabled.count == disabledcnt + 1)
2644 /* just one suggestion, add it to refined list */
2645 v = disabled.elements[disabledcnt];
2647 queue_push(refined, v); /* do not record feature rules */
2648 disableproblem(solv, v);
2649 if (v >= solv->updaterules && v < solv->featurerules)
2651 Rule *r = solv->rules + v + (solv->installed->end - solv->installed->start);
2653 enablerule(solv, r); /* enable corresponding feature rule */
2656 disableupdaterules(solv, job, -(v + 1));
2660 /* more than one solution, disable all */
2661 /* do not push anything on refine list, as we do not know which solution to choose */
2662 /* thus, the user will get another problem if he selects this solution, where he
2663 * can choose the right one */
2664 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2666 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
2667 for (i = disabledcnt; i < disabled.count; i++)
2668 printproblem(solv, disabled.elements[i]);
2670 for (i = disabledcnt; i < disabled.count; i++)
2672 v = disabled.elements[i];
2673 disableproblem(solv, v);
2674 if (v >= solv->updaterules && v < solv->featurerules)
2676 Rule *r = solv->rules + v + (solv->installed->end - solv->installed->start);
2678 enablerule(solv, r);
2683 /* all done, get us back into the same state as before */
2684 /* enable refined rules again */
2685 for (i = 0; i < disabled.count; i++)
2686 enableproblem(solv, disabled.elements[i]);
2687 /* disable problem rules again */
2688 for (i = 0; problem[i]; i++)
2689 disableproblem(solv, problem[i]);
2690 disableupdaterules(solv, job, -1);
2691 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
2695 problems_to_solutions(Solver *solv, Queue *job)
2697 Pool *pool = solv->pool;
2705 if (!solv->problems.count)
2707 queue_clone(&problems, &solv->problems);
2708 queue_init(&solution);
2709 queue_init(&solutions);
2710 /* copy over proof index */
2711 queue_push(&solutions, problems.elements[0]);
2712 problem = problems.elements + 1;
2713 for (i = 1; i < problems.count; i++)
2715 Id v = problems.elements[i];
2718 /* mark end of this problem */
2719 queue_push(&solutions, 0);
2720 queue_push(&solutions, 0);
2721 if (i + 1 == problems.count)
2723 /* copy over proof of next problem */
2724 queue_push(&solutions, problems.elements[i + 1]);
2726 problem = problems.elements + i + 1;
2729 refine_suggestion(solv, job, problem, v, &solution);
2730 if (!solution.count)
2731 continue; /* this solution didn't work out */
2733 for (j = 0; j < solution.count; j++)
2735 why = solution.elements[j];
2736 /* must be either job descriptor or update rule */
2737 assert(why < 0 || (why >= solv->updaterules && why < solv->featurerules));
2739 printproblem(solv, why);
2743 /* job descriptor */
2744 queue_push(&solutions, 0);
2745 queue_push(&solutions, -why);
2749 /* update rule, find replacement package */
2752 p = solv->installed->start + (why - solv->updaterules);
2753 if (solv->decisionmap[p] > 0)
2754 continue; /* false alarm, turned out we can keep the package */
2755 rr = solv->rules + solv->featurerules + (why - solv->updaterules);
2757 rr = solv->rules + why;
2762 if (solv->decisionmap[rr->w2] > 0 && pool->solvables[rr->w2].repo != solv->installed)
2767 Id *dp = pool->whatprovidesdata + rr->d;
2770 if (solv->decisionmap[*dp] > 0 && pool->solvables[*dp].repo != solv->installed)
2778 queue_push(&solutions, p);
2779 queue_push(&solutions, rp);
2782 /* mark end of this solution */
2783 queue_push(&solutions, 0);
2784 queue_push(&solutions, 0);
2786 queue_free(&solution);
2787 queue_free(&problems);
2788 /* copy queue over to solutions */
2789 queue_free(&solv->problems);
2790 queue_clone(&solv->problems, &solutions);
2792 /* bring solver back into problem state */
2793 revert(solv, 1); /* XXX move to reset_solver? */
2796 assert(solv->problems.count == solutions.count);
2797 queue_free(&solutions);
2801 solver_next_problem(Solver *solv, Id problem)
2805 return solv->problems.count ? 1 : 0;
2806 pp = solv->problems.elements + problem;
2807 while (pp[0] || pp[1])
2811 while (pp[0] || pp[1])
2816 problem = pp - solv->problems.elements;
2817 if (problem >= solv->problems.count)
2823 solver_next_solution(Solver *solv, Id problem, Id solution)
2829 pp = solv->problems.elements + solution;
2830 return pp[0] || pp[1] ? solution : 0;
2832 pp = solv->problems.elements + solution;
2833 while (pp[0] || pp[1])
2836 solution = pp - solv->problems.elements;
2837 return pp[0] || pp[1] ? solution : 0;
2841 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
2844 element = element ? element + 2 : solution;
2845 pp = solv->problems.elements + element;
2846 if (!(pp[0] || pp[1]))
2855 * create obsoletesmap from solver decisions
2856 * required for decision handling
2858 * for solvables in installed repo:
2860 * p - one of the packages that obsolete us
2862 * n - number of packages this package obsoletes
2866 create_decisions_obsoletesmap(Solver *solv)
2868 Pool *pool = solv->pool;
2869 Repo *installed = solv->installed;
2870 Id p, *obsoletesmap = NULL;
2874 obsoletesmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
2877 for (i = 0; i < solv->decisionq.count; i++)
2881 n = solv->decisionq.elements[i];
2884 if (n == SYSTEMSOLVABLE)
2886 s = pool->solvables + n;
2887 if (s->repo == installed) /* obsoletes don't count for already installed packages */
2889 FOR_PROVIDES(p, pp, s->name)
2890 if (s->name == pool->solvables[p].name)
2892 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2894 obsoletesmap[p] = n;
2899 for (i = 0; i < solv->decisionq.count; i++)
2904 n = solv->decisionq.elements[i];
2907 if (n == SYSTEMSOLVABLE)
2909 s = pool->solvables + n;
2910 if (s->repo == installed) /* obsoletes don't count for already installed packages */
2914 obsp = s->repo->idarraydata + s->obsoletes;
2915 while ((obs = *obsp++) != 0)
2916 FOR_PROVIDES(p, pp, obs)
2918 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2920 obsoletesmap[p] = n;
2926 return obsoletesmap;
2934 printdecisions(Solver *solv)
2936 Pool *pool = solv->pool;
2937 Repo *installed = solv->installed;
2938 Id p, *obsoletesmap = create_decisions_obsoletesmap( solv );
2942 IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2944 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- Decisions -----\n");
2945 for (i = 0; i < solv->decisionq.count; i++)
2947 p = solv->decisionq.elements[i];
2948 printruleelement(solv, SAT_DEBUG_SCHUBI, 0, p);
2950 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- Decisions end -----\n");
2953 /* print solvables to be erased */
2957 FOR_REPO_SOLVABLES(installed, p, s)
2959 if (solv->decisionmap[p] >= 0)
2961 if (obsoletesmap[p])
2963 POOL_DEBUG(SAT_DEBUG_RESULT, "erase %s\n", solvable2str(pool, s));
2967 /* print solvables to be installed */
2969 for (i = 0; i < solv->decisionq.count; i++)
2972 p = solv->decisionq.elements[i];
2975 if (p == SYSTEMSOLVABLE)
2977 s = pool->solvables + p;
2978 if (installed && s->repo == installed)
2981 if (!obsoletesmap[p])
2983 POOL_DEBUG(SAT_DEBUG_RESULT, "install %s", solvable2str(pool, s));
2988 FOR_PROVIDES(xp, xpp, s->name)
2990 Solvable *s2 = pool->solvables + xp;
2991 if (s2->name != s->name)
2993 if (evrcmp(pool, s->evr, s2->evr, EVRCMP_MATCH_RELEASE) < 0)
2997 POOL_DEBUG(SAT_DEBUG_RESULT, "downgrade %s", solvable2str(pool, s));
2999 POOL_DEBUG(SAT_DEBUG_RESULT, "upgrade %s", solvable2str(pool, s));
3000 POOL_DEBUG(SAT_DEBUG_RESULT, " (obsoletes");
3001 for (j = installed->start; j < installed->end; j++)
3002 if (obsoletesmap[j] == p)
3003 POOL_DEBUG(SAT_DEBUG_RESULT, " %s", solvable2str(pool, pool->solvables + j));
3004 POOL_DEBUG(SAT_DEBUG_RESULT, ")");
3006 POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
3009 sat_free(obsoletesmap);
3011 if (solv->recommendations.count)
3013 POOL_DEBUG(SAT_DEBUG_RESULT, "\nrecommended packages:\n");
3014 for (i = 0; i < solv->recommendations.count; i++)
3016 s = pool->solvables + solv->recommendations.elements[i];
3017 POOL_DEBUG(SAT_DEBUG_RESULT, "- %s%s\n", solvable2str(pool, s), solv->decisionmap[solv->recommendations.elements[i]] > 0 ? " (selected)" : "");
3021 if (solv->suggestions.count)
3023 POOL_DEBUG(SAT_DEBUG_RESULT, "\nsuggested packages:\n");
3024 for (i = 0; i < solv->suggestions.count; i++)
3026 s = pool->solvables + solv->suggestions.elements[i];
3027 POOL_DEBUG(SAT_DEBUG_RESULT, "- %s\n", solvable2str(pool, s));
3033 /* this is basically the reverse of addrpmrulesforsolvable */
3035 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
3037 Pool *pool = solv->pool;
3038 Repo *installed = solv->installed;
3042 Id p, *pp, req, *reqp, con, *conp, obs, *obsp, *dp;
3045 if (rid >= solv->updaterules)
3048 *sourcep = solv->installed->start + (rid - solv->updaterules);
3050 return SOLVER_PROBLEM_UPDATE_RULE;
3052 if (rid >= solv->jobrules)
3055 r = solv->rules + rid;
3056 p = solv->ruletojob.elements[rid - solv->jobrules];
3057 *depp = job->elements[p + 1];
3059 *targetp = job->elements[p];
3060 if (r->d == 0 && r->w2 == 0 && r->p == -SYSTEMSOLVABLE && job->elements[p] != SOLVER_INSTALL_SOLVABLE_ONE_OF)
3061 return SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP;
3062 return SOLVER_PROBLEM_JOB_RULE;
3064 r = solv->rules + rid;
3066 if (r->d == 0 && r->w2 == 0)
3068 /* a rpm rule assertion */
3069 s = pool->solvables - r->p;
3070 if (installed && !solv->fixsystem && s->repo == installed)
3072 assert(!dontfix); /* dontfix packages never have a neg assertion */
3075 /* see why the package is not installable */
3076 if (s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
3079 return SOLVER_PROBLEM_NOT_INSTALLABLE;
3081 /* check requires */
3084 reqp = s->repo->idarraydata + s->requires;
3085 while ((req = *reqp++) != 0)
3087 if (req == SOLVABLE_PREREQMARKER)
3089 dp = pool_whatprovides(pool, req);
3096 return SOLVER_PROBLEM_NOTHING_PROVIDES_DEP;
3099 assert(!solv->allowselfconflicts);
3100 assert(s->conflicts);
3101 conp = s->repo->idarraydata + s->conflicts;
3102 while ((con = *conp++) != 0)
3103 FOR_PROVIDES(p, pp, con)
3107 return SOLVER_PROBLEM_SELF_CONFLICT;
3111 s = pool->solvables - r->p;
3112 if (installed && !solv->fixsystem && s->repo == installed)
3114 if (r->d == 0 && r->w2 < 0)
3116 /* a package conflict */
3117 Solvable *s2 = pool->solvables - r->w2;
3120 if (installed && !solv->fixsystem && s2->repo == installed)
3123 /* if both packages have the same name and at least one of them
3124 * is not installed, they conflict */
3125 if (s->name == s2->name && (!installed || (s->repo != installed || s2->repo != installed)))
3130 return SOLVER_PROBLEM_SAME_NAME;
3133 /* check conflicts in both directions */
3136 conp = s->repo->idarraydata + s->conflicts;
3137 while ((con = *conp++) != 0)
3139 FOR_PROVIDES(p, pp, con)
3141 if (dontfix && pool->solvables[p].repo == installed)
3148 return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3154 conp = s2->repo->idarraydata + s2->conflicts;
3155 while ((con = *conp++) != 0)
3157 FOR_PROVIDES(p, pp, con)
3159 if (dontfix2 && pool->solvables[p].repo == installed)
3166 return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3170 /* check obsoletes in both directions */
3171 if ((!installed || s->repo != installed) && s->obsoletes)
3173 obsp = s->repo->idarraydata + s->obsoletes;
3174 while ((obs = *obsp++) != 0)
3176 FOR_PROVIDES(p, pp, obs)
3183 return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3187 if ((!installed || s2->repo != installed) && s2->obsoletes)
3189 obsp = s2->repo->idarraydata + s2->obsoletes;
3190 while ((obs = *obsp++) != 0)
3192 FOR_PROVIDES(p, pp, obs)
3199 return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3203 /* all cases checked, can't happen */
3206 /* simple requires */
3207 assert(s->requires);
3208 reqp = s->repo->idarraydata + s->requires;
3209 while ((req = *reqp++) != 0)
3211 if (req == SOLVABLE_PREREQMARKER)
3213 dp = pool_whatprovides(pool, req);
3216 if (*dp == r->w2 && dp[1] == 0)
3219 else if (dp - pool->whatprovidesdata == r->d)
3226 return SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE;
3230 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
3233 Id lreqr, lconr, lsysr, ljobr;
3237 lreqr = lconr = lsysr = ljobr = 0;
3238 while ((rid = solv->learnt_pool.elements[idx++]) != 0)
3241 if (rid >= solv->learntrules)
3242 findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
3243 else if (rid >= solv->updaterules)
3248 else if (rid >= solv->jobrules)
3255 r = solv->rules + rid;
3256 if (!r->d && r->w2 < 0)
3263 if (r->d == 0 && r->w2 == 0 && !reqassert)
3265 /* prefer assertions (XXX: bad idea?) */
3271 else if (solv->installed && r->p < 0 && solv->pool->solvables[-r->p].repo == solv->installed)
3273 /* prefer rules of installed packages */
3274 Id op = *reqrp >= 0 ? solv->rules[*reqrp].p : -*reqrp;
3275 if (op <= 0 || solv->pool->solvables[op].repo != solv->installed)
3281 if (!*reqrp && lreqr)
3283 if (!*conrp && lconr)
3285 if (!*jobrp && ljobr)
3287 if (!*sysrp && lsysr)
3292 * search for a rule that describes the problem to the
3293 * user. A pretty hopeless task, actually. We currently
3294 * prefer simple requires.
3297 solver_findproblemrule(Solver *solv, Id problem)
3299 Id reqr, conr, sysr, jobr;
3300 Id idx = solv->problems.elements[problem - 1];
3301 reqr = conr = sysr = jobr = 0;
3302 findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
3315 printprobleminfo(Solver *solv, Queue *job, Id problem)
3317 Pool *pool = solv->pool;
3319 Id dep, source, target;
3322 probr = solver_findproblemrule(solv, problem);
3323 switch (solver_problemruleinfo(solv, job, probr, &dep, &source, &target))
3325 case SOLVER_PROBLEM_UPDATE_RULE:
3326 s = pool_id2solvable(pool, source);
3327 POOL_DEBUG(SAT_DEBUG_RESULT, "problem with installed package %s\n", solvable2str(pool, s));
3329 case SOLVER_PROBLEM_JOB_RULE:
3330 POOL_DEBUG(SAT_DEBUG_RESULT, "conflicting requests\n");
3332 case SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP:
3333 POOL_DEBUG(SAT_DEBUG_RESULT, "nothing provides requested %s\n", dep2str(pool, dep));
3335 case SOLVER_PROBLEM_NOT_INSTALLABLE:
3336 s = pool_id2solvable(pool, source);
3337 POOL_DEBUG(SAT_DEBUG_RESULT, "package %s is not installable\n", solvable2str(pool, s));
3339 case SOLVER_PROBLEM_NOTHING_PROVIDES_DEP:
3340 s = pool_id2solvable(pool, source);
3341 POOL_DEBUG(SAT_DEBUG_RESULT, "nothing provides %s needed by %s\n", dep2str(pool, dep), solvable2str(pool, s));
3343 case SOLVER_PROBLEM_SAME_NAME:
3344 s = pool_id2solvable(pool, source);
3345 s2 = pool_id2solvable(pool, target);
3346 POOL_DEBUG(SAT_DEBUG_RESULT, "cannot install both %s and %s\n", solvable2str(pool, s), solvable2str(pool, s2));
3348 case SOLVER_PROBLEM_PACKAGE_CONFLICT:
3349 s = pool_id2solvable(pool, source);
3350 s2 = pool_id2solvable(pool, target);
3351 POOL_DEBUG(SAT_DEBUG_RESULT, "package %s conflicts with %s provided by %s\n", solvable2str(pool, s), dep2str(pool, dep), solvable2str(pool, s2));
3353 case SOLVER_PROBLEM_PACKAGE_OBSOLETES:
3354 s = pool_id2solvable(pool, source);
3355 s2 = pool_id2solvable(pool, target);
3356 POOL_DEBUG(SAT_DEBUG_RESULT, "package %s obsoletes %s provided by %s\n", solvable2str(pool, s), dep2str(pool, dep), solvable2str(pool, s2));
3358 case SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE:
3359 s = pool_id2solvable(pool, source);
3360 POOL_DEBUG(SAT_DEBUG_RESULT, "package %s requires %s, but none of the providers can be installed\n", solvable2str(pool, s), dep2str(pool, dep));
3362 case SOLVER_PROBLEM_SELF_CONFLICT:
3363 s = pool_id2solvable(pool, source);
3364 POOL_DEBUG(SAT_DEBUG_RESULT, "package %s conflicts with %s provided by itself\n", solvable2str(pool, s), dep2str(pool, dep));
3370 printsolutions(Solver *solv, Queue *job)
3372 Pool *pool = solv->pool;
3374 Id p, rp, how, what;
3375 Id problem, solution, element;
3378 POOL_DEBUG(SAT_DEBUG_RESULT, "Encountered problems! Here are the solutions:\n\n");
3381 while ((problem = solver_next_problem(solv, problem)) != 0)
3383 POOL_DEBUG(SAT_DEBUG_RESULT, "Problem %d:\n", pcnt++);
3384 POOL_DEBUG(SAT_DEBUG_RESULT, "====================================\n");
3385 printprobleminfo(solv, job, problem);
3386 POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
3388 while ((solution = solver_next_solution(solv, problem, solution)) != 0)
3391 while ((element = solver_next_solutionelement(solv, problem, solution, element, &p, &rp)) != 0)
3395 /* job, rp is index into job queue */
3396 how = job->elements[rp - 1] & ~SOLVER_WEAK;
3397 what = job->elements[rp];
3400 case SOLVER_INSTALL_SOLVABLE:
3401 s = pool->solvables + what;
3402 if (solv->installed && s->repo == solv->installed)
3403 POOL_DEBUG(SAT_DEBUG_RESULT, "- do not keep %s installed\n", solvable2str(pool, s));
3405 POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install %s\n", solvable2str(pool, s));
3407 case SOLVER_ERASE_SOLVABLE:
3408 s = pool->solvables + what;
3409 if (solv->installed && s->repo == solv->installed)
3410 POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall %s\n", solvable2str(pool, s));
3412 POOL_DEBUG(SAT_DEBUG_RESULT, "- do not forbid installation of %s\n", solvable2str(pool, s));
3414 case SOLVER_INSTALL_SOLVABLE_NAME:
3415 POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install %s\n", dep2str(pool, what));
3417 case SOLVER_ERASE_SOLVABLE_NAME:
3418 POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall %s\n", dep2str(pool, what));
3420 case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3421 POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install a solvable providing %s\n", dep2str(pool, what));
3423 case SOLVER_ERASE_SOLVABLE_PROVIDES:
3424 POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall all solvables providing %s\n", dep2str(pool, what));
3426 case SOLVER_INSTALL_SOLVABLE_UPDATE:
3427 s = pool->solvables + what;
3428 POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install most recent version of %s\n", solvable2str(pool, s));
3431 POOL_DEBUG(SAT_DEBUG_RESULT, "- do something different\n");
3437 /* policy, replace p with rp */
3438 s = pool->solvables + p;
3439 sd = rp ? pool->solvables + rp : 0;
3443 if (!solv->allowdowngrade && evrcmp(pool, s->evr, sd->evr, EVRCMP_MATCH_RELEASE) > 0)
3445 POOL_DEBUG(SAT_DEBUG_RESULT, "- allow downgrade of %s to %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3448 if (!solv->allowarchchange && s->name == sd->name && s->arch != sd->arch && policy_illegal_archchange(solv, s, sd))
3450 POOL_DEBUG(SAT_DEBUG_RESULT, "- allow architecture change of %s to %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3453 if (!solv->allowvendorchange && s->name == sd->name && s->vendor != sd->vendor && policy_illegal_vendorchange(solv, s, sd))
3456 POOL_DEBUG(SAT_DEBUG_RESULT, "- allow vendor change from '%s' (%s) to '%s' (%s)\n", id2str(pool, s->vendor), solvable2str(pool, s), id2str(pool, sd->vendor), solvable2str(pool, sd));
3458 POOL_DEBUG(SAT_DEBUG_RESULT, "- allow vendor change from '%s' (%s) to no vendor (%s)\n", id2str(pool, s->vendor), solvable2str(pool, s), solvable2str(pool, sd));
3462 POOL_DEBUG(SAT_DEBUG_RESULT, "- allow replacement of %s with %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3466 POOL_DEBUG(SAT_DEBUG_RESULT, "- allow deinstallation of %s\n", solvable2str(pool, s));
3471 POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
3477 /* create reverse obsoletes map for installed solvables
3479 * for each installed solvable find which packages with *different* names
3480 * obsolete the solvable.
3481 * this index is used in policy_findupdatepackages if noupdateprovide is set.
3485 create_obsolete_index(Solver *solv)
3487 Pool *pool = solv->pool;
3489 Repo *installed = solv->installed;
3490 Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
3493 if (!installed || !installed->nsolvables)
3495 solv->obsoletes = obsoletes = sat_calloc(installed->end - installed->start, sizeof(Id));
3496 for (i = 1; i < pool->nsolvables; i++)
3498 s = pool->solvables + i;
3499 if (s->repo == installed)
3503 if (!pool_installable(pool, s))
3505 obsp = s->repo->idarraydata + s->obsoletes;
3506 while ((obs = *obsp++) != 0)
3507 FOR_PROVIDES(p, pp, obs)
3509 if (pool->solvables[p].repo != installed)
3511 if (pool->solvables[p].name == s->name)
3513 obsoletes[p - installed->start]++;
3517 for (i = 0; i < installed->nsolvables; i++)
3520 n += obsoletes[i] + 1;
3523 solv->obsoletes_data = obsoletes_data = sat_calloc(n + 1, sizeof(Id));
3524 POOL_DEBUG(SAT_DEBUG_STATS, "obsoletes data: %d entries\n", n + 1);
3525 for (i = pool->nsolvables - 1; i > 0; i--)
3527 s = pool->solvables + i;
3528 if (s->repo == installed)
3532 if (!pool_installable(pool, s))
3534 obsp = s->repo->idarraydata + s->obsoletes;
3535 while ((obs = *obsp++) != 0)
3536 FOR_PROVIDES(p, pp, obs)
3538 if (pool->solvables[p].repo != installed)
3540 if (pool->solvables[p].name == s->name)
3542 p -= installed->start;
3543 if (obsoletes_data[obsoletes[p]] != i)
3544 obsoletes_data[--obsoletes[p]] = i;
3550 removedisabledconflicts(Solver *solv, Queue *removed)
3552 Pool *pool = solv->pool;
3557 Id *decisionmap = solv->decisionmap;
3559 POOL_DEBUG(SAT_DEBUG_STATS, "removedisabledconflicts\n");
3560 queue_empty(removed);
3561 for (i = 0; i < solv->decisionq.count; i++)
3563 p = solv->decisionq.elements[i];
3566 /* a conflict. we never do conflicts on free decisions, so there
3567 * must have been an unit rule */
3568 why = solv->decisionq_why.elements[i];
3570 r = solv->rules + why;
3571 if (!r->w1 && decisionmap[-p])
3573 /* rule is now disabled, remove from decisionmap */
3574 POOL_DEBUG(SAT_DEBUG_STATS, "removing conflict for package %s[%d]\n", solvable2str(pool, pool->solvables - p), -p);
3575 queue_push(removed, -p);
3576 queue_push(removed, decisionmap[-p]);
3577 decisionmap[-p] = 0;
3580 if (!removed->count)
3582 /* we removed some confliced packages. some of them might still
3583 * be in conflict, so search for unit rules and re-conflict */
3585 for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++)
3587 if (i == solv->nrules)
3590 r = solv->rules + i;
3596 if (r->p < 0 && !decisionmap[-r->p])
3602 if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2))
3604 else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p))
3609 if (r->p < 0 && decisionmap[-r->p] == 0)
3611 if (new || DECISIONMAP_FALSE(r->p))
3613 dp = pool->whatprovidesdata + r->d;
3614 while ((p = *dp++) != 0)
3616 if (new && p == new)
3618 if (p < 0 && decisionmap[-p] == 0)
3627 else if (!DECISIONMAP_FALSE(p))
3637 POOL_DEBUG(SAT_DEBUG_STATS, "re-conflicting package %s[%d]\n", solvable2str(pool, pool->solvables - new), -new);
3638 decisionmap[-new] = -1;
3639 n = 0; /* redo all rules */
3645 weaken_solvable_deps(Solver *solv, Id p)
3650 for (i = 1, r = solv->rules + i; i < solv->jobrules; i++, r++)
3654 if (r->d == 0 && r->w2 < 0)
3655 continue; /* conflict */
3656 queue_push(&solv->weakruleq, i);
3660 /*-----------------------------------------------------------------*/
3670 solver_solve(Solver *solv, Queue *job)
3672 Pool *pool = solv->pool;
3673 Repo *installed = solv->installed;
3676 Map addedmap; /* '1' == have rpm-rules for solvable */
3677 Id how, what, weak, name, p, *pp, d;
3683 /* create whatprovides if not already there */
3684 if (!pool->whatprovides)
3685 pool_createwhatprovides(pool);
3687 /* create obsolete index if needed */
3688 if (solv->noupdateprovide)
3689 create_obsolete_index(solv);
3692 * create basic rule set of all involved packages
3693 * use addedmap bitmap to make sure we don't create rules twice
3697 map_init(&addedmap, pool->nsolvables);
3701 * always install our system solvable
3703 MAPSET(&addedmap, SYSTEMSOLVABLE);
3704 queue_push(&solv->decisionq, SYSTEMSOLVABLE);
3705 queue_push(&solv->decisionq_why, 0);
3706 solv->decisionmap[SYSTEMSOLVABLE] = 1;
3709 * create rules for all package that could be involved with the solving
3710 * so called: rpm rules
3715 oldnrules = solv->nrules;
3716 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
3717 FOR_REPO_SOLVABLES(installed, p, s)
3718 addrpmrulesforsolvable(solv, s, &addedmap);
3719 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
3720 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
3721 oldnrules = solv->nrules;
3722 FOR_REPO_SOLVABLES(installed, p, s)
3723 addrpmrulesforupdaters(solv, s, &addedmap, 1);
3724 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
3727 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
3728 oldnrules = solv->nrules;
3729 for (i = 0; i < job->count; i += 2)
3731 how = job->elements[i] & ~SOLVER_WEAK;
3732 what = job->elements[i + 1];
3736 case SOLVER_INSTALL_SOLVABLE:
3737 addrpmrulesforsolvable(solv, pool->solvables + what, &addedmap);
3739 case SOLVER_INSTALL_SOLVABLE_NAME:
3740 case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3741 name = (how == SOLVER_INSTALL_SOLVABLE_NAME) ? what : 0;
3742 while (ISRELDEP(name))
3744 Reldep *rd = GETRELDEP(pool, name);
3747 FOR_PROVIDES(p, pp, what)
3749 /* if by name, ensure that the name matches */
3750 if (name && pool->solvables[p].name != name)
3752 addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3755 case SOLVER_INSTALL_SOLVABLE_UPDATE:
3756 /* dont allow downgrade */
3757 addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
3759 case SOLVER_INSTALL_SOLVABLE_ONE_OF:
3760 pp = pool->whatprovidesdata + what;
3761 while ((p = *pp++) != 0)
3762 addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3766 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
3768 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for recommended/suggested packages ***\n");
3770 oldnrules = solv->nrules;
3771 addrpmrulesforweak(solv, &addedmap);
3772 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
3774 IF_POOLDEBUG (SAT_DEBUG_STATS)
3776 int possible = 0, installable = 0;
3777 for (i = 1; i < pool->nsolvables; i++)
3779 if (pool_installable(pool, pool->solvables + i))
3781 if (MAPTST(&addedmap, i))
3784 POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
3788 * first pass done, we now have all the rpm rules we need.
3789 * unify existing rules before going over all job rules and
3791 * at this point the system is always solvable,
3792 * as an empty system (remove all packages) is a valid solution
3795 unifyrules(solv); /* remove duplicate rpm rules */
3796 solv->directdecisions = solv->decisionq.count;
3798 POOL_DEBUG(SAT_DEBUG_STATS, "decisions so far: %d\n", solv->decisionq.count);
3799 IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
3800 printdecisions (solv);
3803 * now add all job rules
3806 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
3808 solv->jobrules = solv->nrules;
3810 for (i = 0; i < job->count; i += 2)
3812 oldnrules = solv->nrules;
3814 how = job->elements[i] & ~SOLVER_WEAK;
3815 weak = job->elements[i] & SOLVER_WEAK;
3816 what = job->elements[i + 1];
3819 case SOLVER_INSTALL_SOLVABLE: /* install specific solvable */
3820 s = pool->solvables + what;
3821 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall solvable %s\n", weak ? "weak " : "", solvable2str(pool, s));
3822 addrule(solv, what, 0); /* install by Id */
3823 queue_push(&solv->ruletojob, i);
3825 queue_push(&solv->weakruleq, solv->nrules - 1);
3827 case SOLVER_ERASE_SOLVABLE:
3828 s = pool->solvables + what;
3829 POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase solvable %s\n", weak ? "weak " : "", solvable2str(pool, s));
3830 addrule(solv, -what, 0); /* remove by Id */
3831 queue_push(&solv->ruletojob, i);
3833 queue_push(&solv->weakruleq, solv->nrules - 1);
3835 case SOLVER_INSTALL_SOLVABLE_NAME: /* install by capability */
3836 case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3837 if (how == SOLVER_INSTALL_SOLVABLE_NAME)
3838 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall name %s\n", weak ? "weak " : "", dep2str(pool, what));
3839 if (how == SOLVER_INSTALL_SOLVABLE_PROVIDES)
3840 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall provides %s\n", weak ? "weak " : "", dep2str(pool, what));
3842 name = (how == SOLVER_INSTALL_SOLVABLE_NAME) ? what : 0;
3843 while (ISRELDEP(name))
3845 Reldep *rd = GETRELDEP(pool, name);
3848 FOR_PROVIDES(p, pp, what)
3850 /* if by name, ensure that the name matches */
3851 if (name && pool->solvables[p].name != name)
3857 /* no provider, make this an impossible rule */
3858 queue_push(&q, -SYSTEMSOLVABLE);
3861 p = queue_shift(&q); /* get first provider */
3863 d = 0; /* single provider ? -> make assertion */
3865 d = pool_queuetowhatprovides(pool, &q); /* get all providers */
3866 addrule(solv, p, d); /* add 'requires' rule */
3867 queue_push(&solv->ruletojob, i);
3869 queue_push(&solv->weakruleq, solv->nrules - 1);
3871 case SOLVER_ERASE_SOLVABLE_NAME: /* remove by capability */
3872 case SOLVER_ERASE_SOLVABLE_PROVIDES:
3873 if (how == SOLVER_ERASE_SOLVABLE_NAME)
3874 POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase name %s\n", weak ? "weak " : "", dep2str(pool, what));
3875 if (how == SOLVER_ERASE_SOLVABLE_PROVIDES)
3876 POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase provides %s\n", weak ? "weak " : "", dep2str(pool, what));
3877 name = (how == SOLVER_ERASE_SOLVABLE_NAME) ? what : 0;
3878 while (ISRELDEP(name))
3880 Reldep *rd = GETRELDEP(pool, name);
3883 FOR_PROVIDES(p, pp, what)
3885 /* if by name, ensure that the name matches */
3886 if (name && pool->solvables[p].name != name)
3888 addrule(solv, -p, 0); /* add 'remove' rule */
3889 queue_push(&solv->ruletojob, i);
3891 queue_push(&solv->weakruleq, solv->nrules - 1);
3894 case SOLVER_INSTALL_SOLVABLE_UPDATE: /* find update for solvable */
3895 s = pool->solvables + what;
3896 POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solvable2str(pool, s));
3897 addupdaterule(solv, s, 0);
3898 queue_push(&solv->ruletojob, i);
3900 queue_push(&solv->weakruleq, solv->nrules - 1);
3902 case SOLVER_INSTALL_SOLVABLE_ONE_OF:
3903 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sone of\n", weak ? "weak " : "");
3904 for (pp = pool->whatprovidesdata + what; *pp; pp++)
3905 POOL_DEBUG(SAT_DEBUG_JOB, " %s\n", solvable2str(pool, pool->solvables + *pp));
3906 addrule(solv, -SYSTEMSOLVABLE, what);
3907 queue_push(&solv->ruletojob, i);
3909 queue_push(&solv->weakruleq, solv->nrules - 1);
3911 case SOLVER_WEAKEN_SOLVABLE_DEPS:
3912 s = pool->solvables + what;
3913 POOL_DEBUG(SAT_DEBUG_JOB, "job: weaken deps %s\n", solvable2str(pool, s));
3914 weaken_solvable_deps(solv, what);
3917 IF_POOLDEBUG (SAT_DEBUG_JOB)
3920 if (solv->nrules == oldnrules)
3921 POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n");
3922 for (j = oldnrules; j < solv->nrules; j++)
3924 POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
3925 printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
3929 assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
3932 * now add update rules
3936 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add update rules ***\n");
3941 * create rules for updating installed solvables
3945 solv->updaterules = solv->nrules;
3946 if (installed && !solv->allowuninstall)
3947 { /* loop over all installed solvables */
3948 /* we create all update rules, but disable some later on depending on the job */
3949 for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3951 /* no update rules for patch atoms */
3952 if (s->freshens && !s->supplements)
3954 const char *name = id2str(pool, s->name);
3955 if (name[0] == 'a' && !strncmp(name, "atom:", 5))
3957 addrule(solv, 0, 0);
3961 if (s->repo == installed)
3962 addupdaterule(solv, s, 0); /* allowall = 0 */
3964 addrule(solv, 0, 0); /* create dummy rule */
3966 /* consistency check: we added a rule for _every_ installed solvable */
3967 assert(solv->nrules - solv->updaterules == installed->end - installed->start);
3970 /* create feature rules */
3971 /* those are used later on to keep a version of the installed packages in
3973 solv->featurerules = solv->nrules;
3976 for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3978 if (s->freshens && !s->supplements)
3980 const char *name = id2str(pool, s->name);
3981 if (name[0] == 'a' && !strncmp(name, "atom:", 5))
3983 addrule(solv, 0, 0);
3987 if (s->repo == installed)
3990 addupdaterule(solv, s, 1); /* allowall = 0 */
3991 if (solv->allowuninstall)
3993 queue_push(&solv->weakruleq, solv->nrules - 1);
3996 r = solv->rules + solv->nrules - 1;
3997 sr = r - (installed->end - installed->start);
3999 disablerule(solv, r);
4000 if (sr->p && !unifyrules_sortcmp(r, sr))
4002 /* identical rule, kill feature rule */
4003 memset(r, 0, sizeof(*r));
4007 addrule(solv, 0, 0); /* create dummy rule */
4009 assert(solv->nrules - solv->featurerules == installed->end - installed->start);
4012 /* free unneeded memory */
4013 map_free(&addedmap);
4016 /* create weak map */
4017 map_init(&solv->weakrulemap, solv->nrules);
4018 for (i = 0; i < solv->weakruleq.count; i++)
4020 p = solv->weakruleq.elements[i];
4021 MAPSET(&solv->weakrulemap, p);
4024 /* all new rules are learnt after this point */
4025 solv->learntrules = solv->nrules;
4027 /* disable update rules that conflict with our job */
4028 disableupdaterules(solv, job, -1);
4031 /* make decisions based on job/update assertions */
4032 makeruledecisions(solv);
4034 /* create watches chains */
4037 POOL_DEBUG(SAT_DEBUG_STATS, "problems so far: %d\n", solv->problems.count);
4040 run_solver(solv, 1, solv->dontinstallrecommended ? 0 : 1);
4044 /* disable all erase jobs (continuing weak "keep uninstalled" rules) */
4045 for (i = solv->jobrules, r = solv->rules + i; i < solv->updaterules; i++, r++)
4049 if (r->p > 0) /* install job? */
4051 disablerule(solv, r);
4057 enabledisablelearntrules(solv);
4058 removedisabledconflicts(solv, &redoq);
4061 /* find recommended packages */
4062 /* if redoq.count == 0 we already found all recommended in the
4064 if (redoq.count || solv->dontinstallrecommended)
4066 Id rec, *recp, p, *pp;
4068 /* create map of all suggests that are still open */
4069 solv->recommends_index = -1;
4070 MAPZERO(&solv->recommendsmap);
4071 for (i = 0; i < solv->decisionq.count; i++)
4073 p = solv->decisionq.elements[i];
4076 s = pool->solvables + p;
4079 recp = s->repo->idarraydata + s->recommends;
4080 while ((rec = *recp++) != 0)
4082 FOR_PROVIDES(p, pp, rec)
4083 if (solv->decisionmap[p] > 0)
4086 continue; /* p != 0: already fulfilled */
4087 FOR_PROVIDES(p, pp, rec)
4088 MAPSET(&solv->recommendsmap, p);
4092 for (i = 1; i < pool->nsolvables; i++)
4094 if (solv->decisionmap[i] != 0)
4096 s = pool->solvables + i;
4097 if (!MAPTST(&solv->recommendsmap, i))
4099 if (!s->supplements)
4101 if (!pool_installable(pool, s))
4103 if (!solver_is_supplementing(solv, s))
4106 if (solv->dontinstallrecommended)
4107 queue_push(&solv->recommendations, i);
4109 queue_pushunique(&solv->recommendations, i);
4111 /* we use MODE_SUGGEST here so that repo prio is ignored */
4112 policy_filter_unwanted(solv, &solv->recommendations, 0, POLICY_MODE_SUGGEST);
4115 /* find suggested packages */
4118 Id sug, *sugp, p, *pp;
4120 /* create map of all suggests that are still open */
4121 solv->recommends_index = -1;
4122 MAPZERO(&solv->suggestsmap);
4123 for (i = 0; i < solv->decisionq.count; i++)
4125 p = solv->decisionq.elements[i];
4128 s = pool->solvables + p;
4131 sugp = s->repo->idarraydata + s->suggests;
4132 while ((sug = *sugp++) != 0)
4134 FOR_PROVIDES(p, pp, sug)
4135 if (solv->decisionmap[p] > 0)
4138 continue; /* already fulfilled */
4139 FOR_PROVIDES(p, pp, sug)
4140 MAPSET(&solv->suggestsmap, p);
4144 for (i = 1; i < pool->nsolvables; i++)
4146 if (solv->decisionmap[i] != 0)
4148 s = pool->solvables + i;
4149 if (!MAPTST(&solv->suggestsmap, i))
4153 if (!pool_installable(pool, s))
4155 if (!solver_is_enhancing(solv, s))
4158 queue_push(&solv->suggestions, i);
4160 policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
4165 /* restore decisionmap */
4166 for (i = 0; i < redoq.count; i += 2)
4167 solv->decisionmap[redoq.elements[i]] = redoq.elements[i + 1];
4171 if (solv->problems.count)
4173 int recocount = solv->recommendations.count;
4174 solv->recommendations.count = 0; /* so that revert() doesn't mess with it */
4175 queue_empty(&redoq);
4176 for (i = 0; i < solv->decisionq.count; i++)
4178 Id p = solv->decisionq.elements[i];
4179 queue_push(&redoq, p);
4180 queue_push(&redoq, solv->decisionq_why.elements[i]);
4181 queue_push(&redoq, solv->decisionmap[p > 0 ? p : -p]);
4183 problems_to_solutions(solv, job);
4184 memset(solv->decisionmap, 0, pool->nsolvables * sizeof(Id));
4185 queue_empty(&solv->decisionq);
4186 queue_empty(&solv->decisionq_why);
4187 for (i = 0; i < redoq.count; i += 3)
4189 Id p = redoq.elements[i];
4190 queue_push(&solv->decisionq, p);
4191 queue_push(&solv->decisionq_why, redoq.elements[i + 1]);
4192 solv->decisionmap[p > 0 ? p : -p] = redoq.elements[i + 2];
4194 solv->recommendations.count = recocount;
4199 /***********************************************************************/
4202 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
4206 solver_create_state_maps(solv, &installedmap, 0);
4207 pool_calc_duchanges(solv->pool, solv->installed, &installedmap, mps, nmps);
4208 map_free(&installedmap);
4212 solver_calc_installsizechange(Solver *solv)
4217 solver_create_state_maps(solv, &installedmap, 0);
4218 change = pool_calc_installsizechange(solv->pool, solv->installed, &installedmap);
4219 map_free(&installedmap);