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