src/solver.c

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