src/solver.c

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