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