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