src/solver.c

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