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