- allow repositories that don't consist of a single block of solvables
[platform/upstream/libsolv.git] / src / solver.c
1 /*
2  * Copyright (c) 2007, Novell Inc.
3  *
4  * This program is licensed under the BSD license, read LICENSE.BSD
5  * for further information
6  */
7
8 /*
9  * solver.c
10  *
11  * SAT based dependency solver
12  */
13
14 #include <stdio.h>
15 #include <stdlib.h>
16 #include <unistd.h>
17 #include <string.h>
18
19 #include "solver.h"
20 #include "bitmap.h"
21 #include "pool.h"
22 #include "util.h"
23 #include "evr.h"
24 #include "policy.h"
25
26 #define RULES_BLOCK 63
27
28
29 int
30 solver_dep_installed(Solver *solv, Id dep)
31 {
32   /* disable for now, splitprovides don't work anyway and it breaks
33      a testcase */
34 #if 0
35   Pool *pool = solv->pool;
36   Id p, *pp;
37
38   if (ISRELDEP(dep))
39     {
40       Reldep *rd = GETRELDEP(pool, dep);
41       if (rd->flags == REL_AND)
42         {
43           if (!solver_dep_installed(solv, rd->name))
44             return 0;
45           return solver_dep_installed(solv, rd->evr);
46         }
47       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
48         return solver_dep_installed(solv, rd->evr);
49     }
50   FOR_PROVIDES(p, pp, dep)
51     {
52       if (p == SYSTEMSOLVABLE || (solv->installed && pool->solvables[p].repo == solv->installed))
53         return 1;
54     }
55 #endif
56   return 0;
57 }
58
59
60 /* this mirrors solver_dep_fulfilled but uses map m instead of the decisionmap */
61 static inline int
62 dep_possible(Solver *solv, Id dep, Map *m)
63 {
64   Pool *pool = solv->pool;
65   Id p, *pp;
66
67   if (ISRELDEP(dep))
68     {
69       Reldep *rd = GETRELDEP(pool, dep);
70       if (rd->flags == REL_AND)
71         {
72           if (!dep_possible(solv, rd->name, m))
73             return 0;
74           return dep_possible(solv, rd->evr, m);
75         }
76       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
77         return solver_dep_installed(solv, rd->evr);
78     }
79   FOR_PROVIDES(p, pp, dep)
80     {
81       if (MAPTST(m, p))
82         return 1;
83     }
84   return 0;
85 }
86
87 /*-----------------------------------------------------------------*/
88
89 /*
90  * print rules
91  */
92
93 static void
94 printruleelement(Solver *solv, Rule *r, Id v)
95 {
96   Pool *pool = solv->pool;
97   Solvable *s;
98   if (v < 0)
99     {
100       s = pool->solvables + -v;
101       printf("    !%s-%s.%s [%d]", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), -v);
102     }
103   else
104     {
105       s = pool->solvables + v;
106       printf("    %s-%s.%s [%d]", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), v);
107     }
108   if (r)
109     {
110       if (r->w1 == v)
111         printf(" (w1)");
112       if (r->w2 == v)
113         printf(" (w2)");
114     }
115   if (solv->decisionmap[s - pool->solvables] > 0)
116     printf(" Install.level%d", solv->decisionmap[s - pool->solvables]);
117   if (solv->decisionmap[s - pool->solvables] < 0)
118     printf(" Conflict.level%d", -solv->decisionmap[s - pool->solvables]);
119   if (r && r->w1 == 0)
120     printf(" (disabled)");
121   printf("\n");
122 }
123
124
125 /*
126  * print rule
127  */
128
129 static void
130 printrule(Solver *solv, Rule *r)
131 {
132   int i;
133   Id v;
134
135   if (r >= solv->rules && r < solv->rules + solv->nrules)   /* r is a solver rule */
136     printf("Rule #%d:\n", (int)(r - solv->rules));
137   else
138     printf("Rule:\n");                 /* r is any rule */
139   for (i = 0; ; i++)
140     {
141       if (i == 0)
142         v = r->p;
143       else if (r->d == ID_NULL)
144         {
145           if (i == 2)
146             break;
147           v = r->w2;
148         }
149       else
150         v = solv->pool->whatprovidesdata[r->d + i - 1];
151       if (v == ID_NULL)
152         break;
153       printruleelement(solv, r, v);
154     }
155   printf("    next: %d %d\n", r->n1, r->n2);
156 }
157
158
159 /*-----------------------------------------------------------------*/
160
161 /*
162  * Rule handling
163  */
164
165 static Pool *unifyrules_sortcmp_data;
166
167 /*
168  * compare rules for unification sort
169  */
170
171 static int
172 unifyrules_sortcmp(const void *ap, const void *bp)
173 {
174   Pool *pool = unifyrules_sortcmp_data;
175   Rule *a = (Rule *)ap;
176   Rule *b = (Rule *)bp;
177   Id *ad, *bd;
178   int x;
179   
180   x = a->p - b->p;
181   if (x)
182     return x;                          /* p differs */
183
184   /* identical p */
185   if (a->d == 0 && b->d == 0)
186     return a->w2 - b->w2;              /* assertion: return w2 diff */
187
188   if (a->d == 0)                       /* a is assertion, b not */
189     {
190       x = a->w2 - pool->whatprovidesdata[b->d];
191       return x ? x : -1;
192     }
193
194   if (b->d == 0)                       /* b is assertion, a not */
195     {
196       x = pool->whatprovidesdata[a->d] - b->w2;
197       return x ? x : 1;
198     }
199
200   /* compare whatprovidesdata */
201   ad = pool->whatprovidesdata + a->d;
202   bd = pool->whatprovidesdata + b->d;
203   while (*bd)
204     if ((x = *ad++ - *bd++) != 0)
205       return x;
206   return *ad;
207 }
208
209
210 /*
211  * unify rules
212  */
213
214 static void
215 unifyrules(Solver *solv)
216 {
217   int i, j;
218   Rule *ir, *jr;
219
220   if (solv->nrules <= 1)               /* nothing to unify */
221     return;
222
223   if (solv->pool->verbose > 3) 
224       printf ("----- unifyrules -----\n");
225
226   /* sort rules first */
227   unifyrules_sortcmp_data = solv->pool;
228   qsort(solv->rules + 1, solv->nrules - 1, sizeof(Rule), unifyrules_sortcmp);
229
230   /* prune rules
231    * i = unpruned
232    * j = pruned
233    */
234   jr = 0;
235   for (i = j = 1, ir = solv->rules + 1; i < solv->nrules; i++, ir++)
236     {
237       if (jr && !unifyrules_sortcmp(ir, jr))
238         continue;                      /* prune! */
239       jr = solv->rules + j++;          /* keep! */
240       if (ir != jr)
241         *jr = *ir;
242     }
243
244   /* reduced count from nrules to j rules */
245   if (solv->pool->verbose) printf("pruned rules from %d to %d\n", solv->nrules, j);
246
247   /* adapt rule buffer */
248   solv->rules = (Rule *)xrealloc(solv->rules, ((solv->nrules + RULES_BLOCK) & ~RULES_BLOCK) * sizeof(Rule));
249   solv->nrules = j;
250 #if 1
251   if (solv->pool->verbose)
252     {
253       int binr = 0;
254       int lits = 0;
255       Id *dp;
256       Rule *r;
257
258       for (i = 1; i < solv->nrules; i++)
259         {
260           r = solv->rules + i;
261           if (r->d == 0)
262             binr++;
263           else
264             {
265               dp = solv->pool->whatprovidesdata + r->d;
266               while (*dp++)
267                 lits++;
268             }
269         }
270       printf("  binary: %d\n", binr);
271       printf("  normal: %d, %d literals\n", solv->nrules - 1 - binr, lits);
272     }
273 #endif
274   if (solv->pool->verbose > 3) 
275       printf ("----- unifyrules end -----\n");  
276 }
277
278 #if 0
279
280 /*
281  * hash rule
282  */
283
284 static Hashval
285 hashrule(Solver *solv, Id p, Id d, int n)
286 {
287   unsigned int x = (unsigned int)p;
288   int *dp;
289
290   if (n <= 1)
291     return (x * 37) ^ (unsigned int)d; 
292   dp = solv->pool->whatprovidesdata + d;
293   while (*dp)
294     x = (x * 37) ^ (unsigned int)*dp++;
295   return x;
296 }
297 #endif
298
299
300 /*
301  * add rule
302  *  p = direct literal; > 0 for learnt, < 0 for installed pkg (rpm)
303  *  d, if < 0 direct literal, if > 0 offset into whatprovides, if == 0 rule is assertion (look at p only)
304  *
305  *
306  * A requires b, b provided by B1,B2,B3 => (-A|B1|B2|B3)
307  * 
308  * p < 0 : rule from rpm (installed pkg)
309  * d > 0 : Offset in whatprovidesdata (list of providers)
310  * 
311  * A conflicts b, b provided by B1,B2,B3 => (-A|-B1), (-A|-B2), (-A|-B3)
312  *  d < 0: Id of solvable (e.g. B1)
313  * 
314  * d == 0: unary rule, assertion => (A) or (-A)
315  * 
316  *   Install:    p > 0, d = 0   (A)             user requested install
317  *   Remove:     p < 0, d = 0   (-A)            user requested remove
318  *   Requires:   p < 0, d > 0   (-A|B1|B2|...)  d: <list of providers for requirement of p>
319  *   Updates:    p > 0, d > 0   (A|B1|B2|...)   d: <list of updates for solvable p>
320  *   Conflicts:  p < 0, d < 0   (-A|-B)         either p (conflict issuer) or d (conflict provider)
321  *   ?           p > 0, d < 0   (A|-B)
322  *   No-op ?:    p = 0, d = 0   (null)          (used as policy rule placeholder)
323  */
324
325 static Rule *
326 addrule(Solver *solv, Id p, Id d)
327 {
328   Rule *r = 0;
329   Id *dp = 0;
330
331   int n = 0;                           /* number of literals in rule - 1
332                                           0 = direct assertion (single literal)
333                                           1 = binary rule
334                                         */
335
336   /* it often happenes that requires lead to adding the same rpm rule
337    * multiple times, so we prune those duplicates right away to make
338    * the work for unifyrules a bit easier */
339
340   if (solv->nrules && !solv->jobrules)
341     {
342       r = solv->rules + solv->nrules - 1;   /* get the last added rule */
343       if (r->p == p && r->d == d && d != 0)   /* identical and not user requested */
344         return r;
345     }
346
347   if (d < 0)
348     {
349       if (p == d)
350         return 0;                      /* ignore self conflict */
351       n = 1;
352     }
353   else if (d == 0)                     /* user requested */
354     n = 0;
355   else
356     {
357       for (dp = solv->pool->whatprovidesdata + d; *dp; dp++, n++)
358         if (*dp == -p)
359           return 0;                     /* rule is self-fulfilling */
360       if (n == 1)
361         d = dp[-1];
362     }
363
364   if (n == 0)                          /* direct assertion */
365     {
366       if (!solv->jobrules)
367         {
368           /* this is a rpm rule assertion, we do not have to allocate it */
369           /* it can be identified by a level of 1 and a zero reason */
370           /* we must not drop those rules from the decisionq when rewinding! */
371           if (p > 0)
372             abort();
373           if (solv->decisionmap[-p] > 0 || solv->decisionmap[-p] < -1)
374             abort();
375           if (solv->decisionmap[-p])
376             return NULL;
377           queue_push(&solv->decisionq, p);
378           queue_push(&solv->decisionq_why, 0);
379           solv->decisionmap[-p] = -1;
380           return 0;
381         }
382     }
383   else if (n == 1 && p > d)
384     {
385       /* smallest literal first so we can find dups */
386       n = p;
387       p = d;
388       d = n;
389       n = 1;                           /* re-set n, was used as temp var */
390     }
391
392   /* check if the last added rule is exactly the same as what we're looking for. */
393   if (r && n == 1 && !r->d && r->p == p && r->w2 == d)
394     return r;
395
396   if (r && n > 1 && r->d && r->p == p)
397     {
398       Id *dp2;
399       if (d == r->d)
400         return r;
401       dp2 = solv->pool->whatprovidesdata + r->d;
402       for (dp = solv->pool->whatprovidesdata + d; *dp; dp++, dp2++)
403         if (*dp != *dp2)
404           break;
405       if (*dp == *dp2)
406         return r;
407    }
408   
409   /*
410    * allocate new rule
411    */
412
413   /* check and extend rule buffer */
414   if ((solv->nrules & RULES_BLOCK) == 0)
415     {
416       solv->rules = (Rule *)xrealloc(solv->rules, (solv->nrules + (RULES_BLOCK + 1)) * sizeof(Rule));
417     }
418
419   r = solv->rules + solv->nrules++;    /* point to rule space */
420
421   r->p = p;
422   if (n == 0)
423     {
424       /* direct assertion, no watch needed */
425       r->d = 0;
426       r->w1 = p;
427       r->w2 = 0;
428     }
429   else if (n == 1)
430     {
431       /* binary rule */
432       r->d = 0;
433       r->w1 = p;
434       r->w2 = d;
435     }
436   else
437     {
438       r->d = d;
439       r->w1 = p;
440       r->w2 = solv->pool->whatprovidesdata[d];
441     }
442   r->n1 = 0;
443   r->n2 = 0;
444
445   if (solv->pool->verbose > 3)
446     {
447       printf ("  Add rule: ");
448       printrule (solv, r);
449     }
450   
451   return r;
452 }
453
454 static inline void
455 disablerule(Solver *solv, Rule *r)
456 {
457   r->w1 = 0;
458 }
459
460 static inline void
461 enablerule(Solver *solv, Rule *r)
462 {
463   if (r->d == 0 || r->w2 != r->p)
464     r->w1 = r->p;
465   else
466     r->w1 = solv->pool->whatprovidesdata[r->d];
467 }
468
469
470 /**********************************************************************************/
471
472 /* a problem is an item on the solver's problem list. It can either be >0, in that
473  * case it is a system (upgrade) rule, or it can be <0, which makes it refer to a job
474  * consisting of multiple job rules.
475  */
476
477 static void 
478 disableproblem(Solver *solv, Id v)
479 {
480   Rule *r;
481   int i;
482   Id *jp;
483
484   if (v > 0)
485     {
486       disablerule(solv, solv->rules + v);
487       return;
488     }
489   v = -(v + 1);
490   jp = solv->ruletojob.elements;
491   for (i = solv->jobrules, r = solv->rules + i; i < solv->systemrules; i++, r++, jp++)
492     if (*jp == v)
493       disablerule(solv, r);
494 }
495
496 static void 
497 enableproblem(Solver *solv, Id v)
498 {
499   Rule *r;
500   int i;
501   Id *jp;
502
503   if (v > 0)
504     {
505       enablerule(solv, solv->rules + v);
506       return;
507     }
508   v = -(v + 1);
509   jp = solv->ruletojob.elements;
510   for (i = solv->jobrules, r = solv->rules + i; i < solv->systemrules; i++, r++, jp++)
511     if (*jp == v)
512       enablerule(solv, r);
513 }
514
515 static void
516 printproblem(Solver *solv, Id v)
517 {
518   int i;
519   Rule *r;
520   Id *jp;
521
522   if (v > 0)
523     printrule(solv, solv->rules + v);
524   else
525     {
526       v = -(v + 1);
527       printf("JOB %d\n", v);
528       jp = solv->ruletojob.elements;
529       for (i = solv->jobrules, r = solv->rules + i; i < solv->systemrules; i++, r++, jp++)
530         if (*jp == v)
531           {
532             printf(" -");
533             printrule(solv, r);
534           }
535       printf("ENDJOB\n");
536     }
537 }
538
539
540 /**********************************************************************************/
541
542 /* go through system and job rules and add direct assertions
543  * to the decisionqueue. If we find a conflict, disable rules and
544  * add them to problem queue.
545  */
546 static void
547 makeruledecisions(Solver *solv)
548 {
549   int i, ri;
550   Rule *r, *rr;
551   Id v, vv;
552   int decisionstart;
553
554   /* no learnt rules for now */
555   if (solv->learntrules && solv->learntrules != solv->nrules)
556     abort();
557
558   decisionstart = solv->decisionq.count;
559   /* the loop is over jobrules, system rules and weak rules */
560   for (ri = solv->jobrules, r = solv->rules + ri; ri < solv->nrules; ri++, r++)
561     {
562       if (!r->w1 || r->w2)
563         continue;
564       v = r->p;
565       vv = v > 0 ? v : -v;
566       if (solv->decisionmap[vv] == 0)
567         {
568           queue_push(&solv->decisionq, v);
569           queue_push(&solv->decisionq_why, r - solv->rules);
570           solv->decisionmap[vv] = v > 0 ? 1 : -1;
571           continue;
572         }
573       if (v > 0 && solv->decisionmap[vv] > 0)
574         continue;
575       if (v < 0 && solv->decisionmap[vv] < 0)
576         continue;
577       /* found a conflict! */
578       /* if we are weak, just disable ourself */
579       if (ri >= solv->weakrules)
580         {
581           printf("conflict, but I am weak, disabling ");
582           printrule(solv, r);
583           r->w1 = 0;
584           continue;
585         }
586       /* only job and system rules left */
587       for (i = 0; i < solv->decisionq.count; i++)
588         if (solv->decisionq.elements[i] == -v)
589           break;
590       if (i == solv->decisionq.count)
591         abort();
592       if (solv->decisionq_why.elements[i] == 0)
593         {
594           /* conflict with rpm rule, need only disable our rule */
595           printf("conflict with rpm rule, disabling rule #%d\n", ri);
596           if (v < 0 && v != -SYSTEMSOLVABLE)
597             abort();
598           queue_push(&solv->problems, 0);
599           if (v == -SYSTEMSOLVABLE)
600             queue_push(&solv->problems, 0);     /* sigh, we don't have a rule for that */
601           else
602             queue_push(&solv->problems, -v);    /* sigh, we don't have a rule for that */
603           v = ri;
604           if (ri < solv->systemrules)
605             v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
606           queue_push(&solv->problems, v);
607           disableproblem(solv, v);
608           queue_push(&solv->problems, 0);
609           continue;
610         }
611       /* conflict with another job or system rule */
612       /* remove old decision */
613       printf("conflicting system/job rules over literal %d\n", vv);
614       queue_push(&solv->problems, 0);
615       queue_push(&solv->problems, solv->decisionq_why.elements[i]);
616       /* push all of our rules asserting this literal on the problem stack */
617       for (i = solv->jobrules, rr = solv->rules + i; i < solv->nrules; i++, rr++)
618         {
619           if (!rr->w1 || rr->w2)
620             continue;
621           if (rr->p != v && rr->p != -v)
622             continue;
623           printf(" - disabling rule #%d\n", i);
624           v = i;
625           if (i < solv->systemrules)
626             v = -(solv->ruletojob.elements[i - solv->jobrules] + 1);
627           queue_push(&solv->problems, v);
628           disableproblem(solv, v);
629         }
630       queue_push(&solv->problems, 0);
631
632       /* start over */
633       while (solv->decisionq.count > decisionstart)
634         {
635           v = solv->decisionq.elements[--solv->decisionq.count];
636           --solv->decisionq_why.count;
637           vv = v > 0 ? v : -v;
638           solv->decisionmap[vv] = 0;
639         }
640       ri = solv->jobrules - 1;
641       r = solv->rules + ri;
642     }
643 }
644
645
646 /* FIXME: bad code ahead, replace as soon as possible */
647 static void
648 disableupdaterules(Solver *solv, Queue *job, int jobidx)
649 {
650   Pool *pool = solv->pool;
651   int i, j;
652   Id how, what, p, *pp;
653   Solvable *s;
654   Repo *installed;
655   Rule *r;
656   Id lastjob = -1;
657
658   installed = solv->installed;
659   if (!installed)
660     return;
661
662   if (jobidx != -1)
663     {
664       how = job->elements[jobidx];
665       switch(how)
666         {
667         case SOLVER_INSTALL_SOLVABLE:
668         case SOLVER_ERASE_SOLVABLE:
669         case SOLVER_ERASE_SOLVABLE_NAME:
670         case SOLVER_ERASE_SOLVABLE_PROVIDES:
671           break;
672         default:
673           return;
674         }
675     }
676   /* go through all enabled job rules */
677   MAPZERO(&solv->noupdate);
678   for (i = solv->jobrules; i < solv->systemrules; i++)
679     {
680       r = solv->rules + i;
681       if (!r->w1)       /* disabled? */
682         continue;
683       j = solv->ruletojob.elements[i - solv->jobrules];
684       if (j == lastjob)
685         continue;
686       lastjob = j;
687       how = job->elements[j];
688       what = job->elements[j + 1];
689       switch(how)
690         {
691         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
692           s = pool->solvables + what;
693           FOR_PROVIDES(p, pp, s->name)
694             {
695               if (pool->solvables[p].name != s->name)
696                 continue;
697               if (pool->solvables[p].repo == installed)
698                 MAPSET(&solv->noupdate, p - installed->start);
699             }
700           break;
701         case SOLVER_ERASE_SOLVABLE:
702           s = pool->solvables + what;
703           if (s->repo == installed)
704             MAPSET(&solv->noupdate, what - installed->start);
705           break;
706         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
707         case SOLVER_ERASE_SOLVABLE_PROVIDES:
708           FOR_PROVIDES(p, pp, what)
709             {
710               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
711                 continue;
712               if (pool->solvables[p].repo == installed)
713                 MAPSET(&solv->noupdate, p - installed->start);
714             }
715           break;
716         default:
717           break;
718         }
719     }
720
721   /* fixup update rule status */
722   if (solv->allowuninstall)
723     return;             /* no update rules at all */
724
725   if (jobidx != -1)
726     {
727       /* we just disabled job #jobidx. enable all update rules
728        * that aren't disabled by the remaining job rules */
729       how = job->elements[jobidx];
730       what = job->elements[jobidx + 1];
731       switch(how)
732         {
733         case SOLVER_INSTALL_SOLVABLE:
734           s = pool->solvables + what;
735           FOR_PROVIDES(p, pp, s->name)
736             {
737               if (pool->solvables[p].name != s->name)
738                 continue;
739               if (pool->solvables[p].repo != installed)
740                 continue;
741               if (MAPTST(&solv->noupdate, p - installed->start))
742                 continue;
743               r = solv->rules + solv->systemrules + (p - installed->start);
744               if (r->w1)
745                 continue;
746               enablerule(solv, r);
747               if (pool->verbose)
748                 {
749                   printf("@@@ re-enabling ");
750                   printrule(solv, r);
751                 }
752             }
753           break;
754         case SOLVER_ERASE_SOLVABLE:
755           s = pool->solvables + what;
756           if (s->repo != installed)
757             break;
758           if (MAPTST(&solv->noupdate, what - installed->start))
759             break;
760           r = solv->rules + solv->systemrules + (what - installed->start);
761           if (r->w1)
762             break;
763           enablerule(solv, r);
764           if (pool->verbose)
765             {
766               printf("@@@ re-enabling ");
767               printrule(solv, r);
768             }
769           break;
770         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
771         case SOLVER_ERASE_SOLVABLE_PROVIDES:
772           FOR_PROVIDES(p, pp, what)
773             {
774               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
775                 continue;
776               if (pool->solvables[p].repo != installed)
777                 continue;
778               if (MAPTST(&solv->noupdate, p - installed->start))
779                 continue;
780               r = solv->rules + solv->systemrules + (p - installed->start);
781               if (r->w1)
782                 continue;
783               enablerule(solv, r);
784               if (pool->verbose)
785                 {
786                   printf("@@@ re-enabling ");
787                   printrule(solv, r);
788                 }
789             }
790           break;
791         default:
792           break;
793         }
794       return;
795     }
796
797   for (i = 0; i < installed->nsolvables; i++)
798     {
799       r = solv->rules + solv->systemrules + i;
800       if (r->w1 && MAPTST(&solv->noupdate, i))
801         r->w1 = 0;              /* was enabled, need to disable */
802     }
803 }
804
805
806 /*
807  * add (install) rules for solvable
808  * for unfulfilled requirements, conflicts, obsoletes,....
809  * "unflag" a resolvable if it is not installable via "addrule(solv, -n, 0)"
810  */
811
812 static void
813 addrpmrulesforsolvable(Solver *solv, Solvable *s, Map *m)
814 {
815   Pool *pool = solv->pool;
816   Repo *installed = solv->installed;
817   Queue q;
818   Id qbuf[64];
819   int i;
820   int dontfix;
821   Id req, *reqp;
822   Id con, *conp;
823   Id obs, *obsp;
824   Id rec, *recp;
825   Id sug, *sugp;
826   Id p, *pp;
827   Id *dp;
828   Id n;
829
830   if (solv->pool->verbose > 3)
831     printf ("----- addrpmrulesforsolvable -----\n");
832   
833   queue_init_buffer(&q, qbuf, sizeof(qbuf)/sizeof(*qbuf));
834   queue_push(&q, s - pool->solvables);  /* push solvable Id */
835
836   while (q.count)
837     {
838       /*
839        * n: Id of solvable
840        * s: Pointer to solvable
841        */
842       
843       n = queue_shift(&q);
844       if (MAPTST(m, n))                /* continue if already done */
845         continue;
846
847       MAPSET(m, n);
848       s = pool->solvables + n;         /* s = Solvable in question */
849
850       dontfix = 0;
851       if (installed                     /* Installed system available */
852           && !solv->fixsystem           /* NOT repair errors in rpm dependency graph */
853           && s->repo == installed)      /* solvable is installed? */
854       {
855         dontfix = 1;                   /* dont care about broken rpm deps */
856       }
857
858       /*-----------------------------------------
859        * check requires of s
860        */
861       
862       if (s->requires)
863         {
864           reqp = s->repo->idarraydata + s->requires;
865           while ((req = *reqp++) != 0) /* go throw all requires */
866             {
867               if (req == SOLVABLE_PREREQMARKER)   /* skip the marker */
868                 continue;
869
870               dp = GET_PROVIDESP(req, p);       /* get providers of req; p is a dummy only */ 
871
872               if (*dp == SYSTEMSOLVABLE)        /* always installed */
873                 continue;
874
875               if (dontfix)
876                 {
877                   /* the strategy here is to not insist on dependencies
878                    * that are already broken. so if we find one provider
879                    * that was already installed, we know that the
880                    * dependency was not broken before so we enforce it */
881                   for (i = 0; (p = dp[i]) != 0; i++)    /* for all providers */
882                     {
883                       if (pool->solvables[p].repo == installed)
884                         break;          /* provider was installed */
885                     }
886                   if (!p)               /* previously broken dependency */
887                     {
888                       if (pool->verbose)
889                         printf("ignoring broken requires %s of installed package %s-%s.%s\n", dep2str(pool, req), id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
890                       continue;
891                     }
892                 }
893
894               if (!*dp)
895                 {
896                   /* nothing provides req! */
897                   if (pool->verbose)
898                      printf("package %s-%s.%s [%d] is not installable (%s)\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), (Id)(s - pool->solvables), dep2str(pool, req));
899                   addrule(solv, -n, 0); /* mark requestor as uninstallable */
900                   if (solv->rc_output)
901                     printf(">!> !unflag %s-%s.%s[%s]\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), repo_name(s->repo));
902                   continue;
903                 }
904
905               if (pool->verbose > 2)
906                 {
907                   printf("  %s-%s.%s requires %s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, req));
908                   for (i = 0; dp[i]; i++)
909                     printf("   provided by %s-%s.%s\n", id2str(pool, pool->solvables[dp[i]].name), id2str(pool, pool->solvables[dp[i]].evr), id2str(pool, pool->solvables[dp[i]].arch));
910                 }
911
912               /* add 'requires' dependency */
913               /* rule: (-requestor|provider1|provider2|...|providerN) */
914               addrule(solv, -n, dp - pool->whatprovidesdata);
915
916               /* descend the dependency tree */
917               for (; *dp; dp++)   /* loop through all providers */
918                 {
919                   if (!MAPTST(m, *dp))
920                     queue_push(&q, *dp);
921                 }
922
923             } /* while, requirements of n */
924
925         } /* if, requirements */
926
927       
928       /*-----------------------------------------
929        * check conflicts of s
930        */
931       
932       if (s->conflicts)
933         {
934           conp = s->repo->idarraydata + s->conflicts;
935           while ((con = *conp++) != 0)
936             {
937               FOR_PROVIDES(p, pp, con)
938                 {
939                    /* dontfix: dont care about conflicts with already installed packs */
940                   if (dontfix && pool->solvables[p].repo == installed)
941                     continue;
942                  /* rule: -n|-p: either solvable _or_ provider of conflict */
943                   addrule(solv, -n, -p);
944                 }
945             }
946         }
947
948       /*-----------------------------------------
949        * check obsoletes if not installed
950        */
951       if (!installed || pool->solvables[n].repo != installed)
952         {                              /* not installed */
953           if (s->obsoletes)
954             {
955               obsp = s->repo->idarraydata + s->obsoletes;
956               while ((obs = *obsp++) != 0)
957                 {
958                   FOR_PROVIDES(p, pp, obs)
959                     addrule(solv, -n, -p);
960                 }
961             }
962           FOR_PROVIDES(p, pp, s->name)
963             {
964               if (s->name == pool->solvables[p].name)
965                 addrule(solv, -n, -p);
966             }
967         }
968
969       /*-----------------------------------------
970        * add recommends to the rule list
971        */
972       if (s->recommends)
973         {
974           recp = s->repo->idarraydata + s->recommends;
975           while ((rec = *recp++) != 0)
976             {
977               FOR_PROVIDES(p, pp, rec)
978                 if (!MAPTST(m, p))
979                   queue_push(&q, p);
980             }
981         }
982       if (s->suggests)
983         {
984           sugp = s->repo->idarraydata + s->suggests;
985           while ((sug = *sugp++) != 0)
986             {
987               FOR_PROVIDES(p, pp, sug)
988                 if (!MAPTST(m, p))
989                   queue_push(&q, p);
990             }
991         }
992     }
993   queue_free(&q);
994 }
995
996 static void
997 addrpmrulesforweak(Solver *solv, Map *m)
998 {
999   Pool *pool = solv->pool;
1000   Solvable *s;
1001   Id sup, *supp;
1002   int i, n;
1003
1004   if (pool->verbose) printf("----- addrpmrulesforweak ----- (nrules %d)\n", solv->nrules);
1005   for (i = n = 1; n < pool->nsolvables; i++, n++)
1006     {
1007       if (i == pool->nsolvables)
1008         i = 1;
1009       if (MAPTST(m, i))
1010         continue;
1011       s = pool->solvables + i;
1012       if (!pool_installable(pool, s))
1013         continue;
1014       sup = 0;
1015       if (s->supplements)
1016         {
1017           supp = s->repo->idarraydata + s->supplements;
1018           while ((sup = *supp++) != ID_NULL)
1019             if (dep_possible(solv, sup, m))
1020               break;
1021         }
1022       if (!sup && s->freshens)
1023         {
1024           supp = s->repo->idarraydata + s->freshens;
1025           while ((sup = *supp++) != ID_NULL)
1026             if (dep_possible(solv, sup, m))
1027               break;
1028         }
1029       if (!sup && s->enhances)
1030         {
1031           supp = s->repo->idarraydata + s->enhances;
1032           while ((sup = *supp++) != ID_NULL)
1033             if (dep_possible(solv, sup, m))
1034               break;
1035         }
1036       if (!sup)
1037         continue;
1038       addrpmrulesforsolvable(solv, s, m);
1039       n = 0;
1040     }
1041   if (pool->verbose) printf("----- addrpmrulesforweak ----- done. (nrules%d)\n", solv->nrules);
1042 }
1043
1044 static void
1045 addrpmrulesforupdaters(Solver *solv, Solvable *s, Map *m, int allowall)
1046 {
1047   Pool *pool = solv->pool;
1048   int i;
1049   Queue qs;
1050   Id qsbuf[64];
1051
1052   if (solv->pool->verbose > 3)
1053     printf ("----- addrpmrulesforupdaters -----\n");
1054
1055   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1056   policy_findupdatepackages(solv, s, &qs, allowall);
1057   if (!MAPTST(m, s - pool->solvables))  /* add rule for s if not already done */
1058     addrpmrulesforsolvable(solv, s, m); 
1059   for (i = 0; i < qs.count; i++)
1060     if (!MAPTST(m, qs.elements[i]))
1061       addrpmrulesforsolvable(solv, pool->solvables + qs.elements[i], m);
1062   queue_free(&qs);
1063 }
1064
1065 /*
1066  * add rule for update
1067  *   (A|A1|A2|A3...)  An = update candidates for A
1068  * 
1069  * s = (installed) solvable
1070  */
1071
1072 static void
1073 addupdaterule(Solver *solv, Solvable *s, int allowall)
1074 {
1075   /* installed packages get a special upgrade allowed rule */
1076   Pool *pool = solv->pool;
1077   Id d;
1078   Queue qs;
1079   Id qsbuf[64];
1080
1081   if (solv->pool->verbose > 3)
1082     printf ("-----  addupdaterule -----\n");
1083
1084   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1085   policy_findupdatepackages(solv, s, &qs, allowall);
1086   if (qs.count == 0)                   /* no updaters found */
1087     d = 0;
1088   else
1089     d = pool_queuetowhatprovides(pool, &qs);    /* intern computed queue */
1090   queue_free(&qs);
1091   addrule(solv, s - pool->solvables, d);        /* allow update of s */
1092 }
1093
1094
1095 /*-----------------------------------------------------------------*/
1096 /* watches */
1097
1098
1099 /*
1100  * makewatches
1101  * 
1102  * initial setup for all watches
1103  */
1104
1105 static void
1106 makewatches(Solver *solv)
1107 {
1108   Rule *r;
1109   int i;
1110   int nsolvables = solv->pool->nsolvables;
1111
1112   xfree(solv->watches);
1113                                        /* lower half for removals, upper half for installs */
1114   solv->watches = (Id *)xcalloc(2 * nsolvables, sizeof(Id));
1115 #if 1
1116   /* do it reverse so rpm rules get triggered first */
1117   for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
1118 #else
1119   for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
1120 #endif
1121     {
1122       if (!r->w1                       /* rule is disabled */
1123           || !r->w2)                   /* rule is assertion */
1124         continue;
1125
1126       /* see addwatches(solv, r) */
1127       r->n1 = solv->watches[nsolvables + r->w1];
1128       solv->watches[nsolvables + r->w1] = r - solv->rules;
1129
1130       r->n2 = solv->watches[nsolvables + r->w2];
1131       solv->watches[nsolvables + r->w2] = r - solv->rules;
1132     }
1133 }
1134
1135
1136 /*
1137  * add watches (for rule)
1138  */
1139
1140 static void
1141 addwatches(Solver *solv, Rule *r)
1142 {
1143   int nsolvables = solv->pool->nsolvables;
1144
1145   r->n1 = solv->watches[nsolvables + r->w1];
1146   solv->watches[nsolvables + r->w1] = r - solv->rules;
1147
1148   r->n2 = solv->watches[nsolvables + r->w2];
1149   solv->watches[nsolvables + r->w2] = r - solv->rules;
1150 }
1151
1152
1153 /*-----------------------------------------------------------------*/
1154 /* rule propagation */
1155
1156 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
1157
1158 /*
1159  * propagate
1160  * 
1161  * propagate decision to all rules
1162  */
1163
1164 static Rule *
1165 propagate(Solver *solv, int level)
1166 {
1167   Pool *pool = solv->pool;
1168   Id *rp, *nrp;
1169   Rule *r;
1170   Id p, pkg, ow;
1171   Id *dp;
1172   Id *decisionmap = solv->decisionmap;
1173   Id *watches = solv->watches + pool->nsolvables;
1174
1175   while (solv->propagate_index < solv->decisionq.count)
1176     {
1177       /* negate because our watches trigger if literal goes FALSE */
1178       pkg = -solv->decisionq.elements[solv->propagate_index++];
1179       if (pool->verbose > 3)
1180         {
1181           printf("popagate for decision %d level %d\n", -pkg, level);
1182           printruleelement(solv, 0, -pkg);
1183         }
1184
1185       for (rp = watches + pkg; *rp; rp = nrp)
1186         {
1187           r = solv->rules + *rp;
1188           
1189           if (pool->verbose > 3)
1190             {
1191               printf("  watch triggered ");
1192               printrule(solv, r);
1193             }
1194           
1195           if (pkg == r->w1)
1196             {
1197               ow = r->w2;
1198               nrp = &r->n1;
1199             }
1200           else
1201             {
1202               ow = r->w1;
1203               nrp = &r->n2;
1204             }
1205           /* if clause is TRUE, nothing to do */
1206           if (DECISIONMAP_TRUE(ow))
1207             continue;
1208
1209           if (r->d)
1210             {
1211               /* not a binary clause, check if we need to move our watch */
1212               if (r->p && r->p != ow && !DECISIONMAP_TRUE(-r->p))
1213                 p = r->p;
1214               else
1215                 for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
1216                   if (p != ow && !DECISIONMAP_TRUE(-p))
1217                     break;
1218               if (p)
1219                 {
1220                   /* p is free to watch, move watch to p */
1221                   if (pool->verbose > 3)
1222                     {
1223                       if (p > 0)
1224                         printf("    -> move w%d to %s-%s.%s\n", (pkg == r->w1 ? 1 : 2), id2str(pool, pool->solvables[p].name), id2str(pool, pool->solvables[p].evr), id2str(pool, pool->solvables[p].arch));
1225                       else
1226                         printf("    -> move w%d to !%s-%s.%s\n", (pkg == r->w1 ? 1 : 2), id2str(pool, pool->solvables[-p].name), id2str(pool, pool->solvables[-p].evr), id2str(pool, pool->solvables[-p].arch));
1227                     }
1228                   *rp = *nrp;
1229                   nrp = rp;
1230                   if (pkg == r->w1)
1231                     {
1232                       r->w1 = p;
1233                       r->n1 = watches[p];
1234                     }
1235                   else
1236                     {
1237                       r->w2 = p;
1238                       r->n2 = watches[p];
1239                     }
1240                   watches[p] = r - solv->rules;
1241                   continue;
1242                 }
1243             }
1244           /* unit clause found, set other watch to TRUE */
1245           if (DECISIONMAP_TRUE(-ow))
1246             return r;           /* eek, a conflict! */
1247           if (pool->verbose > 2)
1248             {
1249               printf("unit ");
1250               printrule(solv, r);
1251             }
1252           if (ow > 0)
1253             decisionmap[ow] = level;
1254           else
1255             decisionmap[-ow] = -level;
1256           queue_push(&solv->decisionq, ow);
1257           queue_push(&solv->decisionq_why, r - solv->rules);
1258           if (pool->verbose > 3)
1259             {
1260               Solvable *s = pool->solvables + (ow > 0 ? ow : -ow);
1261               if (ow > 0)
1262                 printf("  -> decided to install %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1263               else
1264                 printf("  -> decided to conflict %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1265             }
1266         }
1267     }
1268   return 0;     /* all is well */
1269 }
1270
1271
1272 /*-----------------------------------------------------------------*/
1273 /* Analysis */
1274
1275 /*
1276  * analyze
1277  *   and learn
1278  */
1279
1280 static int
1281 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *why)
1282 {
1283   Pool *pool = solv->pool;
1284   Queue r;
1285   int rlevel = 1;
1286   Map seen;             /* global? */
1287   Id v, vv, *dp;
1288   int l, i, idx;
1289   int num = 0;
1290   int learnt_why = solv->learnt_pool.count;
1291   Id *decisionmap = solv->decisionmap;
1292  
1293   queue_init(&r);
1294
1295   if (pool->verbose > 1) printf("ANALYZE at %d ----------------------\n", level);
1296   map_init(&seen, pool->nsolvables);
1297   idx = solv->decisionq.count;
1298   for (;;)
1299     {
1300       if (pool->verbose > 1) printrule(solv, c);
1301       queue_push(&solv->learnt_pool, c - solv->rules);
1302       dp = c->d ? pool->whatprovidesdata + c->d : 0;
1303       for (i = -1; ; i++)
1304         {
1305           if (i == -1)
1306             v = c->p;
1307           else if (c->d == 0)
1308             v = i ? 0 : c->w2;
1309           else
1310             v = *dp++;
1311           if (v == 0)
1312             break;
1313           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1314               continue;
1315           vv = v > 0 ? v : -v;
1316           if (MAPTST(&seen, vv))
1317             continue;
1318           l = solv->decisionmap[vv];
1319           if (l < 0)
1320             l = -l;
1321           if (l == 1)
1322             {
1323 #if 0
1324               int j;
1325               for (j = 0; j < solv->decisionq.count; j++)
1326                 if (solv->decisionq.elements[j] == v)
1327                   break;
1328               if (j == solv->decisionq.count)
1329                 abort();
1330               queue_push(&rulq, -(j + 1));
1331 #endif
1332               continue;                 /* initial setting */
1333             }
1334           MAPSET(&seen, vv);
1335           if (l == level)
1336             num++;                      /* need to do this one as well */
1337           else
1338             {
1339               queue_push(&r, v);
1340               if (pool->verbose > 3)
1341                 {
1342                   printf("PUSH %d ", v);
1343                   printruleelement(solv, 0, v);
1344                 }
1345               if (l > rlevel)
1346                 rlevel = l;
1347             }
1348         }
1349       if (pool->verbose > 3)
1350         printf("num = %d\n", num);
1351       if (num <= 0)
1352         abort();
1353       for (;;)
1354         {
1355           v = solv->decisionq.elements[--idx];
1356           vv = v > 0 ? v : -v;
1357           if (MAPTST(&seen, vv))
1358             break;
1359         }
1360       c = solv->rules + solv->decisionq_why.elements[idx];
1361       MAPCLR(&seen, vv);
1362       if (--num == 0)
1363         break;
1364     }
1365   *pr = -v;
1366   if (r.count == 0)
1367     *dr = 0;
1368   else if (r.count == 1 && r.elements[0] < 0)
1369     *dr = r.elements[0];
1370   else
1371     *dr = pool_queuetowhatprovides(pool, &r);
1372   if (pool->verbose > 1)
1373     {
1374       printf("learned rule for level %d (am %d)\n", rlevel, level);
1375       printruleelement(solv, 0, -v);
1376       for (i = 0; i < r.count; i++)
1377         {
1378           v = r.elements[i];
1379           printruleelement(solv, 0, v);
1380         }
1381     }
1382   map_free(&seen);
1383   queue_push(&solv->learnt_pool, 0);
1384   if (pool->verbose > 3)
1385     {
1386       for (i = learnt_why; solv->learnt_pool.elements[i]; i++)
1387         {
1388           printf("learnt_why ");
1389           printrule(solv, solv->rules + solv->learnt_pool.elements[i]);
1390         }
1391     }
1392   if (why)
1393     *why = learnt_why;
1394   return rlevel;
1395 }
1396
1397
1398 /*
1399  * reset_solver
1400  * reset the solver decisions to right after the rpm rules.
1401  * called after rules have been enabled/disabled
1402  */
1403
1404 static void
1405 reset_solver(Solver *solv)
1406 {
1407   int i;
1408   Id v;
1409
1410   /* delete all learnt rules */
1411   solv->nrules = solv->learntrules;
1412   queue_empty(&solv->learnt_why);
1413   queue_empty(&solv->learnt_pool);
1414
1415   /* redo all direct rpm rule decisions */
1416   /* we break at the first decision with a why attached, this is
1417    * either a job/system rule assertion or a propagated decision */
1418   for (i = 0; i < solv->decisionq.count; i++)
1419     {
1420       v = solv->decisionq.elements[i];
1421       solv->decisionmap[v > 0 ? v : -v] = 0;
1422     }
1423   for (i = 0; i < solv->decisionq_why.count; i++)
1424     if (solv->decisionq_why.elements[i])
1425       break;
1426     else
1427       {
1428         v = solv->decisionq.elements[i];
1429         solv->decisionmap[v > 0 ? v : -v] = v > 0 ? 1 : -1;
1430       }
1431
1432   if (solv->pool->verbose > 1)
1433     printf("decisions done reduced from %d to %d\n", solv->decisionq.count, i);
1434
1435   solv->decisionq_why.count = i;
1436   solv->decisionq.count = i;
1437   solv->recommends_index = -1;
1438   solv->propagate_index = 0;
1439
1440   /* redo all job/system decisions */
1441   makeruledecisions(solv);
1442   if (solv->pool->verbose > 1)
1443     printf("decisions after adding job and system rules: %d\n", solv->decisionq.count);
1444   /* recreate watches */
1445   makewatches(solv);
1446 }
1447
1448
1449 /*
1450  * analyze_unsolvable_rule
1451  */
1452
1453 static void
1454 analyze_unsolvable_rule(Solver *solv, Rule *r)
1455 {
1456   int i;
1457   Id why = r - solv->rules;
1458   if (solv->pool->verbose > 1)
1459     {
1460       if (why >= solv->jobrules && why < solv->systemrules)
1461         printf("JOB ");
1462       if (why >= solv->systemrules && why < solv->weakrules)
1463         printf("SYSTEM %d ", why - solv->systemrules);
1464       if (why >= solv->weakrules && why < solv->learntrules)
1465         printf("WEAK ");
1466       if (solv->learntrules && why >= solv->learntrules)
1467         printf("LEARNED ");
1468       printrule(solv, r);
1469     }
1470   if (solv->learntrules && why >= solv->learntrules)
1471     {
1472       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1473         analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i]);
1474       return;
1475     }
1476   /* do not add rpm rules to problem */
1477   if (why < solv->jobrules)
1478     return;
1479   /* turn rule into problem */
1480   if (why >= solv->jobrules && why < solv->systemrules)
1481     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
1482   /* return if problem already countains our rule */
1483   if (solv->problems.count)
1484     {
1485       for (i = solv->problems.count - 1; i >= 0; i--)
1486         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
1487           break;
1488         else if (solv->problems.elements[i] == why)
1489           return;
1490     }
1491   queue_push(&solv->problems, why);
1492 }
1493
1494
1495 /*
1496  * analyze_unsolvable
1497  *
1498  * return: 1 - disabled some rules, try again
1499  *         0 - hopeless
1500  */
1501
1502 static int
1503 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
1504 {
1505   Pool *pool = solv->pool;
1506   Rule *r;
1507   Map seen;             /* global to speed things up? */
1508   Id v, vv, *dp, why;
1509   int l, i, idx;
1510   Id *decisionmap = solv->decisionmap;
1511   int oldproblemcount;
1512   int lastweak;
1513
1514   if (pool->verbose > 1)
1515     printf("ANALYZE UNSOLVABLE ----------------------\n");
1516   oldproblemcount = solv->problems.count;
1517
1518   /* make room for conflicting rule */
1519   queue_push(&solv->problems, 0);
1520   queue_push(&solv->problems, 0);
1521
1522   r = cr;
1523   map_init(&seen, pool->nsolvables);
1524   analyze_unsolvable_rule(solv, r);
1525   dp = r->d ? pool->whatprovidesdata + r->d : 0;
1526   for (i = -1; ; i++)
1527     {
1528       if (i == -1)
1529         v = r->p;
1530       else if (r->d == 0)
1531         v = i ? 0 : r->w2;
1532       else
1533         v = *dp++;
1534       if (v == 0)
1535         break;
1536       if (DECISIONMAP_TRUE(v))  /* the one true literal */
1537           continue;
1538       vv = v > 0 ? v : -v;
1539       l = solv->decisionmap[vv];
1540       if (l < 0)
1541         l = -l;
1542       MAPSET(&seen, vv);
1543     }
1544   idx = solv->decisionq.count;
1545   while (idx > 0)
1546     {
1547       v = solv->decisionq.elements[--idx];
1548       vv = v > 0 ? v : -v;
1549       if (!MAPTST(&seen, vv))
1550         continue;
1551       why = solv->decisionq_why.elements[idx];
1552       if (!why)
1553         {
1554           if (pool->verbose > 3)
1555             {
1556               printf("RPM ");
1557               printruleelement(solv, 0, v);
1558             }
1559           continue;
1560         }
1561       r = solv->rules + why;
1562       analyze_unsolvable_rule(solv, r);
1563       dp = r->d ? pool->whatprovidesdata + r->d : 0;
1564       for (i = -1; ; i++)
1565         {
1566           if (i == -1)
1567             v = r->p;
1568           else if (r->d == 0)
1569             v = i ? 0 : r->w2;
1570           else
1571             v = *dp++;
1572           if (v == 0)
1573             break;
1574           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1575               continue;
1576           vv = v > 0 ? v : -v;
1577           l = solv->decisionmap[vv];
1578           if (l < 0)
1579             l = -l;
1580           MAPSET(&seen, vv);
1581         }
1582     }
1583   map_free(&seen);
1584   queue_push(&solv->problems, 0);       /* mark end of this problem */
1585
1586   lastweak = 0;
1587   if (solv->weakrules != solv->learntrules)
1588     {
1589       for (i = oldproblemcount + 2; i < solv->problems.count - 1; i++)
1590         {
1591           why = solv->problems.elements[i];
1592           if (why < solv->weakrules || why >= solv->learntrules)
1593             continue;
1594           if (!lastweak || lastweak < why)
1595             lastweak = why;
1596         }
1597     }
1598   if (lastweak)
1599     {
1600       /* disable last weak rule */
1601       solv->problems.count = oldproblemcount;
1602       r = solv->rules + lastweak;
1603       printf("disabling weak ");
1604       printrule(solv, r);
1605       r->w1 = 0;
1606       reset_solver(solv);
1607       return 1;
1608     }
1609
1610   /* patch conflicting rule data */
1611   if (cr - solv->rules >= solv->learntrules)
1612     {
1613       /* we have to store the rule internals for learnt rules
1614        * as they get freed for every solver run */
1615       solv->problems.elements[oldproblemcount] = cr->p;
1616       solv->problems.elements[oldproblemcount + 1] = cr->d;
1617     }
1618   else
1619     solv->problems.elements[oldproblemcount + 1] = cr - solv->rules;
1620
1621   if (disablerules)
1622     {
1623       for (i = oldproblemcount + 2; i < solv->problems.count - 1; i++)
1624         disableproblem(solv, solv->problems.elements[i]);
1625       reset_solver(solv);
1626       return 1;
1627     }
1628   if (pool->verbose)
1629     printf("UNSOLVABLE\n");
1630   return 0;
1631 }
1632
1633
1634 /*-----------------------------------------------------------------*/
1635 /* Decision revert */
1636
1637 /*
1638  * revert
1639  * revert decision at level
1640  */
1641
1642 static void
1643 revert(Solver *solv, int level)
1644 {
1645   Id v, vv;
1646   while (solv->decisionq.count)
1647     {
1648       v = solv->decisionq.elements[solv->decisionq.count - 1];
1649       vv = v > 0 ? v : -v;
1650       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1651         break;
1652       if (solv->pool->verbose > 3)
1653         printf("reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1654       solv->decisionmap[vv] = 0;
1655       solv->decisionq.count--;
1656       solv->decisionq_why.count--;
1657       solv->propagate_index = solv->decisionq.count;
1658     }
1659   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
1660     {
1661       solv->branches.count--;
1662       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
1663         solv->branches.count--;
1664     }
1665   solv->recommends_index = -1;
1666 }
1667
1668
1669 /*
1670  * watch2onhighest - put watch2 on literal with highest level
1671  */
1672
1673 static inline void
1674 watch2onhighest(Solver *solv, Rule *r)
1675 {
1676   int l, wl = 0;
1677   Id v, *dp;
1678
1679   if (!r->d)
1680     return;     /* binary rule, both watches are set */
1681   dp = solv->pool->whatprovidesdata + r->d;
1682   while ((v = *dp++) != 0)
1683     {
1684       l = solv->decisionmap[v < 0 ? -v : v];
1685       if (l < 0)
1686         l = -l;
1687       if (l > wl)
1688         {
1689           r->w2 = dp[-1];
1690           wl = l;
1691         }
1692     }
1693 }
1694
1695
1696 /*
1697  * setpropagatelearn
1698  *
1699  * add free decision to decision q, increase level
1700  * propagate decision, return if no conflict.
1701  * in conflict case, analyze conflict rule, add resulting
1702  * rule to learnt rule set, make decision from learnt
1703  * rule (always unit) and re-propagate.
1704  */
1705
1706 static int
1707 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
1708 {
1709   Rule *r;
1710   Id p, d;
1711   int l, why;
1712
1713   if (decision)
1714     {
1715       level++;
1716       if (decision > 0)
1717         solv->decisionmap[decision] = level;
1718       else
1719         solv->decisionmap[-decision] = -level;
1720       queue_push(&solv->decisionq, decision);
1721       queue_push(&solv->decisionq_why, 0);
1722     }
1723   for (;;)
1724     {
1725       r = propagate(solv, level);
1726       if (!r)
1727         break;
1728       if (level == 1)
1729         return analyze_unsolvable(solv, r, disablerules);
1730       printf("conflict with rule #%d\n", (int)(r - solv->rules));
1731       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
1732       if (l >= level || l <= 0)
1733         abort();
1734       printf("reverting decisions (level %d -> %d)\n", level, l);
1735       level = l;
1736       revert(solv, level);
1737       r = addrule(solv, p, d);       /* p requires d */
1738       if (!r)
1739         abort();
1740       if (solv->learnt_why.count != (r - solv->rules) - solv->learntrules)
1741         {
1742           printf("%d %d\n", solv->learnt_why.count, (int)(r - solv->rules) - solv->learntrules);
1743           abort();
1744         }
1745       queue_push(&solv->learnt_why, why);
1746       if (d)
1747         {
1748           /* at least 2 literals, needs watches */
1749           watch2onhighest(solv, r);
1750           addwatches(solv, r);
1751         }
1752       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
1753       queue_push(&solv->decisionq, p);
1754       queue_push(&solv->decisionq_why, r - solv->rules);
1755       if (solv->pool->verbose > 1)
1756         {
1757           printf("decision: ");
1758           printruleelement(solv, 0, p);
1759           printf("new rule: ");
1760           printrule(solv, r);
1761         }
1762     }
1763   return level;
1764 }
1765
1766
1767 /*
1768  * install best package from the queue. We add an extra package, inst, if
1769  * provided. See comment in weak install section.
1770  */
1771 static int
1772 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
1773 {
1774   Pool *pool = solv->pool;
1775   Id p;
1776   int i;
1777
1778   if (dq->count > 1 || inst)
1779     policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
1780
1781   i = 0;
1782   if (dq->count > 1)
1783     {
1784       /* choose the supplemented one */
1785       for (i = 0; i < dq->count; i++)
1786         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
1787           break;
1788       if (i == dq->count)
1789         {
1790           for (i = 1; i < dq->count; i++)
1791             queue_push(&solv->branches, dq->elements[i]);
1792           queue_push(&solv->branches, -level);
1793           i = 0;
1794         }
1795     }
1796   p = dq->elements[i];
1797
1798   if (pool->verbose > 3)
1799     {
1800       Solvable *s = pool->solvables + p;
1801       printf("installing %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1802     }
1803
1804   return setpropagatelearn(solv, level, p, disablerules);
1805 }
1806
1807
1808 /*-----------------------------------------------------------------*/
1809 /* Main solver interface */
1810
1811
1812 /*
1813  * solver_create
1814  * create solver structure
1815  *
1816  * pool: all available solvables
1817  * installed: installed Solvables
1818  *
1819  *
1820  * Upon solving, rules are created to flag the Solvables
1821  * of the 'installed' Repo as installed.
1822  */
1823
1824 Solver *
1825 solver_create(Pool *pool, Repo *installed)
1826 {
1827   Solver *solv;
1828   solv = (Solver *)xcalloc(1, sizeof(Solver));
1829   solv->pool = pool;
1830   solv->installed = installed;
1831
1832   queue_init(&solv->ruletojob);
1833   queue_init(&solv->decisionq);
1834   queue_init(&solv->decisionq_why);
1835   queue_init(&solv->problems);
1836   queue_init(&solv->suggestions);
1837   queue_init(&solv->learnt_why);
1838   queue_init(&solv->learnt_pool);
1839   queue_init(&solv->branches);
1840
1841   map_init(&solv->recommendsmap, pool->nsolvables);
1842   map_init(&solv->suggestsmap, pool->nsolvables);
1843   map_init(&solv->noupdate, installed ? installed->end - installed->start : 0);
1844   solv->recommends_index = 0;
1845
1846   solv->decisionmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
1847   solv->rules = (Rule *)xmalloc((solv->nrules + (RULES_BLOCK + 1)) * sizeof(Rule));
1848   memset(solv->rules, 0, sizeof(Rule));
1849   solv->nrules = 1;
1850
1851   return solv;
1852 }
1853
1854
1855 /*
1856  * solver_free
1857  */
1858
1859 void
1860 solver_free(Solver *solv)
1861 {
1862   queue_free(&solv->ruletojob);
1863   queue_free(&solv->decisionq);
1864   queue_free(&solv->decisionq_why);
1865   queue_free(&solv->learnt_why);
1866   queue_free(&solv->learnt_pool);
1867   queue_free(&solv->problems);
1868   queue_free(&solv->suggestions);
1869   queue_free(&solv->branches);
1870
1871   map_free(&solv->recommendsmap);
1872   map_free(&solv->suggestsmap);
1873   map_free(&solv->noupdate);
1874   xfree(solv->decisionmap);
1875   xfree(solv->rules);
1876   xfree(solv->watches);
1877   xfree(solv->weaksystemrules);
1878   xfree(solv->obsoletes);
1879   xfree(solv->obsoletes_data);
1880   xfree(solv);
1881 }
1882
1883
1884 /*-------------------------------------------------------*/
1885
1886 /*
1887  * run_solver
1888  * 
1889  * all rules have been set up, now actually run the solver
1890  *
1891  */
1892
1893 static void
1894 run_solver(Solver *solv, int disablerules, int doweak)
1895 {
1896   Queue dq;
1897   int systemlevel;
1898   int level, olevel;
1899   Rule *r;
1900   int i, j, n;
1901   Solvable *s;
1902   Pool *pool = solv->pool;
1903   Id p, *dp;
1904
1905   if (pool->verbose > 3)
1906     {
1907       printf("number of rules: %d\n", solv->nrules);
1908       for (i = 0; i < solv->nrules; i++)
1909         printrule(solv, solv->rules + i);
1910     }
1911
1912   /* all new rules are learnt after this point */
1913   solv->learntrules = solv->nrules;
1914   /* crate watches lists */
1915   makewatches(solv);
1916
1917   if (pool->verbose) printf("initial decisions: %d\n", solv->decisionq.count);
1918
1919   /* start SAT algorithm */
1920   level = 1;
1921   systemlevel = level + 1;
1922   if (pool->verbose) printf("solving...\n");
1923
1924   queue_init(&dq);
1925   for (;;)
1926     {
1927       /*
1928        * propagate
1929        */
1930       
1931       if (level == 1)
1932         {
1933           if (pool->verbose) printf("propagating (%d %d)...\n", solv->propagate_index, solv->decisionq.count);
1934           if ((r = propagate(solv, level)) != 0)
1935             {
1936               if (analyze_unsolvable(solv, r, disablerules))
1937                 continue;
1938               queue_free(&dq);
1939               return;
1940             }
1941         }
1942
1943       /*
1944        * installed packages
1945        */
1946       
1947       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
1948         {
1949           if (!solv->updatesystem)
1950             {
1951               /* try to keep as many packages as possible */
1952               if (pool->verbose) printf("installing system packages\n");
1953               for (i = solv->installed->start, n = 0; ; i++)
1954                 {
1955                   if (n == solv->installed->nsolvables)
1956                     break;
1957                   if (i == solv->installed->end)
1958                     i = solv->installed->start;
1959                   s = pool->solvables + i;
1960                   if (s->repo != solv->installed)
1961                     continue;
1962                   n++;
1963                   if (solv->decisionmap[i] != 0)
1964                     continue;
1965                   if (pool->verbose > 3)
1966                     printf("keeping %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1967                   olevel = level;
1968                   level = setpropagatelearn(solv, level, i, disablerules);
1969                   if (level == 0)
1970                     {
1971                       queue_free(&dq);
1972                       return;
1973                     }
1974                   if (level <= olevel)
1975                     n = 0;
1976                 }
1977             }
1978           if (solv->weaksystemrules)
1979             {
1980               if (pool->verbose) printf("installing weak system packages\n");
1981               for (i = solv->installed->start; i < solv->installed->end; i++)
1982                 {
1983                   if (pool->solvables[i].repo != solv->installed)
1984                     continue;
1985                   if (solv->decisionmap[i] > 0 || (solv->decisionmap[i] < 0 && solv->weaksystemrules[i - solv->installed->start] == 0))
1986                     continue;
1987                   /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
1988                   if (MAPTST(&solv->noupdate, i - solv->installed->start))
1989                     continue;
1990                   queue_empty(&dq);
1991                   if (solv->weaksystemrules[i - solv->installed->start])
1992                     {
1993                       dp = pool->whatprovidesdata + solv->weaksystemrules[i - solv->installed->start];
1994                       while ((p = *dp++) != 0)
1995                         {
1996                           if (solv->decisionmap[p] > 0)
1997                             break;
1998                           if (solv->decisionmap[p] == 0)
1999                             queue_push(&dq, p);
2000                         }
2001                       if (p)
2002                         continue;       /* update package already installed */
2003                     }
2004                   if (!dq.count && solv->decisionmap[i] != 0)
2005                     continue;
2006                   olevel = level;
2007                   /* FIXME: i is handled a bit different because we do not want
2008                    * to have it pruned just because it is not recommened.
2009                    * we should not prune installed packages instead */
2010                   level = selectandinstall(solv, level, &dq, (solv->decisionmap[i] ? 0 : i), disablerules);
2011                   if (level == 0)
2012                     {
2013                       queue_free(&dq);
2014                       return;
2015                     }
2016                   if (level <= olevel)
2017                     break;
2018                 }
2019               if (i < solv->installed->end)
2020                 continue;
2021             }
2022           systemlevel = level;
2023         }
2024
2025       /*
2026        * decide
2027        */
2028       
2029       if (pool->verbose) printf("deciding unresolved rules\n");
2030       for (i = 1, n = 1; ; i++, n++)
2031         {
2032           if (n == solv->nrules)
2033             break;
2034           if (i == solv->nrules)
2035             i = 1;
2036           r = solv->rules + i;
2037           if (!r->w1)
2038             continue;
2039           queue_empty(&dq);
2040           if (r->d == 0)
2041             {
2042               /* binary or unary rule */
2043               /* need two positive undecided literals */
2044               if (r->p < 0 || r->w2 <= 0)
2045                 continue;
2046               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2047                 continue;
2048               queue_push(&dq, r->p);
2049               queue_push(&dq, r->w2);
2050             }
2051           else
2052             {
2053               /* make sure that
2054                * all negative literals are installed
2055                * no positive literal is installed
2056                * i.e. the rule is not fulfilled and we
2057                * just need to decide on the positive literals
2058                */
2059               if (r->p < 0)
2060                 {
2061                   if (solv->decisionmap[-r->p] <= 0)
2062                     continue;
2063                 }
2064               else
2065                 {
2066                   if (solv->decisionmap[r->p] > 0)
2067                     continue;
2068                   if (solv->decisionmap[r->p] == 0)
2069                     queue_push(&dq, r->p);
2070                 }
2071               dp = pool->whatprovidesdata + r->d;
2072               while ((p = *dp++) != 0)
2073                 {
2074                   if (p < 0)
2075                     {
2076                       if (solv->decisionmap[-p] <= 0)
2077                         break;
2078                     }
2079                   else
2080                     {
2081                       if (solv->decisionmap[p] > 0)
2082                         break;
2083                       if (solv->decisionmap[p] == 0)
2084                         queue_push(&dq, p);
2085                     }
2086                 }
2087               if (p)
2088                 continue;
2089             }
2090           if (dq.count < 2)
2091             {
2092               /* cannot happen as this means that
2093                * the rule is unit */
2094               printrule(solv, r);
2095               abort();
2096             }
2097           if (pool->verbose > 2)
2098             printrule(solv, r);
2099
2100           olevel = level;
2101           level = selectandinstall(solv, level, &dq, 0, disablerules);
2102           if (level == 0)
2103             {
2104               queue_free(&dq);
2105               return;
2106             }
2107           if (level < systemlevel)
2108             break;
2109           n = 0;
2110         } /* for(), decide */
2111
2112       if (n != solv->nrules)    /* continue if level < systemlevel */
2113         continue;
2114       
2115       if (doweak && !solv->problems.count)
2116         {
2117           int qcount;
2118
2119           if (pool->verbose) printf("installing recommended packages\n");
2120           queue_empty(&dq);
2121           for (i = 1; i < pool->nsolvables; i++)
2122             {
2123               if (solv->decisionmap[i] < 0)
2124                 continue;
2125               if (solv->decisionmap[i] > 0)
2126                 {
2127                   Id *recp, rec, *pp, p;
2128                   s = pool->solvables + i;
2129                   /* installed, check for recommends */
2130                   /* XXX need to special case AND ? */
2131                   if (s->recommends)
2132                     {
2133                       recp = s->repo->idarraydata + s->recommends;
2134                       while ((rec = *recp++) != 0)
2135                         {
2136                           qcount = dq.count;
2137                           FOR_PROVIDES(p, pp, rec)
2138                             {
2139                               if (solv->decisionmap[p] > 0)
2140                                 {
2141                                   dq.count = qcount;
2142                                   break;
2143                                 }
2144                               else if (solv->decisionmap[p] == 0)
2145                                 {
2146                                   queue_pushunique(&dq, p);
2147                                 }
2148                             }
2149                         }
2150                     }
2151                 }
2152               else
2153                 {
2154                   s = pool->solvables + i;
2155                   if (!s->supplements && !s->freshens)
2156                     continue;
2157                   if (!pool_installable(pool, s))
2158                     continue;
2159                   if (solver_is_supplementing(solv, s))
2160                     queue_pushunique(&dq, i);
2161                 }
2162             }
2163           if (dq.count)
2164             {
2165               if (dq.count > 1)
2166                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2167               p = dq.elements[0];
2168               s = pool->solvables + p;
2169               if (pool->verbose > 0)
2170                 printf("installing recommended %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2171               level = setpropagatelearn(solv, level, p, 0);
2172               continue;
2173             }
2174         }
2175
2176      if (solv->solution_callback)
2177         {
2178           solv->solution_callback(solv, solv->solution_callback_data);
2179           if (solv->branches.count)
2180             {
2181               int i = solv->branches.count - 1;
2182               int l = -solv->branches.elements[i];
2183               for (; i > 0; i--)
2184                 if (solv->branches.elements[i - 1] < 0)
2185                   break;
2186               p = solv->branches.elements[i];
2187               if (pool->verbose > 0)
2188                 {
2189                   s = pool->solvables + p;
2190                   printf("branching with %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2191                 }
2192               queue_empty(&dq);
2193               for (j = i + 1; j < solv->branches.count; j++)
2194                 queue_push(&dq, solv->branches.elements[j]);
2195               solv->branches.count = i;
2196               level = l;
2197               revert(solv, level);
2198               if (dq.count > 1)
2199                 for (j = 0; j < dq.count; j++)
2200                   queue_push(&solv->branches, dq.elements[j]);
2201               olevel = level;
2202               level = setpropagatelearn(solv, level, p, disablerules);
2203               if (level == 0)
2204                 {
2205                   queue_free(&dq);
2206                   return;
2207                 }
2208               continue;
2209             }
2210           /* all branches done, we're finally finished */
2211           break;
2212         }
2213
2214       /* minimization step */
2215      if (solv->branches.count)
2216         {
2217           int l = 0, lasti = -1, lastl = -1;
2218           p = 0;
2219           for (i = solv->branches.count - 1; i >= 0; i--)
2220             {
2221               p = solv->branches.elements[i];
2222               if (p < 0)
2223                 l = -p;
2224               else if (p > 0 && solv->decisionmap[p] > l + 1)
2225                 {
2226                   lasti = i;
2227                   lastl = l;
2228                 }
2229             }
2230           if (lasti >= 0)
2231             {
2232               /* kill old solvable so that we do not loop */
2233               p = solv->branches.elements[lasti];
2234               solv->branches.elements[lasti] = 0;
2235               s = pool->solvables + p;
2236               if (pool->verbose > 0)
2237                 printf("minimizing %d -> %d with %s-%s.%s\n", solv->decisionmap[p], l, id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2238
2239               level = lastl;
2240               revert(solv, level);
2241               olevel = level;
2242               level = setpropagatelearn(solv, level, p, disablerules);
2243               if (level == 0)
2244                 {
2245                   queue_free(&dq);
2246                   return;
2247                 }
2248               continue;
2249             }
2250         }
2251       break;
2252     }
2253   queue_free(&dq);
2254 }
2255
2256   
2257 /*
2258  * refine_suggestion
2259  * at this point, all rules that led to conflicts are disabled.
2260  * we re-enable all rules of a problem set but rule "sug", then
2261  * continue to disable more rules until there as again a solution.
2262  */
2263   
2264 /* FIXME: think about conflicting assertions */
2265
2266 static void
2267 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2268 {
2269   Pool *pool = solv->pool;
2270   Rule *r;
2271   int i, j;
2272   Id v;
2273   Queue disabled;
2274   int disabledcnt;
2275
2276   if (pool->verbose)
2277     {
2278       printf("refine_suggestion start\n");
2279       for (i = 0; problem[i]; i++)
2280         {
2281           if (problem[i] == sug)
2282             printf("=> ");
2283           printproblem(solv, problem[i]);
2284         }
2285     }
2286   queue_init(&disabled);
2287   queue_empty(refined);
2288   queue_push(refined, sug);
2289
2290   /* re-enable all problem rules with the exception of "sug" */
2291   revert(solv, 1);
2292   reset_solver(solv);
2293
2294   for (i = 0; problem[i]; i++)
2295     if (problem[i] != sug)
2296       enableproblem(solv, problem[i]);
2297
2298   if (sug < 0)
2299     disableupdaterules(solv, job, -(sug + 1));
2300
2301   for (;;)
2302     {
2303       /* re-enable as many weak rules as possible */
2304       for (i = solv->weakrules; i < solv->learntrules; i++)
2305         {
2306           r = solv->rules + i;
2307           if (!r->w1)
2308             enablerule(solv, r);
2309         }
2310
2311       queue_empty(&solv->problems);
2312       revert(solv, 1);          /* XXX move to reset_solver? */
2313       reset_solver(solv);
2314       run_solver(solv, 0, 0);
2315       if (!solv->problems.count)
2316         {
2317           if (pool->verbose)
2318             printf("no more problems!\n");
2319           if (pool->verbose > 3)
2320             printdecisions(solv);
2321           break;                /* great, no more problems */
2322         }
2323       disabledcnt = disabled.count;
2324       /* skip over problem rule */
2325       for (i = 2; i < solv->problems.count - 1; i++)
2326         {
2327           /* ignore solutions in refined */
2328           v = solv->problems.elements[i];
2329           for (j = 0; problem[j]; j++)
2330             if (problem[j] != sug && problem[j] == v)
2331               break;
2332           if (problem[j])
2333             continue;
2334           queue_push(&disabled, v);
2335         }
2336       if (disabled.count == disabledcnt)
2337         {
2338           /* no solution found, this was an invalid suggestion! */
2339           if (pool->verbose)
2340             printf("no solution found!\n");
2341           refined->count = 0;
2342           break;
2343         }
2344       if (disabled.count == disabledcnt + 1)
2345         {
2346           /* just one suggestion, add it to refined list */
2347           v = disabled.elements[disabledcnt];
2348           queue_push(refined, v);
2349           disableproblem(solv, v);
2350           if (v < 0)
2351             disableupdaterules(solv, job, -(v + 1));
2352         }
2353       else
2354         {
2355           /* more than one solution, disable all */
2356           /* do not push anything on refine list */
2357           if (pool->verbose > 1)
2358             {
2359               printf("more than one solution found:\n");
2360               for (i = disabledcnt; i < disabled.count; i++)
2361                 printproblem(solv, disabled.elements[i]);
2362             }
2363           for (i = disabledcnt; i < disabled.count; i++)
2364             disableproblem(solv, disabled.elements[i]);
2365         }
2366     }
2367   /* all done, get us back into the same state as before */
2368   /* enable refined rules again */
2369   for (i = 0; i < disabled.count; i++)
2370     enableproblem(solv, disabled.elements[i]);
2371   /* disable problem rules again */
2372   for (i = 0; problem[i]; i++)
2373     disableproblem(solv, problem[i]);
2374   if (pool->verbose)
2375     printf("refine_suggestion end\n");
2376 }
2377
2378 static void
2379 problems_to_solutions(Solver *solv, Queue *job)
2380 {
2381   Pool *pool = solv->pool;
2382   Queue problems;
2383   Queue solution;
2384   Queue solutions;
2385   Id *problem;
2386   Id why;
2387   int i, j;
2388
2389   if (!solv->problems.count)
2390     return;
2391   queue_clone(&problems, &solv->problems);
2392   queue_init(&solution);
2393   queue_init(&solutions);
2394   /* copy over problem rule */
2395   queue_push(&solutions, problems.elements[0]);
2396   queue_push(&solutions, problems.elements[1]);
2397   problem = problems.elements + 2;
2398   for (i = 2; i < problems.count; i++)
2399     {
2400       Id v = problems.elements[i];
2401       if (v == 0)
2402         {
2403           /* mark end of this problem */
2404           queue_push(&solutions, 0);
2405           queue_push(&solutions, 0);
2406           if (i + 1 == problems.count)
2407             break;
2408           /* copy over problem rule of next problem */
2409           queue_push(&solutions, problems.elements[i + 1]);
2410           queue_push(&solutions, problems.elements[i + 2]);
2411           i += 2;
2412           problem = problems.elements + i + 1;
2413           continue;
2414         }
2415       refine_suggestion(solv, job, problem, v, &solution);
2416       if (!solution.count)
2417         continue;       /* this solution didn't work out */
2418
2419       for (j = 0; j < solution.count; j++)
2420         {
2421           why = solution.elements[j];
2422 #if 0
2423           printproblem(solv, why);
2424 #endif
2425           if (why < 0)
2426             {
2427               queue_push(&solutions, 0);
2428               queue_push(&solutions, -why);
2429             }
2430           else if (why >= solv->systemrules && why < solv->weakrules)
2431             {
2432               Id p, rp = 0;
2433               p = solv->installed->start + (why - solv->systemrules);
2434               if (solv->weaksystemrules && solv->weaksystemrules[why - solv->systemrules])
2435                 {
2436                   Id *dp = pool->whatprovidesdata + solv->weaksystemrules[why - solv->systemrules];
2437                   for (; *dp; dp++)
2438                     {
2439                       if (*dp >= solv->installed->start && *dp < solv->installed->start + solv->installed->nsolvables)
2440                         continue;
2441                       if (solv->decisionmap[*dp] > 0)
2442                         {
2443                           rp = *dp;
2444                           break;
2445                         }
2446                     }
2447                 }
2448               queue_push(&solutions, p);
2449               queue_push(&solutions, rp);
2450             }
2451           else
2452             abort();
2453         }
2454       /* mark end of this solution */
2455       queue_push(&solutions, 0);
2456       queue_push(&solutions, 0);
2457     }
2458   queue_free(&solution);
2459   queue_free(&problems);
2460   /* copy queue over to solutions */
2461   queue_free(&solv->problems);
2462   queue_clone(&solv->problems, &solutions);
2463   queue_free(&solutions);
2464 }
2465
2466
2467   
2468 /*
2469  * printdecisions
2470  */
2471   
2472 static const char *
2473 id2rc(Solver *solv, Id id)
2474 {
2475   const char *evr;
2476   if (solv->rc_output != 2)
2477     return "";
2478   evr = id2str(solv->pool, id);
2479   if (*evr < '0' || *evr > '9')
2480     return "0:";
2481   while (*evr >= '0' && *evr <= '9')
2482     evr++;
2483   if (*evr != ':')
2484     return "0:";
2485   return "";
2486 }
2487
2488 void
2489 printdecisions(Solver *solv)
2490 {
2491   Pool *pool = solv->pool;
2492   Repo *installed = solv->installed;
2493   Id p, *obsoletesmap;
2494   int i;
2495   Solvable *s;
2496
2497   obsoletesmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
2498   if (installed)
2499     {
2500       for (i = 0; i < solv->decisionq.count; i++)
2501         {
2502           Id *pp, n;
2503
2504           n = solv->decisionq.elements[i];
2505           if (n < 0)
2506             continue;
2507           if (n == SYSTEMSOLVABLE)
2508             continue;
2509           s = pool->solvables + n;
2510           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2511             continue;
2512           FOR_PROVIDES(p, pp, s->name)
2513             if (s->name == pool->solvables[p].name)
2514               {
2515                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2516                   {
2517                     obsoletesmap[p] = n;
2518                     obsoletesmap[n]++;
2519                   }
2520               }
2521         }
2522       for (i = 0; i < solv->decisionq.count; i++)
2523         {
2524           Id obs, *obsp;
2525           Id *pp, n;
2526
2527           n = solv->decisionq.elements[i];
2528           if (n < 0)
2529             continue;
2530           if (n == SYSTEMSOLVABLE)
2531             continue;
2532           s = pool->solvables + n;
2533           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2534             continue;
2535           if (!s->obsoletes)
2536             continue;
2537           obsp = s->repo->idarraydata + s->obsoletes;
2538           while ((obs = *obsp++) != 0)
2539             FOR_PROVIDES(p, pp, obs)
2540               {
2541                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2542                   {
2543                     obsoletesmap[p] = n;
2544                     obsoletesmap[n]++;
2545                   }
2546               }
2547         }
2548     }
2549
2550   if (solv->rc_output)
2551     printf(">!> Solution #1:\n");
2552
2553   int installs = 0, uninstalls = 0, upgrades = 0;
2554   
2555   /* print solvables to be erased */
2556
2557   if (installed)
2558     {
2559       for (i = installed->start; i < installed->end; i++)
2560         {
2561           s = pool->solvables + i;
2562           if (s->repo != installed)
2563             continue;
2564           if (solv->decisionmap[i] > 0)
2565             continue;
2566           if (obsoletesmap[i])
2567             continue;
2568           if (solv->rc_output == 2)
2569             printf(">!> remove  %s-%s%s\n", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2570           else if (solv->rc_output)
2571             printf(">!> remove  %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2572           else
2573             printf("erase   %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2574           uninstalls++;
2575         }
2576     }
2577
2578   /* print solvables to be installed */
2579
2580   for (i = 0; i < solv->decisionq.count; i++)
2581     {
2582       int j;
2583       p = solv->decisionq.elements[i];
2584       if (p < 0)
2585         continue;
2586       if (p == SYSTEMSOLVABLE)
2587         continue;
2588       s = pool->solvables + p;
2589       if (installed && s->repo == installed)
2590         continue;
2591
2592       if (!obsoletesmap[p])
2593         {
2594           if (solv->rc_output)
2595             printf(">!> ");
2596           printf("install %s-%s%s", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2597           if (solv->rc_output != 2)
2598             printf(".%s", id2str(pool, s->arch));
2599           installs++;
2600         }
2601       else if (!solv->rc_output)
2602         {
2603           printf("update  %s-%s.%s  (obsoletes", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2604           for (j = installed->start; j < installed->end; j++)
2605             {
2606               if (obsoletesmap[j] != p)
2607                 continue;
2608               s = pool->solvables + j;
2609               printf(" %s-%s.%s", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2610             }
2611           printf(")");
2612           upgrades++;
2613         }
2614       else
2615         {
2616           Solvable *f, *fn = 0;
2617           for (j = installed->start; j < installed->end; j++)
2618             {
2619               if (obsoletesmap[j] != p)
2620                 continue;
2621               f = pool->solvables + j;
2622               if (fn || f->name != s->name)
2623                 {
2624                   if (solv->rc_output == 2)
2625                     printf(">!> remove  %s-%s%s\n", id2str(pool, f->name), id2rc(solv, f->evr), id2str(pool, f->evr));
2626                   else if (solv->rc_output)
2627                     printf(">!> remove  %s-%s.%s\n", id2str(pool, f->name), id2str(pool, f->evr), id2str(pool, f->arch));
2628                   uninstalls++;
2629                 }
2630               else
2631                 fn = f;
2632             }
2633           if (!fn)
2634             {
2635               printf(">!> install %s-%s%s", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2636               if (solv->rc_output != 2)
2637                 printf(".%s", id2str(pool, s->arch));
2638               installs++;
2639             }
2640           else
2641             {
2642               if (solv->rc_output == 2)
2643                 printf(">!> upgrade %s-%s => %s-%s%s", id2str(pool, fn->name), id2str(pool, fn->evr), id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2644               else
2645                 printf(">!> upgrade %s-%s.%s => %s-%s.%s", id2str(pool, fn->name), id2str(pool, fn->evr), id2str(pool, fn->arch), id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2646               upgrades++;
2647             }
2648         }
2649       if (solv->rc_output)
2650         {
2651           Repo *repo = s->repo;
2652           if (repo && strcmp(repo_name(repo), "locales"))
2653             printf("[%s]", repo_name(repo));
2654         }
2655       printf("\n");
2656     }
2657
2658   if (solv->rc_output)
2659     printf(">!> installs=%d, upgrades=%d, uninstalls=%d\n", installs, upgrades, uninstalls);
2660   
2661   xfree(obsoletesmap);
2662
2663   if (solv->suggestions.count)
2664     {
2665       printf("\nsuggested packages:\n");
2666       for (i = 0; i < solv->suggestions.count; i++)
2667         {
2668           s = pool->solvables + solv->suggestions.elements[i];
2669           printf("- %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2670         }
2671     }
2672 }
2673
2674 int
2675 printconflicts(Solver *solv, Solvable *s, Id pc)
2676 {
2677   Pool *pool = solv->pool;
2678   Solvable *sc = pool->solvables + pc;
2679   Id p, *pp, con, *conp, obs, *obsp;
2680   int numc = 0;
2681
2682   if (s->conflicts)
2683     {
2684       conp = s->repo->idarraydata + s->conflicts;
2685       while ((con = *conp++) != 0)
2686         {
2687           FOR_PROVIDES(p, pp, con)
2688             {
2689               if (p != pc)
2690                 continue;
2691               printf("packags %s-%s.%s conflicts with %s, which is provided by %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, con), id2str(pool, sc->name), id2str(pool, sc->evr), id2str(pool, sc->arch));
2692               numc++;
2693             }
2694         }
2695     }
2696   if (s->obsoletes && (!solv->installed || s->repo != solv->installed))
2697     {
2698       obsp = s->repo->idarraydata + s->obsoletes;
2699       while ((obs = *obsp++) != 0)
2700         {
2701           FOR_PROVIDES(p, pp, obs)
2702             {
2703               if (p != pc)
2704                 continue;
2705               printf("packags %s-%s.%s obsolets %s, which is provided by %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, obs), id2str(pool, sc->name), id2str(pool, sc->evr), id2str(pool, sc->arch));
2706               numc++;
2707             }
2708         }
2709     }
2710   return numc;
2711 }
2712
2713 void
2714 printprobleminfo(Solver *solv, Id p, Id d, Queue *job, Id firstp, Id firstrp)
2715 {
2716   Pool *pool = solv->pool;
2717   Rule *r;
2718   Solvable *s;
2719   Id what;
2720
2721   if (p != 0)
2722     {
2723       /* learnt rule, ignore for now */
2724       printf("some learnt rule...\n");
2725       return;
2726     }
2727   if (d == 0)
2728     {
2729       /* conflict with system solvable, i.e. could not create rule */
2730       if (firstp)
2731         {
2732           printf("got firstp\n");
2733           abort();
2734         }
2735       what = job->elements[firstrp];
2736       switch (job->elements[firstrp - 1])
2737         {
2738         case SOLVER_INSTALL_SOLVABLE_NAME:
2739           printf("no solvable exists with name %s\n", dep2str(pool, what));
2740           break;
2741         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2742           printf("no solvable provides %s\n", dep2str(pool, what));
2743           break;
2744         default:
2745           printf("unknown  job\n");
2746           abort();
2747         }
2748       return;
2749     }
2750   else if (d < 0)
2751     {
2752       Id req, *reqp, *dp;
2753       int count = 0;
2754       /* conflict with rpm rule, package -d is not installable */
2755       s = pool->solvables + (-d);
2756       if (s->requires)
2757         {
2758           reqp = s->repo->idarraydata + s->requires;
2759           while ((req = *reqp++) != 0)
2760             {
2761               if (req == SOLVABLE_PREREQMARKER)
2762                 continue;
2763               dp = GET_PROVIDESP(req, p);
2764               if (*dp)
2765                 continue;
2766               printf("package %s-%s.%s requires %s, but no package provides it\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, req));
2767               count++;
2768             }
2769         }
2770       if (!count)
2771         printf("package %s-%s.%s is not installable\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2772       return;
2773     }
2774   if (d >= solv->jobrules)
2775     {
2776       r = solv->rules + d;
2777       p = r->p;
2778       d = r->d;
2779       if (p < 0 && d < 0)
2780         {
2781           Solvable *sp, *sd;
2782           sp = pool->solvables + (-p);
2783           sd = pool->solvables + (-d);
2784           printf("package %s-%s.%s cannot be installed with package %s-%s.%s\n", id2str(pool, sp->name), id2str(pool, sp->evr), id2str(pool, sp->arch), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2785           return;
2786         }
2787       printf("some job rule...\n");
2788       printrule(solv, r);
2789       return;
2790     }
2791   r = solv->rules + d;
2792   p = r->p;
2793   if (p >= 0)
2794     abort();
2795   d = r->d;
2796   if (d == 0 && r->w2 < 0)
2797     {
2798       Solvable *sp, *sd;
2799       d = r->w2;
2800       sp = pool->solvables + (-p);
2801       sd = pool->solvables + (-d);
2802       if (sp->name == sd->name)
2803         {
2804           printf("cannot install both %s-%s.%s and %s-%s.%s\n", id2str(pool, sp->name), id2str(pool, sp->evr), id2str(pool, sp->arch), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2805         }
2806       else
2807         {
2808           printconflicts(solv, pool->solvables + (-p), -d);
2809           printconflicts(solv, pool->solvables + (-d), -p);
2810         }
2811     }
2812   else
2813     {
2814       /* find requires of p that corresponds with our rule */
2815       Id req, *reqp, *dp;
2816       s = pool->solvables + (-p);
2817       reqp = s->repo->idarraydata + s->requires;
2818       while ((req = *reqp++) != 0)
2819         {
2820           if (req == SOLVABLE_PREREQMARKER)
2821             continue;
2822           dp = GET_PROVIDESP(req, p);
2823           if (d == 0)
2824             {
2825               if (*dp == r->w2 && dp[1] == 0)
2826                 break;
2827             }
2828           else if (dp - pool->whatprovidesdata == d)
2829             break;
2830         }
2831       if (!req)
2832         {
2833           printf("req not found\n");
2834           abort();
2835         }
2836       printf("package %s-%s.%s requires %s, but none of its providers can be installed\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, req));
2837     }
2838 }
2839
2840 void
2841 printsolutions(Solver *solv, Queue *job)
2842 {
2843   Pool *pool = solv->pool;
2844   int pcnt;
2845   int i;
2846   Id p, d, rp, what;
2847   Solvable *s, *sd;
2848
2849   printf("Encountered problems! Here are the solutions:\n\n");
2850   pcnt = 1;
2851   for (i = 0; i < solv->problems.count; )
2852     {
2853       printf("Problem %d:\n", pcnt++);
2854       printf("====================================\n");
2855       p = solv->problems.elements[i++];
2856       d = solv->problems.elements[i++];
2857       printprobleminfo(solv, p, d, job, solv->problems.elements[i], solv->problems.elements[i + 1]);
2858       printf("\n");
2859       for (;;)
2860         {
2861           if (solv->problems.elements[i] == 0 && solv->problems.elements[i + 1] == 0)
2862             {
2863               /* end of solutions for this problems reached */
2864               i += 2;
2865               break;
2866             }
2867           for (;;)
2868             {
2869               p = solv->problems.elements[i];
2870               rp = solv->problems.elements[i + 1];
2871               i += 2;
2872               if (p == 0 && rp == 0)
2873                 {
2874                   /* end of this solution reached */
2875                   printf("\n");
2876                   break;
2877                 }
2878               if (p == 0)
2879                 {
2880                   /* job, p is index into job queue */
2881                   what = job->elements[rp];
2882                   switch (job->elements[rp - 1])
2883                     {
2884                     case SOLVER_INSTALL_SOLVABLE:
2885                       s = pool->solvables + what;
2886                       if (solv->installed && s->repo == solv->installed)
2887                         printf("- do not keep %s-%s.%s installed\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2888                       else
2889                         printf("- do not install %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2890                       break;
2891                     case SOLVER_ERASE_SOLVABLE:
2892                       s = pool->solvables + what;
2893                       if (solv->installed && s->repo == solv->installed)
2894                         printf("- do not deinstall %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2895                       else
2896                         printf("- do not forbid installation of %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2897                       break;
2898                     case SOLVER_INSTALL_SOLVABLE_NAME:
2899                       printf("- do not install %s\n", id2str(pool, what));
2900                       break;
2901                     case SOLVER_ERASE_SOLVABLE_NAME:
2902                       printf("- do not deinstall %s\n", id2str(pool, what));
2903                       break;
2904                     case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2905                       printf("- do not install a solvable providing %s\n", dep2str(pool, what));
2906                       break;
2907                     case SOLVER_ERASE_SOLVABLE_PROVIDES:
2908                       printf("- do not deinstall all solvables providing %s\n", dep2str(pool, what));
2909                       break;
2910                     case SOLVER_INSTALL_SOLVABLE_UPDATE:
2911                       s = pool->solvables + what;
2912                       printf("- do not install most recent version of %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool
2913     , s->arch));
2914                       break;
2915                     default:
2916                       printf("- do something different\n");
2917                       break;
2918                     }
2919                 }
2920               else
2921                 {
2922                   /* policy, replace p with rp */
2923                   s = pool->solvables + p;
2924                   sd = rp ? pool->solvables + rp : 0;
2925                   if (sd)
2926                     {
2927                       int gotone = 0;
2928                       if (!solv->allowdowngrade && evrcmp(pool, s->evr, sd->evr) > 0)
2929                         {
2930                           printf("- allow downgrade of %s-%s.%s to %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2931                           gotone = 1;
2932                         }
2933                       if (!solv->allowarchchange && s->name == sd->name && s->arch != sd->arch && policy_illegal_archchange(pool, s, sd))
2934                         {
2935                           printf("- allow architecture change of %s-%s.%s to %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2936                           gotone = 1;
2937                         }
2938                       if (!solv->allowvendorchange && s->name == sd->name && s->vendor != sd->vendor && policy_illegal_vendorchange(pool, s, sd))
2939                         {
2940                           if (sd->vendor)
2941                             printf("- allow vendor change from '%s' (%s-%s.%s) to '%s' (%s-%s.%s)\n", id2str(pool, s->vendor), id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), id2str(pool, sd->vendor), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2942                           else
2943                             printf("- allow vendor change from '%s' (%s-%s.%s) to no vendor (%s-%s.%s)\n", id2str(pool, s->vendor), id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2944                           gotone = 1;
2945                         }
2946                       if (!gotone)
2947                         printf("- allow replacement of %s-%s.%s with %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2948                     }
2949                   else
2950                     {
2951                       printf("- allow deinstallation of %s-%s.%s [%d]\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), (Id)(s - pool->solvables));
2952                     }
2953
2954                 }
2955             }
2956         }
2957     }
2958 }
2959
2960
2961 /* for each installed solvable find which packages with *different* names
2962  * obsolete the solvable.
2963  * this index is used in policy_findupdatepackages if noupdateprovide is set.
2964  */
2965
2966 static void
2967 create_obsolete_index(Solver *solv)
2968 {
2969   Pool *pool = solv->pool;
2970   Solvable *s;
2971   Repo *installed = solv->installed;
2972   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
2973   int i, n;
2974
2975   if (!installed || !installed->nsolvables)
2976     return;
2977   /* create reverse obsoletes map for installed solvables */
2978   solv->obsoletes = obsoletes = xcalloc(installed->end - installed->start, sizeof(Id));
2979   for (i = 1; i < pool->nsolvables; i++)
2980     {
2981       s = pool->solvables + i;
2982       if (s->repo == installed)
2983         continue;
2984       if (!s->obsoletes)
2985         continue;
2986       if (!pool_installable(pool, s))
2987         continue;
2988       obsp = s->repo->idarraydata + s->obsoletes;
2989       while ((obs = *obsp++) != 0)
2990         FOR_PROVIDES(p, pp, obs)
2991           {
2992             if (pool->solvables[p].repo != installed)
2993               continue;
2994             if (pool->solvables[p].name == s->name)
2995               continue;
2996             obsoletes[p - installed->start]++;
2997           }
2998     }
2999   n = 0;
3000   for (i = 0; i < installed->nsolvables; i++)
3001     if (obsoletes[i])
3002       {
3003         n += obsoletes[i] + 1;
3004         obsoletes[i] = n;
3005       }
3006   solv->obsoletes_data = obsoletes_data = xcalloc(n + 1, sizeof(Id));
3007   if (pool->verbose) printf("obsoletes data: %d entries\n", n + 1);
3008   for (i = pool->nsolvables - 1; i > 0; i--)
3009     {
3010       s = pool->solvables + i;
3011       if (!s->obsoletes)
3012         continue;
3013       if (!pool_installable(pool, s))
3014         continue;
3015       obsp = s->repo->idarraydata + s->obsoletes;
3016       while ((obs = *obsp++) != 0)
3017         FOR_PROVIDES(p, pp, obs)
3018           {
3019             if (pool->solvables[p].repo != installed)
3020               continue;
3021             if (pool->solvables[p].name == s->name)
3022               continue;
3023             p -= installed->start;
3024             if (obsoletes_data[obsoletes[p]] != i)
3025               obsoletes_data[--obsoletes[p]] = i;
3026           }
3027     }
3028 }
3029
3030
3031 /*-----------------------------------------------------------------*/
3032 /* main() */
3033
3034 /*
3035  *
3036  * solve job queue
3037  *
3038  */
3039
3040 void
3041 solve(Solver *solv, Queue *job)
3042 {
3043   Pool *pool = solv->pool;
3044   Repo *installed = solv->installed;
3045   int i;
3046   Map addedmap;                        /* '1' == have rule for solvable */
3047   Id how, what, p, *pp, d;
3048   Queue q;
3049   Solvable *s;
3050
3051   /* create obsolete index if needed */
3052   if (solv->noupdateprovide)
3053     create_obsolete_index(solv);
3054
3055   /*
3056    * create basic rule set of all involved packages
3057    * use addedmap bitmap to make sure we don't create rules twice
3058    * 
3059    */
3060
3061   map_init(&addedmap, pool->nsolvables);
3062   queue_init(&q);
3063
3064   /*
3065    * always install our system solvable
3066    */
3067   MAPSET(&addedmap, SYSTEMSOLVABLE);
3068   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
3069   queue_push(&solv->decisionq_why, 0);
3070   solv->decisionmap[SYSTEMSOLVABLE] = 1;
3071
3072   /*
3073    * create rules for all package that could be involved with the solving
3074    * so called: rpm rules
3075    * 
3076    */
3077   if (installed)
3078     {
3079       if (pool->verbose > 3)
3080         printf ("*** create rules for installed solvables ***\n");
3081       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3082         if (s->repo == installed)
3083           addrpmrulesforsolvable(solv, s, &addedmap);
3084       if (pool->verbose > 3)
3085         printf ("*** create rules for updaters of installed solvables ***\n");
3086       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3087         if (s->repo == installed)
3088           addrpmrulesforupdaters(solv, s, &addedmap, 1);
3089     }
3090
3091   if (solv->pool->verbose > 3)
3092     printf ("*** create rpm rules for packages involved with a job ***\n");
3093   for (i = 0; i < job->count; i += 2)
3094     {
3095       how = job->elements[i];
3096       what = job->elements[i + 1];
3097
3098       switch(how)
3099         {
3100         case SOLVER_INSTALL_SOLVABLE:
3101           addrpmrulesforsolvable(solv, pool->solvables + what, &addedmap);
3102           break;
3103         case SOLVER_INSTALL_SOLVABLE_NAME:
3104         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3105           FOR_PROVIDES(p, pp, what)
3106             {
3107               /* if by name, ensure that the name matches */
3108               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3109                 continue;
3110               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3111             }
3112           break;
3113         case SOLVER_INSTALL_SOLVABLE_UPDATE:
3114           /* dont allow downgrade */
3115           addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
3116           break;
3117         }
3118     }
3119
3120   if (solv->pool->verbose > 3)
3121     printf ("*** create rpm rules for recommended/suggested packages ***\n");
3122   if (solv->pool->verbose > 3)
3123       printf ("*** Add rules for week dependencies ***\n");
3124
3125
3126   addrpmrulesforweak(solv, &addedmap);
3127
3128 #if 1
3129   if (pool->verbose)
3130     {
3131       int possible = 0, installable = 0;
3132       for (i = 1; i < pool->nsolvables; i++)
3133         {
3134           if (pool_installable(pool, pool->solvables + i))
3135             installable++;
3136           if (MAPTST(&addedmap, i))
3137             possible++;
3138         }
3139       printf("%d of %d installable solvables considered for solving\n", possible, installable);
3140     }
3141 #endif
3142
3143   /*
3144    * first pass done, we now have all the rpm rules we need.
3145    * unify existing rules before going over all job rules and
3146    * policy rules.
3147    * at this point the system is always solvable,
3148    * as an empty system (remove all packages) is a valid solution
3149    */
3150   
3151   unifyrules(solv);     /* remove duplicate rpm rules */
3152
3153   if (pool->verbose) printf("Decisions based on %d rpm rules.\n", solv->decisionq.count);
3154
3155   /*
3156    * now add all job rules
3157    */
3158
3159   if (solv->pool->verbose > 3)
3160       printf ("*** Add JOB rules ***\n");  
3161   
3162   solv->jobrules = solv->nrules;
3163
3164   for (i = 0; i < job->count; i += 2)
3165     {
3166       how = job->elements[i];
3167       what = job->elements[i + 1];
3168       switch(how)
3169         {
3170         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
3171           s = pool->solvables + what;
3172           if (solv->rc_output)
3173             {
3174               printf(">!> Installing %s from channel %s\n", id2str(pool, s->name), repo_name(s->repo));
3175             }
3176           if (pool->verbose)
3177             printf("job: install solvable %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
3178           addrule(solv, what, 0);                       /* install by Id */
3179           queue_push(&solv->ruletojob, i);
3180           break;
3181         case SOLVER_ERASE_SOLVABLE:
3182           s = pool->solvables + what;
3183           if (pool->verbose)
3184             printf("job: erase solvable %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
3185           addrule(solv, -what, 0);                      /* remove by Id */
3186           queue_push(&solv->ruletojob, i);
3187           break;
3188         case SOLVER_INSTALL_SOLVABLE_NAME:              /* install by capability */
3189         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3190           if (pool->verbose && how == SOLVER_INSTALL_SOLVABLE_NAME)
3191             printf("job: install name %s\n", id2str(pool, what));
3192           if (pool->verbose && how == SOLVER_INSTALL_SOLVABLE_PROVIDES)
3193             printf("job: install provides %s\n", dep2str(pool, what));
3194           queue_empty(&q);
3195           FOR_PROVIDES(p, pp, what)
3196             {
3197               /* if by name, ensure that the name matches */
3198               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3199                 continue;
3200               queue_push(&q, p);
3201             }
3202           if (!q.count) 
3203             {
3204               /* no provider, make this an impossible rule */
3205               queue_push(&q, -SYSTEMSOLVABLE);
3206             }
3207
3208           p = queue_shift(&q);         /* get first provider */
3209           if (!q.count)
3210             d = 0;                     /* single provider ? -> make assertion */
3211           else
3212             d = pool_queuetowhatprovides(pool, &q);   /* get all providers */
3213           addrule(solv, p, d);         /* add 'requires' rule */
3214           queue_push(&solv->ruletojob, i);
3215           break;
3216         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
3217         case SOLVER_ERASE_SOLVABLE_PROVIDES:
3218           if (pool->verbose && how == SOLVER_ERASE_SOLVABLE_NAME)
3219             printf("job: erase name %s\n", id2str(pool, what));
3220           if (pool->verbose && how == SOLVER_ERASE_SOLVABLE_PROVIDES)
3221             printf("job: erase provides %s\n", dep2str(pool, what));
3222           FOR_PROVIDES(p, pp, what)
3223             {
3224               /* if by name, ensure that the name matches */
3225               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
3226                 continue;
3227               addrule(solv, -p, 0);  /* add 'remove' rule */
3228               queue_push(&solv->ruletojob, i);
3229             }
3230           break;
3231         case SOLVER_INSTALL_SOLVABLE_UPDATE:              /* find update for solvable */
3232           s = pool->solvables + what;
3233           if (pool->verbose)
3234             printf("job: update %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
3235           addupdaterule(solv, s, 0);
3236           queue_push(&solv->ruletojob, i);
3237           break;
3238         }
3239     }
3240
3241   if (solv->ruletojob.count != solv->nrules - solv->jobrules)
3242     abort();
3243
3244   /*
3245    * now add system rules
3246    * 
3247    */
3248
3249  if (solv->pool->verbose > 3)
3250      printf ("*** Add system rules ***\n");
3251   
3252   
3253   solv->systemrules = solv->nrules;
3254
3255   /*
3256    * create rules for updating installed solvables
3257    * 
3258    */
3259   
3260   if (installed && !solv->allowuninstall)
3261     {                                  /* loop over all installed solvables */
3262       /* we create all update rules, but disable some later on depending on the job */
3263       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3264         if (s->repo == installed)
3265           addupdaterule(solv, s, 0);
3266         else
3267           addupdaterule(solv, 0, 0);    /* create dummy rule */
3268       /* consistency check: we added a rule for _every_ system solvable */
3269       if (solv->nrules - solv->systemrules != installed->end - installed->start)
3270         abort();
3271     }
3272
3273   /* create special weak system rules */
3274   /* those are used later on to keep a version of the installed packages in
3275      best effort mode */
3276   if (installed && installed->nsolvables)
3277     {
3278       solv->weaksystemrules = xcalloc(installed->end - installed->start, sizeof(Id));
3279       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3280         if (s->repo == installed)
3281           {
3282             policy_findupdatepackages(solv, s, &q, 1);
3283             if (q.count)
3284               solv->weaksystemrules[i - installed->start] = pool_queuetowhatprovides(pool, &q);
3285           }
3286     }
3287
3288   /* free unneeded memory */
3289   map_free(&addedmap);
3290   queue_free(&q);
3291
3292   solv->weakrules = solv->nrules;
3293
3294   /* try real hard to keep packages installed */
3295   if (0)
3296     {
3297       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3298         if (s->repo == installed)
3299           {
3300             /* FIXME: can't work with refine_suggestion! */
3301             /* need to always add the rule but disable it */
3302             if (MAPTST(&solv->noupdate, i - installed->start))
3303               continue;
3304             d = solv->weaksystemrules[i - installed->start];
3305             addrule(solv, i, d);
3306           }
3307     }
3308
3309   /*
3310    * solve !
3311    * 
3312    */
3313   
3314   disableupdaterules(solv, job, -1);
3315   makeruledecisions(solv);
3316
3317   if (pool->verbose) printf("problems so far: %d\n", solv->problems.count);
3318
3319   run_solver(solv, 1, 1);
3320
3321   /* find suggested packages */
3322   if (!solv->problems.count)
3323     {
3324       Id sug, *sugp, p, *pp;
3325
3326       /* create map of all suggests that are still open */
3327       solv->recommends_index = -1;
3328       MAPZERO(&solv->suggestsmap);
3329       for (i = 0; i < solv->decisionq.count; i++)
3330         {
3331           p = solv->decisionq.elements[i];
3332           if (p < 0)
3333             continue;
3334           s = pool->solvables + p;
3335           if (s->suggests)
3336             {
3337               sugp = s->repo->idarraydata + s->suggests;
3338               while ((sug = *sugp++) != 0)
3339                 {
3340                   FOR_PROVIDES(p, pp, sug)
3341                     if (solv->decisionmap[p] > 0)
3342                       break;
3343                   if (p)
3344                     continue;   /* already fulfilled */
3345                   FOR_PROVIDES(p, pp, sug)
3346                     MAPSET(&solv->suggestsmap, p);
3347                 }
3348             }
3349         }
3350       for (i = 1; i < pool->nsolvables; i++)
3351         {
3352           if (solv->decisionmap[i] != 0)
3353             continue;
3354           s = pool->solvables + i;
3355           if (!MAPTST(&solv->suggestsmap, i))
3356             {
3357               if (!s->enhances)
3358                 continue;
3359               if (!pool_installable(pool, s))
3360                 continue;
3361               if (!solver_is_enhancing(solv, s))
3362                 continue;
3363             }
3364           queue_push(&solv->suggestions, i);
3365         }
3366       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
3367     }
3368
3369   if (solv->problems.count)
3370     problems_to_solutions(solv, job);
3371 }
3372