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