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