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