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 /*-------------------------------------------------------------------
1049  *
1050  * add (install) rules for solvable
1051  *
1052  * s: Solvable for which to add rules
1053  * m: m[s] = 1 for solvables which have rules, prevent rule duplication
1054  *
1055  * Algorithm: 'visit all nodes of a graph'. The graph nodes are
1056  *  solvables, the edges their dependencies.
1057  *  Starting from an installed solvable, this will create all rules
1058  *  representing the graph created by the solvables dependencies.
1059  *
1060  * for unfulfilled requirements, conflicts, obsoletes,....
1061  * add a negative assertion for solvables that are not installable
1062  *
1063  * It will also create rules for all solvables referenced by 's'
1064  *  i.e. descend to all providers of requirements of 's'
1065  *
1066  */
1067
1068 static void
1069 addrpmrulesforsolvable(Solver *solv, Solvable *s, Map *m)
1070 {
1071   Pool *pool = solv->pool;
1072   Repo *installed = solv->installed;
1073
1074   /* 'work' queue. keeps Ids of solvables we still have to work on.
1075      And buffer for it. */
1076   Queue workq;
1077   Id workqbuf[64];
1078
1079   int i;
1080     /* if to add rules for broken deps ('rpm -V' functionality)
1081      * 0 = yes, 1 = no
1082      */
1083   int dontfix;
1084 #if CODE10
1085   int patchatom;
1086 #endif
1087     /* Id var and pointer for each dependency
1088      * (not used in parallel)
1089      */
1090   Id req, *reqp;
1091   Id con, *conp;
1092   Id obs, *obsp;
1093   Id rec, *recp;
1094   Id sug, *sugp;
1095     /* var and ptr for loops */
1096   Id p, *pp;
1097     /* ptr to 'whatprovides' */
1098   Id *dp;
1099     /* Id for current solvable 's' */
1100   Id n;
1101
1102   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforsolvable -----\n");
1103
1104   queue_init_buffer(&workq, workqbuf, sizeof(workqbuf)/sizeof(*workqbuf));
1105   queue_push(&workq, s - pool->solvables);      /* push solvable Id to work queue */
1106
1107   /* loop until there's no more work left */
1108   while (workq.count)
1109     {
1110       /*
1111        * n: Id of solvable
1112        * s: Pointer to solvable
1113        */
1114
1115       n = queue_shift(&workq);             /* 'pop' next solvable to work on from queue */
1116       if (MAPTST(m, n))                    /* continue if already visited */
1117         continue;
1118
1119       MAPSET(m, n);                        /* mark as visited */
1120       s = pool->solvables + n;             /* s = Solvable in question */
1121
1122       dontfix = 0;
1123       if (installed                        /* Installed system available */
1124           && !solv->fixsystem              /* NOT repair errors in rpm dependency graph */
1125           && s->repo == installed)         /* solvable is installed? */
1126       {
1127         dontfix = 1;                       /* dont care about broken rpm deps */
1128       }
1129
1130       if (!dontfix
1131           && s->arch != ARCH_SRC
1132           && s->arch != ARCH_NOSRC
1133           && !pool_installable(pool, s))
1134         {
1135           POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "package %s [%d] is not installable\n", solvable2str(pool, s), (Id)(s - pool->solvables));
1136           addrule(solv, -n, 0);            /* uninstallable */
1137         }
1138
1139       /*-----------------------------------------
1140        * check requires of s
1141        */
1142
1143       if (s->requires)
1144         {
1145           reqp = s->repo->idarraydata + s->requires;
1146           while ((req = *reqp++) != 0)            /* go through all requires */
1147             {
1148               if (req == SOLVABLE_PREREQMARKER)   /* skip the marker */
1149                 continue;
1150
1151               /* find list of solvables providing 'req' */
1152               dp = pool_whatprovides(pool, req);
1153
1154               if (*dp == SYSTEMSOLVABLE)          /* always installed */
1155                 continue;
1156
1157 #if CODE10
1158               if (patchatom)
1159                 {
1160                   addpatchatomrequires(solv, s, dp, &workq, m);
1161                   continue;
1162                 }
1163 #endif
1164               if (dontfix)
1165                 {
1166                   /* the strategy here is to not insist on dependencies
1167                    * that are already broken. so if we find one provider
1168                    * that was already installed, we know that the
1169                    * dependency was not broken before so we enforce it */
1170
1171                   /* check if any of the providers for 'req' is installed */
1172                   for (i = 0; (p = dp[i]) != 0; i++)
1173                     {
1174                       if (pool->solvables[p].repo == installed)
1175                         break;          /* provider was installed */
1176                     }
1177                   /* didn't find an installed provider: previously broken dependency */
1178                   if (!p)
1179                     {
1180                       POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "ignoring broken requires %s of installed package %s\n", dep2str(pool, req), solvable2str(pool, s));
1181                       continue;
1182                     }
1183                 }
1184
1185               if (!*dp)
1186                 {
1187                   /* nothing provides req! */
1188                   POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "package %s [%d] is not installable (%s)\n", solvable2str(pool, s), (Id)(s - pool->solvables), dep2str(pool, req));
1189                   addrule(solv, -n, 0); /* mark requestor as uninstallable */
1190                   continue;
1191                 }
1192
1193               IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
1194                 {
1195                   POOL_DEBUG(SAT_DEBUG_RULE_CREATION,"  %s requires %s\n", solvable2str(pool, s), dep2str(pool, req));
1196                   for (i = 0; dp[i]; i++)
1197                     POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "   provided by %s\n", solvable2str(pool, pool->solvables + dp[i]));
1198                 }
1199
1200               /* add 'requires' dependency */
1201               /* rule: (-requestor|provider1|provider2|...|providerN) */
1202               addrule(solv, -n, dp - pool->whatprovidesdata);
1203
1204               /* descend the dependency tree
1205                  push all non-visited providers on the work queue */
1206               for (; *dp; dp++)
1207                 {
1208                   if (!MAPTST(m, *dp))
1209                     queue_push(&workq, *dp);
1210                 }
1211
1212             } /* while, requirements of n */
1213
1214         } /* if, requirements */
1215
1216       /* that's all we check for src packages */
1217       if (s->arch == ARCH_SRC || s->arch == ARCH_NOSRC)
1218         continue;
1219
1220       /*-----------------------------------------
1221        * check conflicts of s
1222        */
1223
1224       if (s->conflicts)
1225         {
1226           conp = s->repo->idarraydata + s->conflicts;
1227           /* foreach conflicts of 's' */
1228           while ((con = *conp++) != 0)
1229             {
1230               /* foreach providers of a conflict of 's' */
1231               FOR_PROVIDES(p, pp, con)
1232                 {
1233                   /* dontfix: dont care about conflicts with already installed packs */
1234                   if (dontfix && pool->solvables[p].repo == installed)
1235                     continue;
1236                   /* p == n: self conflict */
1237                   if (p == n && !solv->allowselfconflicts)
1238                     p = 0;      /* make it a negative assertion, aka 'uninstallable' */
1239                  /* rule: -n|-p: either solvable _or_ provider of conflict */
1240                   addrule(solv, -n, -p);
1241                 }
1242             }
1243         }
1244
1245       /*-----------------------------------------
1246        * check obsoletes if not installed
1247        * (only installation will trigger the obsoletes in rpm)
1248        */
1249       if (!installed || pool->solvables[n].repo != installed)
1250         {                              /* not installed */
1251           int noobs = solv->noobsoletes.size && MAPTST(&solv->noobsoletes, n);
1252           if (s->obsoletes && !noobs)
1253             {
1254               obsp = s->repo->idarraydata + s->obsoletes;
1255               /* foreach obsoletes */
1256               while ((obs = *obsp++) != 0)
1257                 {
1258                   /* foreach provider of an obsoletes of 's' */
1259                   FOR_PROVIDES(p, pp, obs)
1260                     {
1261                       if (!solv->obsoleteusesprovides /* obsoletes are matched names, not provides */
1262                           && !pool_match_nevr(pool, pool->solvables + p, obs))
1263                         continue;
1264                       addrule(solv, -n, -p);
1265                     }
1266                 }
1267             }
1268           FOR_PROVIDES(p, pp, s->name)
1269             {
1270               Solvable *ps = pool->solvables + p;
1271               /* we still obsolete packages with same nevra, like rpm does */
1272               /* (actually, rpm mixes those packages. yuck...) */
1273               if (noobs && (s->name != ps->name || s->evr != ps->evr || s->arch != ps->arch))
1274                 continue;
1275               if (!solv->implicitobsoleteusesprovides && s->name != ps->name)
1276                 continue;
1277               addrule(solv, -n, -p);
1278             }
1279         }
1280
1281       /*-----------------------------------------
1282        * add recommends to the work queue
1283        */
1284       if (s->recommends)
1285         {
1286           recp = s->repo->idarraydata + s->recommends;
1287           while ((rec = *recp++) != 0)
1288             {
1289               FOR_PROVIDES(p, pp, rec)
1290                 if (!MAPTST(m, p))
1291                   queue_push(&workq, p);
1292             }
1293         }
1294       if (s->suggests)
1295         {
1296           sugp = s->repo->idarraydata + s->suggests;
1297           while ((sug = *sugp++) != 0)
1298             {
1299               FOR_PROVIDES(p, pp, sug)
1300                 if (!MAPTST(m, p))
1301                   queue_push(&workq, p);
1302             }
1303         }
1304     }
1305   queue_free(&workq);
1306   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforsolvable end -----\n");
1307 }
1308
1309
1310 /*-------------------------------------------------------------------
1311  *
1312  * Add package rules for weak rules
1313  *
1314  * m: visited solvables
1315  */
1316
1317 static void
1318 addrpmrulesforweak(Solver *solv, Map *m)
1319 {
1320   Pool *pool = solv->pool;
1321   Solvable *s;
1322   Id sup, *supp;
1323   int i, n;
1324
1325   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforweak -----\n");
1326     /* foreach solvable in pool */
1327   for (i = n = 1; n < pool->nsolvables; i++, n++)
1328     {
1329       if (i == pool->nsolvables)                 /* wrap i */
1330         i = 1;
1331       if (MAPTST(m, i))                          /* been there */
1332         continue;
1333
1334       s = pool->solvables + i;
1335       if (!pool_installable(pool, s))            /* only look at installable ones */
1336         continue;
1337
1338       sup = 0;
1339       if (s->supplements)
1340         {
1341           /* find possible supplements */
1342           supp = s->repo->idarraydata + s->supplements;
1343           while ((sup = *supp++) != ID_NULL)
1344             if (dep_possible(solv, sup, m))
1345               break;
1346         }
1347
1348         /* if nothing found, check for enhances */
1349       if (!sup && s->enhances)
1350         {
1351           supp = s->repo->idarraydata + s->enhances;
1352           while ((sup = *supp++) != ID_NULL)
1353             if (dep_possible(solv, sup, m))
1354               break;
1355         }
1356         /* if nothing found, goto next solvables */
1357       if (!sup)
1358         continue;
1359       addrpmrulesforsolvable(solv, s, m);
1360       n = 0;
1361     }
1362   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforweak end -----\n");
1363 }
1364
1365
1366 /*-------------------------------------------------------------------
1367  *
1368  * add package rules for possible updates
1369  *
1370  * s: solvable
1371  * m: map of already visited solvables
1372  * allow_all: 0 = dont allow downgrades, 1 = allow all candidates
1373  */
1374
1375 static void
1376 addrpmrulesforupdaters(Solver *solv, Solvable *s, Map *m, int allow_all)
1377 {
1378   Pool *pool = solv->pool;
1379   int i;
1380     /* queue and buffer for it */
1381   Queue qs;
1382   Id qsbuf[64];
1383
1384   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforupdaters -----\n");
1385
1386   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1387     /* find update candidates for 's' */
1388   policy_findupdatepackages(solv, s, &qs, allow_all);
1389     /* add rule for 's' if not already done */
1390   if (!MAPTST(m, s - pool->solvables))
1391     addrpmrulesforsolvable(solv, s, m);
1392     /* foreach update candidate, add rule if not already done */
1393   for (i = 0; i < qs.count; i++)
1394     if (!MAPTST(m, qs.elements[i]))
1395       addrpmrulesforsolvable(solv, pool->solvables + qs.elements[i], m);
1396   queue_free(&qs);
1397
1398   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforupdaters -----\n");
1399 }
1400
1401 static Id
1402 finddistupgradepackages(Solver *solv, Solvable *s, Queue *qs, int allow_all)
1403 {
1404   Pool *pool = solv->pool;
1405   int i;
1406
1407   policy_findupdatepackages(solv, s, qs, allow_all);
1408   if (!qs->count)
1409     {
1410       if (allow_all)
1411         return 0;
1412       policy_findupdatepackages(solv, s, qs, 1);
1413       if (!qs->count)
1414         return 0;
1415       qs->count = 0;
1416       return -SYSTEMSOLVABLE;
1417     }
1418   if (allow_all)
1419     return s - pool->solvables;
1420   /* check if it is ok to keep the installed package */
1421   for (i = 0; i < qs->count; i++)
1422     {
1423       Solvable *ns = pool->solvables + qs->elements[i];
1424       if (s->evr == ns->evr && solvable_identical(pool, s, ns))
1425         return s - pool->solvables;
1426     }
1427   /* nope, it must be some other package */
1428   return queue_shift(qs);
1429 }
1430
1431 /*-------------------------------------------------------------------
1432  *
1433  * add rule for update
1434  *   (A|A1|A2|A3...)  An = update candidates for A
1435  *
1436  * s = (installed) solvable
1437  */
1438
1439 static void
1440 addupdaterule(Solver *solv, Solvable *s, int allow_all)
1441 {
1442   /* installed packages get a special upgrade allowed rule */
1443   Pool *pool = solv->pool;
1444   Id p, d;
1445   Queue qs;
1446   Id qsbuf[64];
1447
1448   POOL_DEBUG(SAT_DEBUG_SCHUBI, "-----  addupdaterule -----\n");
1449   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1450   p = s - pool->solvables;
1451   /* find update candidates for 's' */
1452   if (solv->distupgrade)
1453     p = finddistupgradepackages(solv, s, &qs, allow_all);
1454   else
1455     policy_findupdatepackages(solv, s, &qs, allow_all);
1456   d = qs.count ? pool_queuetowhatprovides(pool, &qs) : 0;
1457   queue_free(&qs);
1458   addrule(solv, p, d);  /* allow update of s */
1459   POOL_DEBUG(SAT_DEBUG_SCHUBI, "-----  addupdaterule end -----\n");
1460 }
1461
1462
1463 /********************************************************************/
1464 /* watches */
1465
1466
1467 /*-------------------------------------------------------------------
1468  * makewatches
1469  *
1470  * initial setup for all watches
1471  */
1472
1473 static void
1474 makewatches(Solver *solv)
1475 {
1476   Rule *r;
1477   int i;
1478   int nsolvables = solv->pool->nsolvables;
1479
1480   sat_free(solv->watches);
1481                                        /* lower half for removals, upper half for installs */
1482   solv->watches = sat_calloc(2 * nsolvables, sizeof(Id));
1483 #if 1
1484   /* do it reverse so rpm rules get triggered first (XXX: obsolete?) */
1485   for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
1486 #else
1487   for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
1488 #endif
1489     {
1490       if (!r->w2)               /* assertions do not need watches */
1491         continue;
1492
1493       /* see addwatches_rule(solv, r) */
1494       r->n1 = solv->watches[nsolvables + r->w1];
1495       solv->watches[nsolvables + r->w1] = r - solv->rules;
1496
1497       r->n2 = solv->watches[nsolvables + r->w2];
1498       solv->watches[nsolvables + r->w2] = r - solv->rules;
1499     }
1500 }
1501
1502
1503 /*-------------------------------------------------------------------
1504  *
1505  * add watches (for rule)
1506  * sets up watches for a single rule
1507  *
1508  * see also makewatches()
1509  */
1510
1511 static inline void
1512 addwatches_rule(Solver *solv, Rule *r)
1513 {
1514   int nsolvables = solv->pool->nsolvables;
1515
1516   r->n1 = solv->watches[nsolvables + r->w1];
1517   solv->watches[nsolvables + r->w1] = r - solv->rules;
1518
1519   r->n2 = solv->watches[nsolvables + r->w2];
1520   solv->watches[nsolvables + r->w2] = r - solv->rules;
1521 }
1522
1523
1524 /********************************************************************/
1525 /*
1526  * rule propagation
1527  */
1528
1529
1530 /* shortcuts to check if a literal (positive or negative) assignment
1531  * evaluates to 'true' or 'false'
1532  */
1533 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
1534 #define DECISIONMAP_FALSE(p) ((p) > 0 ? (decisionmap[p] < 0) : (decisionmap[-p] > 0))
1535 #define DECISIONMAP_UNDEF(p) (decisionmap[(p) > 0 ? (p) : -(p)] == 0)
1536
1537 /*-------------------------------------------------------------------
1538  *
1539  * propagate
1540  *
1541  * make decision and propagate to all rules
1542  *
1543  * Evaluate each term affected by the decision (linked through watches)
1544  * If we find unit rules we make new decisions based on them
1545  *
1546  * Everything's fixed there, it's just finding rules that are
1547  * unit.
1548  *
1549  * return : 0 = everything is OK
1550  *          rule = conflict found in this rule
1551  */
1552
1553 static Rule *
1554 propagate(Solver *solv, int level)
1555 {
1556   Pool *pool = solv->pool;
1557   Id *rp, *next_rp;           /* rule pointer, next rule pointer in linked list */
1558   Rule *r;                    /* rule */
1559   Id p, pkg, other_watch;
1560   Id *dp;
1561   Id *decisionmap = solv->decisionmap;
1562
1563   Id *watches = solv->watches + pool->nsolvables;   /* place ptr in middle */
1564
1565   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate -----\n");
1566
1567   /* foreach non-propagated decision */
1568   while (solv->propagate_index < solv->decisionq.count)
1569     {
1570         /*
1571          * 'pkg' was just decided
1572          * negate because our watches trigger if literal goes FALSE
1573          */
1574       pkg = -solv->decisionq.elements[solv->propagate_index++];
1575
1576       IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1577         {
1578           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagate for decision %d level %d\n", -pkg, level);
1579           solver_printruleelement(solv, SAT_DEBUG_PROPAGATE, 0, -pkg);
1580         }
1581
1582       /* foreach rule where 'pkg' is now FALSE */
1583       for (rp = watches + pkg; *rp; rp = next_rp)
1584         {
1585           r = solv->rules + *rp;
1586           if (r->d < 0)
1587             {
1588               /* rule is disabled, goto next */
1589               if (pkg == r->w1)
1590                 next_rp = &r->n1;
1591               else
1592                 next_rp = &r->n2;
1593               continue;
1594             }
1595
1596           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1597             {
1598               POOL_DEBUG(SAT_DEBUG_PROPAGATE,"  watch triggered ");
1599               solver_printrule(solv, SAT_DEBUG_PROPAGATE, r);
1600             }
1601
1602             /* 'pkg' was just decided (was set to FALSE)
1603              *
1604              *  now find other literal watch, check clause
1605              *   and advance on linked list
1606              */
1607           if (pkg == r->w1)
1608             {
1609               other_watch = r->w2;
1610               next_rp = &r->n1;
1611             }
1612           else
1613             {
1614               other_watch = r->w1;
1615               next_rp = &r->n2;
1616             }
1617
1618             /*
1619              * This term is already true (through the other literal)
1620              * so we have nothing to do
1621              */
1622           if (DECISIONMAP_TRUE(other_watch))
1623             continue;
1624
1625             /*
1626              * The other literal is FALSE or UNDEF
1627              *
1628              */
1629
1630           if (r->d)
1631             {
1632               /* Not a binary clause, try to move our watch.
1633                *
1634                * Go over all literals and find one that is
1635                *   not other_watch
1636                *   and not FALSE
1637                *
1638                * (TRUE is also ok, in that case the rule is fulfilled)
1639                */
1640               if (r->p                                /* we have a 'p' */
1641                   && r->p != other_watch              /* which is not watched */
1642                   && !DECISIONMAP_FALSE(r->p))        /* and not FALSE */
1643                 {
1644                   p = r->p;
1645                 }
1646               else                                    /* go find a 'd' to make 'true' */
1647                 {
1648                   /* foreach p in 'd'
1649                      we just iterate sequentially, doing it in another order just changes the order of decisions, not the decisions itself
1650                    */
1651                   for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
1652                     {
1653                       if (p != other_watch              /* which is not watched */
1654                           && !DECISIONMAP_FALSE(p))     /* and not FALSE */
1655                         break;
1656                     }
1657                 }
1658
1659               if (p)
1660                 {
1661                   /*
1662                    * if we found some p that is UNDEF or TRUE, move
1663                    * watch to it
1664                    */
1665                   IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1666                     {
1667                       if (p > 0)
1668                         POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> move w%d to %s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables + p));
1669                       else
1670                         POOL_DEBUG(SAT_DEBUG_PROPAGATE,"    -> move w%d to !%s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables - p));
1671                     }
1672
1673                   *rp = *next_rp;
1674                   next_rp = rp;
1675
1676                   if (pkg == r->w1)
1677                     {
1678                       r->w1 = p;
1679                       r->n1 = watches[p];
1680                     }
1681                   else
1682                     {
1683                       r->w2 = p;
1684                       r->n2 = watches[p];
1685                     }
1686                   watches[p] = r - solv->rules;
1687                   continue;
1688                 }
1689               /* search failed, thus all unwatched literals are FALSE */
1690
1691             } /* not binary */
1692
1693             /*
1694              * unit clause found, set literal other_watch to TRUE
1695              */
1696
1697           if (DECISIONMAP_FALSE(other_watch))      /* check if literal is FALSE */
1698             return r;                              /* eek, a conflict! */
1699
1700           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1701             {
1702               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "   unit ");
1703               solver_printrule(solv, SAT_DEBUG_PROPAGATE, r);
1704             }
1705
1706           if (other_watch > 0)
1707             decisionmap[other_watch] = level;    /* install! */
1708           else
1709             decisionmap[-other_watch] = -level;  /* remove! */
1710
1711           queue_push(&solv->decisionq, other_watch);
1712           queue_push(&solv->decisionq_why, r - solv->rules);
1713
1714           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1715             {
1716               Solvable *s = pool->solvables + (other_watch > 0 ? other_watch : -other_watch);
1717               if (other_watch > 0)
1718                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> decided to install %s\n", solvable2str(pool, s));
1719               else
1720                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> decided to conflict %s\n", solvable2str(pool, s));
1721             }
1722
1723         } /* foreach rule involving 'pkg' */
1724
1725     } /* while we have non-decided decisions */
1726
1727   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate end-----\n");
1728
1729   return 0;     /* all is well */
1730 }
1731
1732
1733 /********************************************************************/
1734 /* Analysis */
1735
1736 /*-------------------------------------------------------------------
1737  *
1738  * analyze
1739  *   and learn
1740  */
1741
1742 static int
1743 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp)
1744 {
1745   Pool *pool = solv->pool;
1746   Queue r;
1747   int rlevel = 1;
1748   Map seen;             /* global? */
1749   Id d, v, vv, *dp, why;
1750   int l, i, idx;
1751   int num = 0, l1num = 0;
1752   int learnt_why = solv->learnt_pool.count;
1753   Id *decisionmap = solv->decisionmap;
1754
1755   queue_init(&r);
1756
1757   POOL_DEBUG(SAT_DEBUG_ANALYZE, "ANALYZE at %d ----------------------\n", level);
1758   map_init(&seen, pool->nsolvables);
1759   idx = solv->decisionq.count;
1760   for (;;)
1761     {
1762       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1763         solver_printruleclass(solv, SAT_DEBUG_ANALYZE, c);
1764       queue_push(&solv->learnt_pool, c - solv->rules);
1765       d = c->d < 0 ? -c->d - 1 : c->d;
1766       dp = d ? pool->whatprovidesdata + d : 0;
1767       /* go through all literals of the rule */
1768       for (i = -1; ; i++)
1769         {
1770           if (i == -1)
1771             v = c->p;
1772           else if (d == 0)
1773             v = i ? 0 : c->w2;
1774           else
1775             v = *dp++;
1776           if (v == 0)
1777             break;
1778
1779           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1780             continue;
1781           vv = v > 0 ? v : -v;
1782           if (MAPTST(&seen, vv))
1783             continue;
1784           l = solv->decisionmap[vv];
1785           if (l < 0)
1786             l = -l;
1787           MAPSET(&seen, vv);
1788           if (l == 1)
1789             l1num++;                    /* need to do this one in level1 pass */
1790           else if (l == level)
1791             num++;                      /* need to do this one as well */
1792           else
1793             {
1794               queue_push(&r, v);        /* not level1 or conflict level, add to new rule */
1795               if (l > rlevel)
1796                 rlevel = l;
1797             }
1798         }
1799 l1retry:
1800       if (!num && !--l1num)
1801         break;  /* all level 1 literals done */
1802       for (;;)
1803         {
1804           assert(idx > 0);
1805           v = solv->decisionq.elements[--idx];
1806           vv = v > 0 ? v : -v;
1807           if (MAPTST(&seen, vv))
1808             break;
1809         }
1810       MAPCLR(&seen, vv);
1811       if (num && --num == 0)
1812         {
1813           *pr = -v;     /* so that v doesn't get lost */
1814           if (!l1num)
1815             break;
1816           POOL_DEBUG(SAT_DEBUG_ANALYZE, "got %d involved level 1 decisions\n", l1num);
1817           for (i = 0; i < r.count; i++)
1818             {
1819               v = r.elements[i];
1820               MAPCLR(&seen, v > 0 ? v : -v);
1821             }
1822           /* only level 1 marks left */
1823           l1num++;
1824           goto l1retry;
1825         }
1826       why = solv->decisionq_why.elements[idx];
1827       if (!why)                 /* just in case, maybe for SYSTEMSOLVABLE */
1828         goto l1retry;
1829       c = solv->rules + why;
1830     }
1831   map_free(&seen);
1832
1833   if (r.count == 0)
1834     *dr = 0;
1835   else if (r.count == 1 && r.elements[0] < 0)
1836     *dr = r.elements[0];
1837   else
1838     *dr = pool_queuetowhatprovides(pool, &r);
1839   IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1840     {
1841       POOL_DEBUG(SAT_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level);
1842       solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, *pr);
1843       for (i = 0; i < r.count; i++)
1844         solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, r.elements[i]);
1845     }
1846   /* push end marker on learnt reasons stack */
1847   queue_push(&solv->learnt_pool, 0);
1848   if (whyp)
1849     *whyp = learnt_why;
1850   solv->stats_learned++;
1851   return rlevel;
1852 }
1853
1854
1855 /*-------------------------------------------------------------------
1856  *
1857  * reset_solver
1858  *
1859  * reset the solver decisions to right after the rpm rules.
1860  * called after rules have been enabled/disabled
1861  */
1862
1863 static void
1864 reset_solver(Solver *solv)
1865 {
1866   Pool *pool = solv->pool;
1867   int i;
1868   Id v;
1869
1870   /* rewind decisions to direct rpm rule assertions */
1871   for (i = solv->decisionq.count - 1; i >= solv->directdecisions; i--)
1872     {
1873       v = solv->decisionq.elements[i];
1874       solv->decisionmap[v > 0 ? v : -v] = 0;
1875     }
1876
1877   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions done reduced from %d to %d\n", solv->decisionq.count, solv->directdecisions);
1878
1879   solv->decisionq_why.count = solv->directdecisions;
1880   solv->decisionq.count = solv->directdecisions;
1881   solv->recommends_index = -1;
1882   solv->propagate_index = 0;
1883
1884   /* adapt learnt rule status to new set of enabled/disabled rules */
1885   enabledisablelearntrules(solv);
1886
1887   /* redo all job/update decisions */
1888   makeruledecisions(solv);
1889   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count);
1890 }
1891
1892
1893 /*-------------------------------------------------------------------
1894  *
1895  * analyze_unsolvable_rule
1896  */
1897
1898 static void
1899 analyze_unsolvable_rule(Solver *solv, Rule *r, Id *lastweakp)
1900 {
1901   Pool *pool = solv->pool;
1902   int i;
1903   Id why = r - solv->rules;
1904
1905   IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE)
1906     solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
1907   if (solv->learntrules && why >= solv->learntrules)
1908     {
1909       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1910         if (solv->learnt_pool.elements[i] > 0)
1911           analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], lastweakp);
1912       return;
1913     }
1914   if (MAPTST(&solv->weakrulemap, why))
1915     if (!*lastweakp || why > *lastweakp)
1916       *lastweakp = why;
1917   /* do not add rpm rules to problem */
1918   if (why < solv->rpmrules_end)
1919     return;
1920   /* turn rule into problem */
1921   if (why >= solv->jobrules && why < solv->jobrules_end)
1922     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
1923   /* return if problem already countains our rule */
1924   if (solv->problems.count)
1925     {
1926       for (i = solv->problems.count - 1; i >= 0; i--)
1927         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
1928           break;
1929         else if (solv->problems.elements[i] == why)
1930           return;
1931     }
1932   queue_push(&solv->problems, why);
1933 }
1934
1935
1936 /*-------------------------------------------------------------------
1937  *
1938  * analyze_unsolvable
1939  *
1940  * return: 1 - disabled some rules, try again
1941  *         0 - hopeless
1942  */
1943
1944 static int
1945 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
1946 {
1947   Pool *pool = solv->pool;
1948   Rule *r;
1949   Map seen;             /* global to speed things up? */
1950   Id d, v, vv, *dp, why;
1951   int l, i, idx;
1952   Id *decisionmap = solv->decisionmap;
1953   int oldproblemcount;
1954   int oldlearntpoolcount;
1955   Id lastweak;
1956
1957   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n");
1958   solv->stats_unsolvable++;
1959   oldproblemcount = solv->problems.count;
1960   oldlearntpoolcount = solv->learnt_pool.count;
1961
1962   /* make room for proof index */
1963   /* must update it later, as analyze_unsolvable_rule would confuse
1964    * it with a rule index if we put the real value in already */
1965   queue_push(&solv->problems, 0);
1966
1967   r = cr;
1968   map_init(&seen, pool->nsolvables);
1969   queue_push(&solv->learnt_pool, r - solv->rules);
1970   lastweak = 0;
1971   analyze_unsolvable_rule(solv, r, &lastweak);
1972   d = r->d < 0 ? -r->d - 1 : r->d;
1973   dp = d ? pool->whatprovidesdata + d : 0;
1974   for (i = -1; ; i++)
1975     {
1976       if (i == -1)
1977         v = r->p;
1978       else if (d == 0)
1979         v = i ? 0 : r->w2;
1980       else
1981         v = *dp++;
1982       if (v == 0)
1983         break;
1984       if (DECISIONMAP_TRUE(v))  /* the one true literal */
1985           continue;
1986       vv = v > 0 ? v : -v;
1987       l = solv->decisionmap[vv];
1988       if (l < 0)
1989         l = -l;
1990       MAPSET(&seen, vv);
1991     }
1992   idx = solv->decisionq.count;
1993   while (idx > 0)
1994     {
1995       v = solv->decisionq.elements[--idx];
1996       vv = v > 0 ? v : -v;
1997       if (!MAPTST(&seen, vv))
1998         continue;
1999       why = solv->decisionq_why.elements[idx];
2000       queue_push(&solv->learnt_pool, why);
2001       r = solv->rules + why;
2002       analyze_unsolvable_rule(solv, r, &lastweak);
2003       d = r->d < 0 ? -r->d - 1 : r->d;
2004       dp = d ? pool->whatprovidesdata + d : 0;
2005       for (i = -1; ; i++)
2006         {
2007           if (i == -1)
2008             v = r->p;
2009           else if (d == 0)
2010             v = i ? 0 : r->w2;
2011           else
2012             v = *dp++;
2013           if (v == 0)
2014             break;
2015           if (DECISIONMAP_TRUE(v))      /* the one true literal */
2016               continue;
2017           vv = v > 0 ? v : -v;
2018           l = solv->decisionmap[vv];
2019           if (l < 0)
2020             l = -l;
2021           MAPSET(&seen, vv);
2022         }
2023     }
2024   map_free(&seen);
2025   queue_push(&solv->problems, 0);       /* mark end of this problem */
2026
2027   if (lastweak)
2028     {
2029       /* disable last weak rule */
2030       solv->problems.count = oldproblemcount;
2031       solv->learnt_pool.count = oldlearntpoolcount;
2032       r = solv->rules + lastweak;
2033       POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling ");
2034       solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
2035       disablerule(solv, r);
2036       reset_solver(solv);
2037       return 1;
2038     }
2039
2040   /* finish proof */
2041   queue_push(&solv->learnt_pool, 0);
2042   solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
2043
2044   if (disablerules)
2045     {
2046       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
2047         disableproblem(solv, solv->problems.elements[i]);
2048       /* XXX: might want to enable all weak rules again */
2049       reset_solver(solv);
2050       return 1;
2051     }
2052   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "UNSOLVABLE\n");
2053   return 0;
2054 }
2055
2056
2057 /********************************************************************/
2058 /* Decision revert */
2059
2060 /*-------------------------------------------------------------------
2061  *
2062  * revert
2063  * revert decision at level
2064  */
2065
2066 static void
2067 revert(Solver *solv, int level)
2068 {
2069   Pool *pool = solv->pool;
2070   Id v, vv;
2071   while (solv->decisionq.count)
2072     {
2073       v = solv->decisionq.elements[solv->decisionq.count - 1];
2074       vv = v > 0 ? v : -v;
2075       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
2076         break;
2077       POOL_DEBUG(SAT_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
2078       if (v > 0 && solv->recommendations.count && v == solv->recommendations.elements[solv->recommendations.count - 1])
2079         solv->recommendations.count--;
2080       solv->decisionmap[vv] = 0;
2081       solv->decisionq.count--;
2082       solv->decisionq_why.count--;
2083       solv->propagate_index = solv->decisionq.count;
2084     }
2085   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
2086     {
2087       solv->branches.count--;
2088       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
2089         solv->branches.count--;
2090     }
2091   solv->recommends_index = -1;
2092 }
2093
2094
2095 /*-------------------------------------------------------------------
2096  *
2097  * watch2onhighest - put watch2 on literal with highest level
2098  */
2099
2100 static inline void
2101 watch2onhighest(Solver *solv, Rule *r)
2102 {
2103   int l, wl = 0;
2104   Id d, v, *dp;
2105
2106   d = r->d < 0 ? -r->d - 1 : r->d;
2107   if (!d)
2108     return;     /* binary rule, both watches are set */
2109   dp = solv->pool->whatprovidesdata + d;
2110   while ((v = *dp++) != 0)
2111     {
2112       l = solv->decisionmap[v < 0 ? -v : v];
2113       if (l < 0)
2114         l = -l;
2115       if (l > wl)
2116         {
2117           r->w2 = dp[-1];
2118           wl = l;
2119         }
2120     }
2121 }
2122
2123
2124 /*-------------------------------------------------------------------
2125  *
2126  * setpropagatelearn
2127  *
2128  * add free decision (solvable to install) to decisionq
2129  * increase level and propagate decision
2130  * return if no conflict.
2131  *
2132  * in conflict case, analyze conflict rule, add resulting
2133  * rule to learnt rule set, make decision from learnt
2134  * rule (always unit) and re-propagate.
2135  *
2136  * returns the new solver level or 0 if unsolvable
2137  *
2138  */
2139
2140 static int
2141 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
2142 {
2143   Pool *pool = solv->pool;
2144   Rule *r;
2145   Id p = 0, d = 0;
2146   int l, why;
2147
2148   if (decision)
2149     {
2150       level++;
2151       if (decision > 0)
2152         solv->decisionmap[decision] = level;
2153       else
2154         solv->decisionmap[-decision] = -level;
2155       queue_push(&solv->decisionq, decision);
2156       queue_push(&solv->decisionq_why, 0);
2157     }
2158   for (;;)
2159     {
2160       r = propagate(solv, level);
2161       if (!r)
2162         break;
2163       if (level == 1)
2164         return analyze_unsolvable(solv, r, disablerules);
2165       POOL_DEBUG(SAT_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules));
2166       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
2167       assert(l > 0 && l < level);
2168       POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l);
2169       level = l;
2170       revert(solv, level);
2171       r = addrule(solv, p, d);       /* p requires d */
2172       assert(r);
2173       assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules);
2174       queue_push(&solv->learnt_why, why);
2175       if (d)
2176         {
2177           /* at least 2 literals, needs watches */
2178           watch2onhighest(solv, r);
2179           addwatches_rule(solv, r);
2180         }
2181       else
2182         {
2183           /* learnt rule is an assertion */
2184           queue_push(&solv->ruleassertions, r - solv->rules);
2185         }
2186       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
2187       queue_push(&solv->decisionq, p);
2188       queue_push(&solv->decisionq_why, r - solv->rules);
2189       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
2190         {
2191           POOL_DEBUG(SAT_DEBUG_ANALYZE, "decision: ");
2192           solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, p);
2193           POOL_DEBUG(SAT_DEBUG_ANALYZE, "new rule: ");
2194           solver_printrule(solv, SAT_DEBUG_ANALYZE, r);
2195         }
2196     }
2197   return level;
2198 }
2199
2200
2201 /*-------------------------------------------------------------------
2202  *
2203  * select and install
2204  *
2205  * install best package from the queue. We add an extra package, inst, if
2206  * provided. See comment in weak install section.
2207  *
2208  * returns the new solver level or 0 if unsolvable
2209  *
2210  */
2211
2212 static int
2213 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
2214 {
2215   Pool *pool = solv->pool;
2216   Id p;
2217   int i;
2218
2219   if (dq->count > 1 || inst)
2220     policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
2221
2222   i = 0;
2223   if (dq->count > 1)
2224     {
2225       /* choose the supplemented one */
2226       for (i = 0; i < dq->count; i++)
2227         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
2228           break;
2229       if (i == dq->count)
2230         {
2231           for (i = 1; i < dq->count; i++)
2232             queue_push(&solv->branches, dq->elements[i]);
2233           queue_push(&solv->branches, -level);
2234           i = 0;
2235         }
2236     }
2237   p = dq->elements[i];
2238
2239   POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvable2str(pool, pool->solvables + p));
2240
2241   return setpropagatelearn(solv, level, p, disablerules);
2242 }
2243
2244
2245 /********************************************************************/
2246 /* Main solver interface */
2247
2248
2249 /*-------------------------------------------------------------------
2250  *
2251  * solver_create
2252  * create solver structure
2253  *
2254  * pool: all available solvables
2255  * installed: installed Solvables
2256  *
2257  *
2258  * Upon solving, rules are created to flag the Solvables
2259  * of the 'installed' Repo as installed.
2260  */
2261
2262 Solver *
2263 solver_create(Pool *pool, Repo *installed)
2264 {
2265   Solver *solv;
2266   solv = (Solver *)sat_calloc(1, sizeof(Solver));
2267   solv->pool = pool;
2268   solv->installed = installed;
2269
2270   queue_init(&solv->ruletojob);
2271   queue_init(&solv->decisionq);
2272   queue_init(&solv->decisionq_why);
2273   queue_init(&solv->problems);
2274   queue_init(&solv->suggestions);
2275   queue_init(&solv->recommendations);
2276   queue_init(&solv->orphaned);
2277   queue_init(&solv->learnt_why);
2278   queue_init(&solv->learnt_pool);
2279   queue_init(&solv->branches);
2280   queue_init(&solv->covenantq);
2281   queue_init(&solv->weakruleq);
2282   queue_init(&solv->ruleassertions);
2283
2284   map_init(&solv->recommendsmap, pool->nsolvables);
2285   map_init(&solv->suggestsmap, pool->nsolvables);
2286   map_init(&solv->noupdate, installed ? installed->end - installed->start : 0);
2287   solv->recommends_index = 0;
2288
2289   solv->decisionmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
2290   solv->nrules = 1;
2291   solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
2292   memset(solv->rules, 0, sizeof(Rule));
2293
2294   return solv;
2295 }
2296
2297
2298 /*-------------------------------------------------------------------
2299  *
2300  * solver_free
2301  */
2302
2303 void
2304 solver_free(Solver *solv)
2305 {
2306   queue_free(&solv->ruletojob);
2307   queue_free(&solv->decisionq);
2308   queue_free(&solv->decisionq_why);
2309   queue_free(&solv->learnt_why);
2310   queue_free(&solv->learnt_pool);
2311   queue_free(&solv->problems);
2312   queue_free(&solv->suggestions);
2313   queue_free(&solv->recommendations);
2314   queue_free(&solv->orphaned);
2315   queue_free(&solv->branches);
2316   queue_free(&solv->covenantq);
2317   queue_free(&solv->weakruleq);
2318   queue_free(&solv->ruleassertions);
2319
2320   map_free(&solv->recommendsmap);
2321   map_free(&solv->suggestsmap);
2322   map_free(&solv->noupdate);
2323   map_free(&solv->weakrulemap);
2324   map_free(&solv->noobsoletes);
2325
2326   sat_free(solv->decisionmap);
2327   sat_free(solv->rules);
2328   sat_free(solv->watches);
2329   sat_free(solv->obsoletes);
2330   sat_free(solv->obsoletes_data);
2331   sat_free(solv);
2332 }
2333
2334
2335 /*-------------------------------------------------------------------
2336  *
2337  * run_solver
2338  *
2339  * all rules have been set up, now actually run the solver
2340  *
2341  */
2342
2343 static void
2344 run_solver(Solver *solv, int disablerules, int doweak)
2345 {
2346   Queue dq;             /* local decisionqueue */
2347   Queue dqs;            /* local decisionqueue for supplements */
2348   int systemlevel;
2349   int level, olevel;
2350   Rule *r;
2351   int i, j, n;
2352   Solvable *s;
2353   Pool *pool = solv->pool;
2354   Id p, *dp;
2355
2356   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
2357     {
2358       POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
2359       for (i = 1; i < solv->nrules; i++)
2360         solver_printruleclass(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
2361     }
2362
2363   POOL_DEBUG(SAT_DEBUG_STATS, "initial decisions: %d\n", solv->decisionq.count);
2364
2365   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2366     solver_printdecisions(solv);
2367
2368   /* start SAT algorithm */
2369   level = 1;
2370   systemlevel = level + 1;
2371   POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n");
2372
2373   queue_init(&dq);
2374   queue_init(&dqs);
2375
2376   /*
2377    * here's the main loop:
2378    * 1) propagate new decisions (only needed for level 1)
2379    * 2) try to keep installed packages
2380    * 3) fulfill all unresolved rules
2381    * 4) install recommended packages
2382    * 5) minimalize solution if we had choices
2383    * if we encounter a problem, we rewind to a safe level and restart
2384    * with step 1
2385    */
2386
2387   for (;;)
2388     {
2389       /*
2390        * propagate
2391        */
2392
2393       if (level == 1)
2394         {
2395           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
2396           if ((r = propagate(solv, level)) != 0)
2397             {
2398               if (analyze_unsolvable(solv, r, disablerules))
2399                 continue;
2400               queue_free(&dq);
2401               return;
2402             }
2403         }
2404
2405      if (level < systemlevel)
2406         {
2407           POOL_DEBUG(SAT_DEBUG_STATS, "resolving job rules\n");
2408           for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
2409             {
2410               Id l;
2411               if (r->d < 0)             /* ignore disabled rules */
2412                 continue;
2413               queue_empty(&dq);
2414               FOR_RULELITERALS(l, dp, r)
2415                 {
2416                   if (l < 0)
2417                     {
2418                       if (solv->decisionmap[-l] <= 0)
2419                         break;
2420                     }
2421                   else
2422                     {
2423                       if (solv->decisionmap[l] > 0)
2424                         break;
2425                       if (solv->decisionmap[l] == 0)
2426                         queue_push(&dq, l);
2427                     }
2428                 }
2429               if (l || !dq.count)
2430                 continue;
2431               /* prune to installed if not updating */
2432               if (!solv->updatesystem && solv->installed && dq.count > 1)
2433                 {
2434                   int j, k;
2435                   for (j = k = 0; j < dq.count; j++)
2436                     {
2437                       Solvable *s = pool->solvables + dq.elements[j];
2438                       if (s->repo == solv->installed)
2439                         dq.elements[k++] = dq.elements[j];
2440                     }
2441                   if (k)
2442                     dq.count = k;
2443                 }
2444               olevel = level;
2445               level = selectandinstall(solv, level, &dq, 0, disablerules);
2446               if (level == 0)
2447                 {
2448                   queue_free(&dq);
2449                   return;
2450                 }
2451               if (level <= olevel)
2452                 break;
2453             }
2454           systemlevel = level + 1;
2455           if (i < solv->jobrules_end)
2456             continue;
2457         }
2458
2459
2460       /*
2461        * installed packages
2462        */
2463
2464       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
2465         {
2466           if (!solv->updatesystem)
2467             {
2468               /*
2469                * Normal run (non-updating)
2470                * Keep as many packages installed as possible
2471                */
2472               POOL_DEBUG(SAT_DEBUG_STATS, "installing old packages\n");
2473
2474               for (i = solv->installed->start; i < solv->installed->end; i++)
2475                 {
2476                   s = pool->solvables + i;
2477
2478                     /* skip if not installed */
2479                   if (s->repo != solv->installed)
2480                     continue;
2481
2482                     /* skip if already decided */
2483                   if (solv->decisionmap[i] != 0)
2484                     continue;
2485
2486                   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "keeping %s\n", solvable2str(pool, s));
2487
2488                   olevel = level;
2489                   level = setpropagatelearn(solv, level, i, disablerules);
2490
2491                   if (level == 0)                /* unsolvable */
2492                     {
2493                       queue_free(&dq);
2494                       return;
2495                     }
2496                   if (level <= olevel)
2497                     break;
2498                 }
2499               if (i < solv->installed->end)
2500                 continue;
2501             }
2502
2503           POOL_DEBUG(SAT_DEBUG_STATS, "resolving update/feature rules\n");
2504
2505           for (i = solv->installed->start, r = solv->rules + solv->updaterules; i < solv->installed->end; i++, r++)
2506             {
2507               Rule *rr;
2508               Id inst;
2509               s = pool->solvables + i;
2510
2511                 /* skip if not installed (can't update) */
2512               if (s->repo != solv->installed)
2513                 continue;
2514                 /* skip if already decided */
2515               if (solv->decisionmap[i] > 0)
2516                 continue;
2517
2518                 /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2519               if (MAPTST(&solv->noupdate, i - solv->installed->start))
2520                 continue;
2521
2522               queue_empty(&dq);
2523
2524               rr = r;
2525               if (rr->d < 0)    /* disabled -> look at feature rule ? */
2526                 rr -= solv->installed->end - solv->installed->start;
2527               if (!rr->p)       /* identical to update rule? */
2528                 rr = r;
2529               if (rr->p <= 0)
2530                 continue;
2531
2532               FOR_RULELITERALS(p, dp, rr)
2533                 {
2534                   if (solv->decisionmap[p] > 0)
2535                     break;
2536                   if (solv->decisionmap[p] == 0)
2537                     queue_push(&dq, p);
2538                 }
2539               if (p || !dq.count)       /* already fulfilled or empty */
2540                 continue;
2541               if (dq.elements[0] == i)
2542                 inst = queue_shift(&dq);
2543               else
2544                 inst = 0;
2545               olevel = level;
2546               /* FIXME: it is handled a bit different because we do not want
2547                * to have it pruned just because it is not recommened.
2548                * we should not prune installed packages instead.
2549                */
2550               level = selectandinstall(solv, level, &dq, inst, disablerules);
2551               if (level == 0)
2552                 {
2553                   queue_free(&dq);
2554                   return;
2555                 }
2556               if (level <= olevel)
2557                 break;
2558             }
2559           systemlevel = level + 1;
2560           if (i < solv->installed->end)
2561             continue;
2562         }
2563
2564       if (level < systemlevel)
2565         systemlevel = level;
2566
2567       /*
2568        * decide
2569        */
2570
2571       POOL_DEBUG(SAT_DEBUG_STATS, "deciding unresolved rules\n");
2572       for (i = 1, n = 1; ; i++, n++)
2573         {
2574           if (n == solv->nrules)
2575             break;
2576           if (i == solv->nrules)
2577             i = 1;
2578           r = solv->rules + i;
2579           if (r->d < 0)         /* ignore disabled rules */
2580             continue;
2581           queue_empty(&dq);
2582           if (r->d == 0)
2583             {
2584               /* binary or unary rule */
2585               /* need two positive undecided literals */
2586               if (r->p < 0 || r->w2 <= 0)
2587                 continue;
2588               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2589                 continue;
2590               queue_push(&dq, r->p);
2591               queue_push(&dq, r->w2);
2592             }
2593           else
2594             {
2595               /* make sure that
2596                * all negative literals are installed
2597                * no positive literal is installed
2598                * i.e. the rule is not fulfilled and we
2599                * just need to decide on the positive literals
2600                */
2601               if (r->p < 0)
2602                 {
2603                   if (solv->decisionmap[-r->p] <= 0)
2604                     continue;
2605                 }
2606               else
2607                 {
2608                   if (solv->decisionmap[r->p] > 0)
2609                     continue;
2610                   if (solv->decisionmap[r->p] == 0)
2611                     queue_push(&dq, r->p);
2612                 }
2613               dp = pool->whatprovidesdata + r->d;
2614               while ((p = *dp++) != 0)
2615                 {
2616                   if (p < 0)
2617                     {
2618                       if (solv->decisionmap[-p] <= 0)
2619                         break;
2620                     }
2621                   else
2622                     {
2623                       if (solv->decisionmap[p] > 0)
2624                         break;
2625                       if (solv->decisionmap[p] == 0)
2626                         queue_push(&dq, p);
2627                     }
2628                 }
2629               if (p)
2630                 continue;
2631             }
2632           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
2633             {
2634               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
2635               solver_printruleclass(solv, SAT_DEBUG_PROPAGATE, r);
2636             }
2637           /* dq.count < 2 cannot happen as this means that
2638            * the rule is unit */
2639           assert(dq.count > 1);
2640
2641           olevel = level;
2642           level = selectandinstall(solv, level, &dq, 0, disablerules);
2643           if (level == 0)
2644             {
2645               queue_free(&dq);
2646               return;
2647             }
2648           if (level < systemlevel)
2649             break;
2650           n = 0;
2651         } /* for(), decide */
2652
2653       if (n != solv->nrules)    /* continue if level < systemlevel */
2654         continue;
2655
2656       if (doweak)
2657         {
2658           int qcount;
2659
2660           POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended packages\n");
2661           queue_empty(&dq);
2662           queue_empty(&dqs);
2663           for (i = 1; i < pool->nsolvables; i++)
2664             {
2665               if (solv->decisionmap[i] < 0)
2666                 continue;
2667               if (solv->decisionmap[i] > 0)
2668                 {
2669                   /* installed, check for recommends */
2670                   Id *recp, rec, *pp, p;
2671                   s = pool->solvables + i;
2672                   if (solv->ignorealreadyrecommended && s->repo == solv->installed)
2673                     continue;
2674                   /* XXX need to special case AND ? */
2675                   if (s->recommends)
2676                     {
2677                       recp = s->repo->idarraydata + s->recommends;
2678                       while ((rec = *recp++) != 0)
2679                         {
2680                           qcount = dq.count;
2681                           FOR_PROVIDES(p, pp, rec)
2682                             {
2683                               if (solv->decisionmap[p] > 0)
2684                                 {
2685                                   dq.count = qcount;
2686                                   break;
2687                                 }
2688                               else if (solv->decisionmap[p] == 0)
2689                                 {
2690                                   queue_pushunique(&dq, p);
2691                                 }
2692                             }
2693                         }
2694                     }
2695                 }
2696               else
2697                 {
2698                   s = pool->solvables + i;
2699                   if (!s->supplements)
2700                     continue;
2701                   if (!pool_installable(pool, s))
2702                     continue;
2703                   if (!solver_is_supplementing(solv, s))
2704                     continue;
2705                   if (solv->ignorealreadyrecommended && solv->installed)
2706                     queue_pushunique(&dqs, i);  /* needs filter */
2707                   else
2708                     queue_pushunique(&dq, i);
2709                 }
2710             }
2711           if (solv->ignorealreadyrecommended && dqs.count)
2712             {
2713               /* turn off all new packages */
2714               for (i = 0; i < solv->decisionq.count; i++)
2715                 {
2716                   p = solv->decisionq.elements[i];
2717                   if (p < 0)
2718                     continue;
2719                   s = pool->solvables + p;
2720                   if (s->repo && s->repo != solv->installed)
2721                     solv->decisionmap[p] = -solv->decisionmap[p];
2722                 }
2723               /* filter out old supplements */
2724               for (i = 0; i < dqs.count; i++)
2725                 {
2726                   p = dqs.elements[i];
2727                   s = pool->solvables + p;
2728                   if (!s->supplements)
2729                     continue;
2730                   if (!solver_is_supplementing(solv, s))
2731                     queue_pushunique(&dq, p);
2732                 }
2733               /* undo turning off */
2734               for (i = 0; i < solv->decisionq.count; i++)
2735                 {
2736                   p = solv->decisionq.elements[i];
2737                   if (p < 0)
2738                     continue;
2739                   s = pool->solvables + p;
2740                   if (s->repo && s->repo != solv->installed)
2741                     solv->decisionmap[p] = -solv->decisionmap[p];
2742                 }
2743             }
2744           if (dq.count)
2745             {
2746               if (dq.count > 1)
2747                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2748               p = dq.elements[0];
2749               POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2750               queue_push(&solv->recommendations, p);
2751               level = setpropagatelearn(solv, level, p, 0);
2752               continue;
2753             }
2754         }
2755
2756      if (solv->distupgrade && solv->installed)
2757         {
2758           /* let's see if we can install some unsupported package */
2759           int ri;
2760           POOL_DEBUG(SAT_DEBUG_STATS, "deciding unsupported packages\n");
2761           for (i = solv->installed->start, ri = 0; i < solv->installed->end; i++, ri++)
2762             {
2763               s = pool->solvables + i;
2764               if (s->repo != solv->installed)
2765                 continue;
2766               if (solv->decisionmap[i])
2767                 continue;
2768               if (!solv->rules[solv->updaterules + ri].p && !solv->rules[solv->featurerules + ri].p)
2769                 break;
2770             }
2771           if (i < solv->installed->end)
2772             {
2773               if (solv->distupgrade_removeunsupported)
2774                 {
2775                   POOL_DEBUG(SAT_DEBUG_STATS, "removing unsupported %s\n", solvable2str(pool, pool->solvables + i));
2776                   level = setpropagatelearn(solv, level, -i, 0);
2777                 }
2778               else
2779                 {
2780                   POOL_DEBUG(SAT_DEBUG_STATS, "keeping unsupported %s\n", solvable2str(pool, pool->solvables + i));
2781                   level = setpropagatelearn(solv, level, i, 0);
2782                 }
2783               continue;
2784             }
2785         }
2786
2787      if (solv->solution_callback)
2788         {
2789           solv->solution_callback(solv, solv->solution_callback_data);
2790           if (solv->branches.count)
2791             {
2792               int i = solv->branches.count - 1;
2793               int l = -solv->branches.elements[i];
2794               for (; i > 0; i--)
2795                 if (solv->branches.elements[i - 1] < 0)
2796                   break;
2797               p = solv->branches.elements[i];
2798               POOL_DEBUG(SAT_DEBUG_STATS, "branching with %s\n", solvable2str(pool, pool->solvables + p));
2799               queue_empty(&dq);
2800               for (j = i + 1; j < solv->branches.count; j++)
2801                 queue_push(&dq, solv->branches.elements[j]);
2802               solv->branches.count = i;
2803               level = l;
2804               revert(solv, level);
2805               if (dq.count > 1)
2806                 for (j = 0; j < dq.count; j++)
2807                   queue_push(&solv->branches, dq.elements[j]);
2808               olevel = level;
2809               level = setpropagatelearn(solv, level, p, disablerules);
2810               if (level == 0)
2811                 {
2812                   queue_free(&dq);
2813                   return;
2814                 }
2815               continue;
2816             }
2817           /* all branches done, we're finally finished */
2818           break;
2819         }
2820
2821       /* minimization step */
2822      if (solv->branches.count)
2823         {
2824           int l = 0, lasti = -1, lastl = -1;
2825           p = 0;
2826           for (i = solv->branches.count - 1; i >= 0; i--)
2827             {
2828               p = solv->branches.elements[i];
2829               if (p < 0)
2830                 l = -p;
2831               else if (p > 0 && solv->decisionmap[p] > l + 1)
2832                 {
2833                   lasti = i;
2834                   lastl = l;
2835                 }
2836             }
2837           if (lasti >= 0)
2838             {
2839               /* kill old solvable so that we do not loop */
2840               p = solv->branches.elements[lasti];
2841               solv->branches.elements[lasti] = 0;
2842               POOL_DEBUG(SAT_DEBUG_STATS, "minimizing %d -> %d with %s\n", solv->decisionmap[p], l, solvable2str(pool, pool->solvables + p));
2843
2844               level = lastl;
2845               revert(solv, level);
2846               olevel = level;
2847               level = setpropagatelearn(solv, level, p, disablerules);
2848               if (level == 0)
2849                 {
2850                   queue_free(&dq);
2851                   return;
2852                 }
2853               continue;
2854             }
2855         }
2856       break;
2857     }
2858   POOL_DEBUG(SAT_DEBUG_STATS, "solver statistics: %d learned rules, %d unsolvable\n", solv->stats_learned, solv->stats_unsolvable);
2859
2860   POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
2861   queue_free(&dq);
2862   queue_free(&dqs);
2863 }
2864
2865
2866 /*-------------------------------------------------------------------
2867  *
2868  * refine_suggestion
2869  *
2870  * at this point, all rules that led to conflicts are disabled.
2871  * we re-enable all rules of a problem set but rule "sug", then
2872  * continue to disable more rules until there as again a solution.
2873  */
2874
2875 /* FIXME: think about conflicting assertions */
2876
2877 static void
2878 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2879 {
2880   Pool *pool = solv->pool;
2881   int i, j;
2882   Id v;
2883   Queue disabled;
2884   int disabledcnt;
2885
2886   IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2887     {
2888       POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
2889       for (i = 0; problem[i]; i++)
2890         {
2891           if (problem[i] == sug)
2892             POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
2893           solver_printproblem(solv, problem[i]);
2894         }
2895     }
2896   queue_init(&disabled);
2897   queue_empty(refined);
2898   queue_push(refined, sug);
2899
2900   /* re-enable all problem rules with the exception of "sug"(gestion) */
2901   revert(solv, 1);
2902   reset_solver(solv);
2903
2904   for (i = 0; problem[i]; i++)
2905     if (problem[i] != sug)
2906       enableproblem(solv, problem[i]);
2907
2908   if (sug < 0)
2909     disableupdaterules(solv, job, -(sug + 1));
2910   else if (sug >= solv->updaterules && sug < solv->updaterules_end)
2911     {
2912       /* enable feature rule */
2913       Rule *r = solv->rules + solv->featurerules + (sug - solv->updaterules);
2914       if (r->p)
2915         enablerule(solv, r);
2916     }
2917
2918   enableweakrules(solv);
2919
2920   for (;;)
2921     {
2922       int njob, nfeature, nupdate;
2923       queue_empty(&solv->problems);
2924       revert(solv, 1);          /* XXX no longer needed? */
2925       reset_solver(solv);
2926
2927       if (!solv->problems.count)
2928         run_solver(solv, 0, 0);
2929
2930       if (!solv->problems.count)
2931         {
2932           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
2933           IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2934             solver_printdecisions(solv);
2935           break;                /* great, no more problems */
2936         }
2937       disabledcnt = disabled.count;
2938       /* start with 1 to skip over proof index */
2939       njob = nfeature = nupdate = 0;
2940       for (i = 1; i < solv->problems.count - 1; i++)
2941         {
2942           /* ignore solutions in refined */
2943           v = solv->problems.elements[i];
2944           if (v == 0)
2945             break;      /* end of problem reached */
2946           for (j = 0; problem[j]; j++)
2947             if (problem[j] != sug && problem[j] == v)
2948               break;
2949           if (problem[j])
2950             continue;
2951           if (v >= solv->featurerules && v < solv->featurerules_end)
2952             nfeature++;
2953           else if (v > 0)
2954             nupdate++;
2955           else
2956             njob++;
2957           queue_push(&disabled, v);
2958         }
2959       if (disabled.count == disabledcnt)
2960         {
2961           /* no solution found, this was an invalid suggestion! */
2962           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
2963           refined->count = 0;
2964           break;
2965         }
2966       if (!njob && nupdate && nfeature)
2967         {
2968           /* got only update rules, filter out feature rules */
2969           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "throwing away feature rules\n");
2970           for (i = j = disabledcnt; i < disabled.count; i++)
2971             {
2972               v = disabled.elements[i];
2973               if (v < solv->featurerules || v >= solv->featurerules_end)
2974                 disabled.elements[j++] = v;
2975             }
2976           disabled.count = j;
2977           nfeature = 0;
2978         }
2979       if (disabled.count == disabledcnt + 1)
2980         {
2981           /* just one suggestion, add it to refined list */
2982           v = disabled.elements[disabledcnt];
2983           if (!nfeature)
2984             queue_push(refined, v);     /* do not record feature rules */
2985           disableproblem(solv, v);
2986           if (v >= solv->updaterules && v < solv->updaterules_end)
2987             {
2988               Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
2989               if (r->p)
2990                 enablerule(solv, r);    /* enable corresponding feature rule */
2991             }
2992           if (v < 0)
2993             disableupdaterules(solv, job, -(v + 1));
2994         }
2995       else
2996         {
2997           /* more than one solution, disable all */
2998           /* do not push anything on refine list, as we do not know which solution to choose */
2999           /* thus, the user will get another problem if he selects this solution, where he
3000            * can choose the right one */
3001           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
3002             {
3003               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
3004               for (i = disabledcnt; i < disabled.count; i++)
3005                 solver_printproblem(solv, disabled.elements[i]);
3006             }
3007           for (i = disabledcnt; i < disabled.count; i++)
3008             {
3009               v = disabled.elements[i];
3010               disableproblem(solv, v);
3011               if (v >= solv->updaterules && v < solv->updaterules_end)
3012                 {
3013                   Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
3014                   if (r->p)
3015                     enablerule(solv, r);
3016                 }
3017             }
3018         }
3019     }
3020   /* all done, get us back into the same state as before */
3021   /* enable refined rules again */
3022   for (i = 0; i < disabled.count; i++)
3023     enableproblem(solv, disabled.elements[i]);
3024   /* disable problem rules again */
3025
3026   /* FIXME! */
3027   for (i = 0; problem[i]; i++)
3028     enableproblem(solv, problem[i]);
3029   disableupdaterules(solv, job, -1);
3030
3031   /* disable problem rules again */
3032   for (i = 0; problem[i]; i++)
3033     disableproblem(solv, problem[i]);
3034   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
3035 }
3036
3037
3038 /*-------------------------------------------------------------------
3039  * sorting helper for problems
3040  */
3041
3042 static int
3043 problems_sortcmp(const void *ap, const void *bp)
3044 {
3045   Id a = *(Id *)ap, b = *(Id *)bp;
3046   if (a < 0 && b > 0)
3047     return 1;
3048   if (a > 0 && b < 0)
3049     return -1;
3050   return a - b;
3051 }
3052
3053
3054 /*-------------------------------------------------------------------
3055  * sort problems
3056  */
3057
3058 static void
3059 problems_sort(Solver *solv)
3060 {
3061   int i, j;
3062   if (!solv->problems.count)
3063     return;
3064   for (i = j = 1; i < solv->problems.count; i++)
3065     {
3066       if (!solv->problems.elements[i])
3067         {
3068           if (i > j + 1)
3069             qsort(solv->problems.elements + j, i - j, sizeof(Id), problems_sortcmp);
3070           if (++i == solv->problems.count)
3071             break;
3072           j = i + 1;
3073         }
3074     }
3075 }
3076
3077
3078 /*-------------------------------------------------------------------
3079  * convert problems to solutions
3080  */
3081
3082 static void
3083 problems_to_solutions(Solver *solv, Queue *job)
3084 {
3085   Pool *pool = solv->pool;
3086   Queue problems;
3087   Queue solution;
3088   Queue solutions;
3089   Id *problem;
3090   Id why;
3091   int i, j, nsol;
3092
3093   if (!solv->problems.count)
3094     return;
3095   problems_sort(solv);
3096   queue_clone(&problems, &solv->problems);
3097   queue_init(&solution);
3098   queue_init(&solutions);
3099   /* copy over proof index */
3100   queue_push(&solutions, problems.elements[0]);
3101   problem = problems.elements + 1;
3102   for (i = 1; i < problems.count; i++)
3103     {
3104       Id v = problems.elements[i];
3105       if (v == 0)
3106         {
3107           /* mark end of this problem */
3108           queue_push(&solutions, 0);
3109           queue_push(&solutions, 0);
3110           if (i + 1 == problems.count)
3111             break;
3112           /* copy over proof of next problem */
3113           queue_push(&solutions, problems.elements[i + 1]);
3114           i++;
3115           problem = problems.elements + i + 1;
3116           continue;
3117         }
3118       refine_suggestion(solv, job, problem, v, &solution);
3119       if (!solution.count)
3120         continue;       /* this solution didn't work out */
3121
3122       nsol = 0;
3123       for (j = 0; j < solution.count; j++)
3124         {
3125           why = solution.elements[j];
3126           /* must be either job descriptor or update rule */
3127           assert(why < 0 || (why >= solv->updaterules && why < solv->updaterules_end));
3128 #if 0
3129           solver_printproblem(solv, why);
3130 #endif
3131           if (why < 0)
3132             {
3133               /* job descriptor */
3134               queue_push(&solutions, 0);
3135               queue_push(&solutions, -why);
3136             }
3137           else
3138             {
3139               /* update rule, find replacement package */
3140               Id p, d, *dp, rp = 0;
3141               Rule *rr;
3142               p = solv->installed->start + (why - solv->updaterules);
3143               rr = solv->rules + solv->featurerules + (why - solv->updaterules);
3144               if (!rr->p)
3145                 rr = solv->rules + why;
3146               if (solv->distupgrade && solv->rules[why].p != p && solv->decisionmap[p] > 0)
3147                 {
3148                   /* distupgrade case, allow to keep old package */
3149                   queue_push(&solutions, p);
3150                   queue_push(&solutions, p);
3151                   nsol++;
3152                   continue;
3153                 }
3154               if (solv->decisionmap[p] > 0)
3155                 continue;       /* false alarm, turned out we can keep the package */
3156               if (rr->w2)
3157                 {
3158                   d = rr->d < 0 ? -rr->d - 1 : rr->d;
3159                   if (!d)
3160                     {
3161                       if (solv->decisionmap[rr->w2] > 0 && pool->solvables[rr->w2].repo != solv->installed)
3162                         rp = rr->w2;
3163                     }
3164                   else
3165                     {
3166                       for (dp = pool->whatprovidesdata + d; *dp; dp++)
3167                         {
3168                           if (solv->decisionmap[*dp] > 0 && pool->solvables[*dp].repo != solv->installed)
3169                             {
3170                               rp = *dp;
3171                               break;
3172                             }
3173                         }
3174                     }
3175                 }
3176               queue_push(&solutions, p);
3177               queue_push(&solutions, rp);
3178             }
3179           nsol++;
3180         }
3181       /* mark end of this solution */
3182       if (nsol)
3183         {
3184           queue_push(&solutions, 0);
3185           queue_push(&solutions, 0);
3186         }
3187       else
3188         {
3189           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "Oops, everything was fine?\n");
3190         }
3191     }
3192   queue_free(&solution);
3193   queue_free(&problems);
3194   /* copy queue over to solutions */
3195   queue_free(&solv->problems);
3196   queue_clone(&solv->problems, &solutions);
3197
3198   /* bring solver back into problem state */
3199   revert(solv, 1);              /* XXX move to reset_solver? */
3200   reset_solver(solv);
3201
3202   assert(solv->problems.count == solutions.count);
3203   queue_free(&solutions);
3204 }
3205
3206
3207 /*-------------------------------------------------------------------
3208  *
3209  * problem iterator
3210  *
3211  * advance to next problem
3212  */
3213
3214 Id
3215 solver_next_problem(Solver *solv, Id problem)
3216 {
3217   Id *pp;
3218   if (problem == 0)
3219     return solv->problems.count ? 1 : 0;
3220   pp = solv->problems.elements + problem;
3221   while (pp[0] || pp[1])
3222     {
3223       /* solution */
3224       pp += 2;
3225       while (pp[0] || pp[1])
3226         pp += 2;
3227       pp += 2;
3228     }
3229   pp += 2;
3230   problem = pp - solv->problems.elements;
3231   if (problem >= solv->problems.count)
3232     return 0;
3233   return problem + 1;
3234 }
3235
3236
3237 /*-------------------------------------------------------------------
3238  *
3239  * solution iterator
3240  */
3241
3242 Id
3243 solver_next_solution(Solver *solv, Id problem, Id solution)
3244 {
3245   Id *pp;
3246   if (solution == 0)
3247     {
3248       solution = problem;
3249       pp = solv->problems.elements + solution;
3250       return pp[0] || pp[1] ? solution : 0;
3251     }
3252   pp = solv->problems.elements + solution;
3253   while (pp[0] || pp[1])
3254     pp += 2;
3255   pp += 2;
3256   solution = pp - solv->problems.elements;
3257   return pp[0] || pp[1] ? solution : 0;
3258 }
3259
3260
3261 /*-------------------------------------------------------------------
3262  *
3263  * solution element iterator
3264  */
3265
3266 Id
3267 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
3268 {
3269   Id *pp;
3270   element = element ? element + 2 : solution;
3271   pp = solv->problems.elements + element;
3272   if (!(pp[0] || pp[1]))
3273     return 0;
3274   *p = pp[0];
3275   *rp = pp[1];
3276   return element;
3277 }
3278
3279
3280 /*-------------------------------------------------------------------
3281  *
3282  * Retrieve information about a problematic rule
3283  *
3284  * this is basically the reverse of addrpmrulesforsolvable
3285  */
3286
3287 SolverProbleminfo
3288 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
3289 {
3290   Pool *pool = solv->pool;
3291   Repo *installed = solv->installed;
3292   Rule *r;
3293   Solvable *s;
3294   int dontfix = 0;
3295   Id p, d, *pp, req, *reqp, con, *conp, obs, *obsp, *dp;
3296
3297   assert(rid > 0);
3298   if (rid >= solv->jobrules && rid < solv->jobrules_end)
3299     {
3300
3301       r = solv->rules + rid;
3302       p = solv->ruletojob.elements[rid - solv->jobrules];
3303       *depp = job->elements[p + 1];
3304       *sourcep = p;
3305       *targetp = job->elements[p];
3306       d = r->d < 0 ? -r->d - 1 : r->d;
3307       if (d == 0 && r->w2 == 0 && r->p == -SYSTEMSOLVABLE && (job->elements[p] & SOLVER_SELECTMASK) != SOLVER_SOLVABLE_ONE_OF)
3308         return SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP;
3309       return SOLVER_PROBLEM_JOB_RULE;
3310     }
3311   if (rid >= solv->updaterules && rid < solv->updaterules_end)
3312     {
3313       *depp = 0;
3314       *sourcep = solv->installed->start + (rid - solv->updaterules);
3315       *targetp = 0;
3316       return SOLVER_PROBLEM_UPDATE_RULE;
3317     }
3318   assert(rid < solv->rpmrules_end);
3319   r = solv->rules + rid;
3320   assert(r->p < 0);
3321   d = r->d < 0 ? -r->d - 1 : r->d;
3322   if (d == 0 && r->w2 == 0)
3323     {
3324       /* a rpm rule assertion */
3325       s = pool->solvables - r->p;
3326       if (installed && !solv->fixsystem && s->repo == installed)
3327         dontfix = 1;
3328       assert(!dontfix); /* dontfix packages never have a neg assertion */
3329       *sourcep = -r->p;
3330       *targetp = 0;
3331       /* see why the package is not installable */
3332       if (s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
3333         {
3334           *depp = 0;
3335           return SOLVER_PROBLEM_NOT_INSTALLABLE;
3336         }
3337       /* check requires */
3338       if (s->requires)
3339         {
3340           reqp = s->repo->idarraydata + s->requires;
3341           while ((req = *reqp++) != 0)
3342             {
3343               if (req == SOLVABLE_PREREQMARKER)
3344                 continue;
3345               dp = pool_whatprovides(pool, req);
3346               if (*dp == 0)
3347                 break;
3348             }
3349           if (req)
3350             {
3351               *depp = req;
3352               return SOLVER_PROBLEM_NOTHING_PROVIDES_DEP;
3353             }
3354         }
3355       if (!solv->allowselfconflicts && s->conflicts)
3356         {
3357           conp = s->repo->idarraydata + s->conflicts;
3358           while ((con = *conp++) != 0)
3359             FOR_PROVIDES(p, pp, con)
3360               if (p == -r->p)
3361                 {
3362                   *depp = con;
3363                   return SOLVER_PROBLEM_SELF_CONFLICT;
3364                 }
3365         }
3366       /* should never happen */
3367       *depp = 0;
3368       return SOLVER_PROBLEM_RPM_RULE;
3369     }
3370   s = pool->solvables - r->p;
3371   if (installed && !solv->fixsystem && s->repo == installed)
3372     dontfix = 1;
3373   if (d == 0 && r->w2 < 0)
3374     {
3375       /* a package conflict */
3376       Solvable *s2 = pool->solvables - r->w2;
3377       int dontfix2 = 0;
3378
3379       if (installed && !solv->fixsystem && s2->repo == installed)
3380         dontfix2 = 1;
3381
3382       /* if both packages have the same name and at least one of them
3383        * is not installed, they conflict */
3384       if (s->name == s2->name && !(installed && s->repo == installed && s2->repo == installed))
3385         {
3386           /* also check noobsoletes map */
3387           if ((s->evr == s2->evr && s->arch == s2->arch) || !solv->noobsoletes.size
3388                 || ((!installed || s->repo != installed) && !MAPTST(&solv->noobsoletes, -r->p))
3389                 || ((!installed || s2->repo != installed) && !MAPTST(&solv->noobsoletes, -r->w2)))
3390             {
3391               *depp = 0;
3392               *sourcep = -r->p;
3393               *targetp = -r->w2;
3394               return SOLVER_PROBLEM_SAME_NAME;
3395             }
3396         }
3397
3398       /* check conflicts in both directions */
3399       if (s->conflicts)
3400         {
3401           conp = s->repo->idarraydata + s->conflicts;
3402           while ((con = *conp++) != 0)
3403             {
3404               FOR_PROVIDES(p, pp, con)
3405                 {
3406                   if (dontfix && pool->solvables[p].repo == installed)
3407                     continue;
3408                   if (p != -r->w2)
3409                     continue;
3410                   *depp = con;
3411                   *sourcep = -r->p;
3412                   *targetp = p;
3413                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3414                 }
3415             }
3416         }
3417       if (s2->conflicts)
3418         {
3419           conp = s2->repo->idarraydata + s2->conflicts;
3420           while ((con = *conp++) != 0)
3421             {
3422               FOR_PROVIDES(p, pp, con)
3423                 {
3424                   if (dontfix2 && pool->solvables[p].repo == installed)
3425                     continue;
3426                   if (p != -r->p)
3427                     continue;
3428                   *depp = con;
3429                   *sourcep = -r->w2;
3430                   *targetp = p;
3431                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3432                 }
3433             }
3434         }
3435       /* check obsoletes in both directions */
3436       if ((!installed || s->repo != installed) && s->obsoletes && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->p)))
3437         {
3438           obsp = s->repo->idarraydata + s->obsoletes;
3439           while ((obs = *obsp++) != 0)
3440             {
3441               FOR_PROVIDES(p, pp, obs)
3442                 {
3443                   if (p != -r->w2)
3444                     continue;
3445                   if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3446                     continue;
3447                   *depp = obs;
3448                   *sourcep = -r->p;
3449                   *targetp = p;
3450                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3451                 }
3452             }
3453         }
3454       if ((!installed || s2->repo != installed) && s2->obsoletes && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->w2)))
3455         {
3456           obsp = s2->repo->idarraydata + s2->obsoletes;
3457           while ((obs = *obsp++) != 0)
3458             {
3459               FOR_PROVIDES(p, pp, obs)
3460                 {
3461                   if (p != -r->p)
3462                     continue;
3463                   if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3464                     continue;
3465                   *depp = obs;
3466                   *sourcep = -r->w2;
3467                   *targetp = p;
3468                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3469                 }
3470             }
3471         }
3472       if (solv->implicitobsoleteusesprovides && (!installed || s->repo != installed) && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->p)))
3473         {
3474           FOR_PROVIDES(p, pp, s->name)
3475             {
3476               if (p != -r->w2)
3477                 continue;
3478               *depp = s->name;
3479               *sourcep = -r->p;
3480               *targetp = p;
3481               return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3482             }
3483         }
3484       if (solv->implicitobsoleteusesprovides && (!installed || s2->repo != installed) && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->w2)))
3485         {
3486           FOR_PROVIDES(p, pp, s2->name)
3487             {
3488               if (p != -r->p)
3489                 continue;
3490               *depp = s2->name;
3491               *sourcep = -r->w2;
3492               *targetp = p;
3493               return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3494             }
3495         }
3496       /* all cases checked, can't happen */
3497       *depp = 0;
3498       *sourcep = -r->p;
3499       *targetp = 0;
3500       return SOLVER_PROBLEM_RPM_RULE;
3501     }
3502   /* simple requires */
3503   if (s->requires)
3504     {
3505       reqp = s->repo->idarraydata + s->requires;
3506       while ((req = *reqp++) != 0)
3507         {
3508           if (req == SOLVABLE_PREREQMARKER)
3509             continue;
3510           dp = pool_whatprovides(pool, req);
3511           if (d == 0)
3512             {
3513               if (*dp == r->w2 && dp[1] == 0)
3514                 break;
3515             }
3516           else if (dp - pool->whatprovidesdata == d)
3517             break;
3518         }
3519       if (req)
3520         {
3521           *depp = req;
3522           *sourcep = -r->p;
3523           *targetp = 0;
3524           return SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE;
3525         }
3526     }
3527   /* all cases checked, can't happen */
3528   *depp = 0;
3529   *sourcep = -r->p;
3530   *targetp = 0;
3531   return SOLVER_PROBLEM_RPM_RULE;
3532 }
3533
3534
3535 /*-------------------------------------------------------------------
3536  *
3537  * find problem rule
3538  */
3539
3540 static void
3541 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
3542 {
3543   Id rid, d;
3544   Id lreqr, lconr, lsysr, ljobr;
3545   Rule *r;
3546   int reqassert = 0;
3547
3548   lreqr = lconr = lsysr = ljobr = 0;
3549   while ((rid = solv->learnt_pool.elements[idx++]) != 0)
3550     {
3551       assert(rid > 0);
3552       if (rid >= solv->learntrules)
3553         findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
3554       else if (rid >= solv->jobrules && rid < solv->jobrules_end)
3555         {
3556           if (!*jobrp)
3557             *jobrp = rid;
3558         }
3559       else if (rid >= solv->updaterules && rid < solv->updaterules_end)
3560         {
3561           if (!*sysrp)
3562             *sysrp = rid;
3563         }
3564       else
3565         {
3566           assert(rid < solv->rpmrules_end);
3567           r = solv->rules + rid;
3568           d = r->d < 0 ? -r->d - 1 : r->d;
3569           if (!d && r->w2 < 0)
3570             {
3571               if (!*conrp)
3572                 *conrp = rid;
3573             }
3574           else
3575             {
3576               if (!d && r->w2 == 0 && !reqassert)
3577                 {
3578                   /* prefer assertions (XXX: bad idea?) */
3579                   *reqrp = rid;
3580                   reqassert = 1;
3581                 }
3582               if (!*reqrp)
3583                 *reqrp = rid;
3584               else if (solv->installed && r->p < 0 && solv->pool->solvables[-r->p].repo == solv->installed)
3585                 {
3586                   /* prefer rules of installed packages */
3587                   Id op = *reqrp >= 0 ? solv->rules[*reqrp].p : -*reqrp;
3588                   if (op <= 0 || solv->pool->solvables[op].repo != solv->installed)
3589                     *reqrp = rid;
3590                 }
3591             }
3592         }
3593     }
3594   if (!*reqrp && lreqr)
3595     *reqrp = lreqr;
3596   if (!*conrp && lconr)
3597     *conrp = lconr;
3598   if (!*jobrp && ljobr)
3599     *jobrp = ljobr;
3600   if (!*sysrp && lsysr)
3601     *sysrp = lsysr;
3602 }
3603
3604
3605 /*-------------------------------------------------------------------
3606  *
3607  * find problem rule
3608  *
3609  * search for a rule that describes the problem to the
3610  * user. A pretty hopeless task, actually. We currently
3611  * prefer simple requires.
3612  */
3613
3614 Id
3615 solver_findproblemrule(Solver *solv, Id problem)
3616 {
3617   Id reqr, conr, sysr, jobr;
3618   Id idx = solv->problems.elements[problem - 1];
3619   reqr = conr = sysr = jobr = 0;
3620   findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
3621   if (reqr)
3622     return reqr;
3623   if (conr)
3624     return conr;
3625   if (sysr)
3626     return sysr;
3627   if (jobr)
3628     return jobr;
3629   assert(0);
3630 }
3631
3632
3633 /*-------------------------------------------------------------------
3634  *
3635  * create reverse obsoletes map for installed solvables
3636  *
3637  * for each installed solvable find which packages with *different* names
3638  * obsolete the solvable.
3639  * this index is used in policy_findupdatepackages if noupdateprovide is set.
3640  */
3641
3642 static void
3643 create_obsolete_index(Solver *solv)
3644 {
3645   Pool *pool = solv->pool;
3646   Solvable *s;
3647   Repo *installed = solv->installed;
3648   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
3649   int i, n;
3650
3651   if (!installed || !installed->nsolvables)
3652     return;
3653   solv->obsoletes = obsoletes = sat_calloc(installed->end - installed->start, sizeof(Id));
3654   for (i = 1; i < pool->nsolvables; i++)
3655     {
3656       s = pool->solvables + i;
3657       if (!s->obsoletes)
3658         continue;
3659       if (!pool_installable(pool, s))
3660         continue;
3661       obsp = s->repo->idarraydata + s->obsoletes;
3662       while ((obs = *obsp++) != 0)
3663         {
3664           FOR_PROVIDES(p, pp, obs)
3665             {
3666               if (pool->solvables[p].repo != installed)
3667                 continue;
3668               if (pool->solvables[p].name == s->name)
3669                 continue;
3670               if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3671                 continue;
3672               obsoletes[p - installed->start]++;
3673             }
3674         }
3675     }
3676   n = 0;
3677   for (i = 0; i < installed->nsolvables; i++)
3678     if (obsoletes[i])
3679       {
3680         n += obsoletes[i] + 1;
3681         obsoletes[i] = n;
3682       }
3683   solv->obsoletes_data = obsoletes_data = sat_calloc(n + 1, sizeof(Id));
3684   POOL_DEBUG(SAT_DEBUG_STATS, "obsoletes data: %d entries\n", n + 1);
3685   for (i = pool->nsolvables - 1; i > 0; i--)
3686     {
3687       s = pool->solvables + i;
3688       if (!s->obsoletes)
3689         continue;
3690       if (!pool_installable(pool, s))
3691         continue;
3692       obsp = s->repo->idarraydata + s->obsoletes;
3693       while ((obs = *obsp++) != 0)
3694         {
3695           FOR_PROVIDES(p, pp, obs)
3696             {
3697               if (pool->solvables[p].repo != installed)
3698                 continue;
3699               if (pool->solvables[p].name == s->name)
3700                 continue;
3701               if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3702                 continue;
3703               p -= installed->start;
3704               if (obsoletes_data[obsoletes[p]] != i)
3705                 obsoletes_data[--obsoletes[p]] = i;
3706             }
3707         }
3708     }
3709 }
3710
3711
3712 /*-------------------------------------------------------------------
3713  *
3714  * remove disabled conflicts
3715  */
3716
3717 static void
3718 removedisabledconflicts(Solver *solv, Queue *removed)
3719 {
3720   Pool *pool = solv->pool;
3721   int i, n;
3722   Id p, why, *dp;
3723   Id new;
3724   Rule *r;
3725   Id *decisionmap = solv->decisionmap;
3726
3727   POOL_DEBUG(SAT_DEBUG_STATS, "removedisabledconflicts\n");
3728   queue_empty(removed);
3729   for (i = 0; i < solv->decisionq.count; i++)
3730     {
3731       p = solv->decisionq.elements[i];
3732       if (p > 0)
3733         continue;
3734       /* a conflict. we never do conflicts on free decisions, so there
3735        * must have been an unit rule */
3736       why = solv->decisionq_why.elements[i];
3737       assert(why > 0);
3738       r = solv->rules + why;
3739       if (r->d < 0 && decisionmap[-p])
3740         {
3741           /* rule is now disabled, remove from decisionmap */
3742           POOL_DEBUG(SAT_DEBUG_STATS, "removing conflict for package %s[%d]\n", solvable2str(pool, pool->solvables - p), -p);
3743           queue_push(removed, -p);
3744           queue_push(removed, decisionmap[-p]);
3745           decisionmap[-p] = 0;
3746         }
3747     }
3748   if (!removed->count)
3749     return;
3750   /* we removed some confliced packages. some of them might still
3751    * be in conflict, so search for unit rules and re-conflict */
3752   new = 0;
3753   for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++)
3754     {
3755       if (i == solv->nrules)
3756         {
3757           i = 1;
3758           r = solv->rules + i;
3759         }
3760       if (r->d < 0)
3761         continue;
3762       if (!r->w2)
3763         {
3764           if (r->p < 0 && !decisionmap[-r->p])
3765             new = r->p;
3766         }
3767       else if (!r->d)
3768         {
3769           /* binary rule */
3770           if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2))
3771             new = r->p;
3772           else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p))
3773             new = r->w2;
3774         }
3775       else
3776         {
3777           if (r->p < 0 && decisionmap[-r->p] == 0)
3778             new = r->p;
3779           if (new || DECISIONMAP_FALSE(r->p))
3780             {
3781               dp = pool->whatprovidesdata + r->d;
3782               while ((p = *dp++) != 0)
3783                 {
3784                   if (new && p == new)
3785                     continue;
3786                   if (p < 0 && decisionmap[-p] == 0)
3787                     {
3788                       if (new)
3789                         {
3790                           new = 0;
3791                           break;
3792                         }
3793                       new = p;
3794                     }
3795                   else if (!DECISIONMAP_FALSE(p))
3796                     {
3797                       new = 0;
3798                       break;
3799                     }
3800                 }
3801             }
3802         }
3803       if (new)
3804         {
3805           POOL_DEBUG(SAT_DEBUG_STATS, "re-conflicting package %s[%d]\n", solvable2str(pool, pool->solvables - new), -new);
3806           decisionmap[-new] = -1;
3807           new = 0;
3808           n = 0;        /* redo all rules */
3809         }
3810     }
3811 }
3812
3813
3814 /*-------------------------------------------------------------------
3815  *
3816  * weaken solvable dependencies
3817  */
3818
3819 static void
3820 weaken_solvable_deps(Solver *solv, Id p)
3821 {
3822   int i;
3823   Rule *r;
3824
3825   for (i = 1, r = solv->rules + i; i < solv->rpmrules_end; i++, r++)
3826     {
3827       if (r->p != -p)
3828         continue;
3829       if ((r->d == 0 || r->d == -1) && r->w2 < 0)
3830         continue;       /* conflict */
3831       queue_push(&solv->weakruleq, i);
3832     }
3833 }
3834
3835 /********************************************************************/
3836 /* main() */
3837
3838 /*
3839  *
3840  * solve job queue
3841  *
3842  */
3843
3844 void
3845 solver_solve(Solver *solv, Queue *job)
3846 {
3847   Pool *pool = solv->pool;
3848   Repo *installed = solv->installed;
3849   int i;
3850   int oldnrules;
3851   Map addedmap;                /* '1' == have rpm-rules for solvable */
3852   Map installcandidatemap;
3853   Id how, what, select, name, weak, p, *pp, d;
3854   Queue q, redoq;
3855   Solvable *s;
3856   int goterase;
3857   Rule *r;
3858
3859   POOL_DEBUG(SAT_DEBUG_STATS, "solver started\n");
3860   POOL_DEBUG(SAT_DEBUG_STATS, "fixsystem=%d updatesystem=%d dosplitprovides=%d, noupdateprovide=%d\n", solv->fixsystem, solv->updatesystem, solv->dosplitprovides, solv->noupdateprovide);
3861   POOL_DEBUG(SAT_DEBUG_STATS, "distupgrade=%d distupgrade_removeunsupported=%d\n", solv->distupgrade, solv->distupgrade_removeunsupported);
3862   POOL_DEBUG(SAT_DEBUG_STATS, "allowuninstall=%d, allowdowngrade=%d, allowarchchange=%d, allowvendorchange=%d\n", solv->allowuninstall, solv->allowdowngrade, solv->allowarchchange, solv->allowvendorchange);
3863   POOL_DEBUG(SAT_DEBUG_STATS, "promoteepoch=%d, allowvirtualconflicts=%d, allowselfconflicts=%d\n", pool->promoteepoch, solv->allowvirtualconflicts, solv->allowselfconflicts);
3864   POOL_DEBUG(SAT_DEBUG_STATS, "obsoleteusesprovides=%d, implicitobsoleteusesprovides=%d\n", solv->obsoleteusesprovides, solv->implicitobsoleteusesprovides);
3865   POOL_DEBUG(SAT_DEBUG_STATS, "dontinstallrecommended=%d, ignorealreadyrecommended=%d, dontshowinstalledrecommended=%d\n", solv->dontinstallrecommended, solv->ignorealreadyrecommended, solv->dontshowinstalledrecommended);
3866   /* create whatprovides if not already there */
3867   if (!pool->whatprovides)
3868     pool_createwhatprovides(pool);
3869
3870   /* create obsolete index if needed */
3871   create_obsolete_index(solv);
3872
3873   /*
3874    * create basic rule set of all involved packages
3875    * use addedmap bitmap to make sure we don't create rules twice
3876    *
3877    */
3878
3879   /* create noobsolete map if needed */
3880   for (i = 0; i < job->count; i += 2)
3881     {
3882       how = job->elements[i] & ~SOLVER_WEAK;
3883       if ((how & SOLVER_JOBMASK) != SOLVER_NOOBSOLETES)
3884         continue;
3885       what = job->elements[i + 1];
3886       select = how & SOLVER_SELECTMASK;
3887       if (!solv->noobsoletes.size)
3888         map_init(&solv->noobsoletes, pool->nsolvables);
3889       FOR_JOB_SELECT(p, pp, select, what)
3890         MAPSET(&solv->noobsoletes, p);
3891     }
3892
3893   map_init(&addedmap, pool->nsolvables);
3894   map_init(&installcandidatemap, pool->nsolvables);
3895   queue_init(&q);
3896
3897   /*
3898    * always install our system solvable
3899    */
3900   MAPSET(&addedmap, SYSTEMSOLVABLE);
3901   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
3902   queue_push(&solv->decisionq_why, 0);
3903   solv->decisionmap[SYSTEMSOLVABLE] = 1; /* installed at level '1' */
3904
3905   /*
3906    * create rules for all package that could be involved with the solving
3907    * so called: rpm rules
3908    *
3909    */
3910   if (installed)
3911     {
3912       oldnrules = solv->nrules;
3913       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
3914       FOR_REPO_SOLVABLES(installed, p, s)
3915         addrpmrulesforsolvable(solv, s, &addedmap);
3916       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
3917       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
3918       oldnrules = solv->nrules;
3919       FOR_REPO_SOLVABLES(installed, p, s)
3920         addrpmrulesforupdaters(solv, s, &addedmap, 1);
3921       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
3922     }
3923
3924   /*
3925    * create rules for all packages involved in the job
3926    * (to be installed or removed)
3927    */
3928
3929   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
3930   oldnrules = solv->nrules;
3931   for (i = 0; i < job->count; i += 2)
3932     {
3933       how = job->elements[i];
3934       what = job->elements[i + 1];
3935       select = how & SOLVER_SELECTMASK;
3936
3937       switch (how & SOLVER_JOBMASK)
3938         {
3939         case SOLVER_INSTALL:
3940           FOR_JOB_SELECT(p, pp, select, what)
3941             {
3942               MAPSET(&installcandidatemap, p);
3943               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3944             }
3945           break;
3946         case SOLVER_UPDATE:
3947           /* FIXME: semantics? */
3948           FOR_JOB_SELECT(p, pp, select, what)
3949             addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
3950           break;
3951         }
3952     }
3953   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
3954
3955   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for recommended/suggested packages ***\n");
3956
3957   oldnrules = solv->nrules;
3958
3959     /*
3960      * add rules for suggests, enhances
3961      */
3962   addrpmrulesforweak(solv, &addedmap);
3963   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
3964
3965   IF_POOLDEBUG (SAT_DEBUG_STATS)
3966     {
3967       int possible = 0, installable = 0;
3968       for (i = 1; i < pool->nsolvables; i++)
3969         {
3970           if (pool_installable(pool, pool->solvables + i))
3971             installable++;
3972           if (MAPTST(&addedmap, i))
3973             possible++;
3974         }
3975       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
3976     }
3977
3978   /*
3979    * first pass done, we now have all the rpm rules we need.
3980    * unify existing rules before going over all job rules and
3981    * policy rules.
3982    * at this point the system is always solvable,
3983    * as an empty system (remove all packages) is a valid solution
3984    */
3985
3986   unifyrules(solv);                               /* remove duplicate rpm rules */
3987
3988   solv->rpmrules_end = solv->nrules;              /* mark end of rpm rules */
3989
3990   solv->directdecisions = solv->decisionq.count;
3991   POOL_DEBUG(SAT_DEBUG_STATS, "decisions so far: %d\n", solv->decisionq.count);
3992
3993   /*
3994    * create feature rules
3995    *
3996    * foreach installed:
3997    *   create assertion (keep installed, if no update available)
3998    *   or
3999    *   create update rule (A|update1(A)|update2(A)|...)
4000    *
4001    * those are used later on to keep a version of the installed packages in
4002    * best effort mode
4003    */
4004
4005   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add feature rules ***\n");
4006   solv->featurerules = solv->nrules;              /* mark start of feature rules */
4007   if (installed)
4008     {
4009         /* foreach possibly installed solvable */
4010       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
4011         {
4012           if (s->repo != installed)
4013             {
4014               addrule(solv, 0, 0);      /* create dummy rule */
4015               continue;
4016             }
4017           addupdaterule(solv, s, 1);    /* allow s to be updated */
4018         }
4019         /*
4020          * assert one rule per installed solvable,
4021          * either an assertion (A)
4022          * or a possible update (A|update1(A)|update2(A)|...)
4023          */
4024       assert(solv->nrules - solv->featurerules == installed->end - installed->start);
4025     }
4026   solv->featurerules_end = solv->nrules;
4027
4028     /*
4029      * Add update rules for installed solvables
4030      *
4031      * almost identical to feature rules
4032      * except that downgrades/archchanges/vendorchanges are not allowed
4033      */
4034
4035   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add update rules ***\n");
4036   solv->updaterules = solv->nrules;
4037
4038   if (installed)
4039     { /* foreach installed solvables */
4040       /* we create all update rules, but disable some later on depending on the job */
4041       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
4042         {
4043           Rule *sr;
4044
4045           if (s->repo != installed)
4046             {
4047               addrule(solv, 0, 0);      /* create dummy rule */
4048               continue;
4049             }
4050           addupdaterule(solv, s, 0);    /* allowall = 0: downgrades not allowed */
4051             /*
4052              * check for and remove duplicate
4053              */
4054           r = solv->rules + solv->nrules - 1;           /* r: update rule */
4055           sr = r - (installed->end - installed->start); /* sr: feature rule */
4056           /* it's orphaned if there is no feature rule or the feature rule
4057            * consists just of the installed package */
4058           if (!sr->p || (sr->p == i && !sr->d && !sr->w2))
4059             queue_push(&solv->orphaned, i);
4060           if (!r->p)
4061             {
4062               assert(!sr->p);   /* can't have feature rule and no update rule */
4063               continue;
4064             }
4065           unifyrules_sortcmp_data = pool;
4066           if (!unifyrules_sortcmp(r, sr))
4067             {
4068               /* identical rule, kill unneeded rule */
4069               if (solv->allowuninstall)
4070                 {
4071                   /* keep feature rule, make it weak */
4072                   memset(r, 0, sizeof(*r));
4073                   queue_push(&solv->weakruleq, sr - solv->rules);
4074                 }
4075               else
4076                 {
4077                   /* keep update rule */
4078                   memset(sr, 0, sizeof(*sr));
4079                 }
4080             }
4081           else if (solv->allowuninstall)
4082             {
4083               /* make both feature and update rule weak */
4084               queue_push(&solv->weakruleq, r - solv->rules);
4085               queue_push(&solv->weakruleq, sr - solv->rules);
4086             }
4087           else
4088             disablerule(solv, sr);
4089         }
4090       /* consistency check: we added a rule for _every_ installed solvable */
4091       assert(solv->nrules - solv->updaterules == installed->end - installed->start);
4092     }
4093   solv->updaterules_end = solv->nrules;
4094
4095
4096   /*
4097    * now add all job rules
4098    */
4099
4100   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
4101
4102   solv->jobrules = solv->nrules;
4103   for (i = 0; i < job->count; i += 2)
4104     {
4105       oldnrules = solv->nrules;
4106
4107       how = job->elements[i];
4108       what = job->elements[i + 1];
4109       weak = how & SOLVER_WEAK;
4110       select = how & SOLVER_SELECTMASK;
4111       switch (how & SOLVER_JOBMASK)
4112         {
4113         case SOLVER_INSTALL:
4114           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4115           if (select == SOLVER_SOLVABLE)
4116             {
4117               p = what;
4118               d = 0;
4119             }
4120           else
4121             {
4122               queue_empty(&q);
4123               FOR_JOB_SELECT(p, pp, select, what)
4124                 queue_push(&q, p);
4125               if (!q.count)
4126                 {
4127                   /* no candidate found, make this an impossible rule */
4128                   queue_push(&q, -SYSTEMSOLVABLE);
4129                 }
4130               p = queue_shift(&q);      /* get first candidate */
4131               d = !q.count ? 0 : pool_queuetowhatprovides(pool, &q);    /* internalize */
4132             }
4133           addrule(solv, p, d);          /* add install rule */
4134           queue_push(&solv->ruletojob, i);
4135           if (weak)
4136             queue_push(&solv->weakruleq, solv->nrules - 1);
4137           break;
4138         case SOLVER_ERASE:
4139           POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4140           if (select == SOLVER_SOLVABLE && solv->installed && pool->solvables[what].repo == solv->installed)
4141             {
4142               /* special case for "erase a specific solvable": we also
4143                * erase all other solvables with that name, so that they
4144                * don't get picked up as replacement */
4145               name = pool->solvables[what].name;
4146               FOR_PROVIDES(p, pp, name)
4147                 {
4148                   if (p == what)
4149                     continue;
4150                   s = pool->solvables + p;
4151                   if (s->name != name)
4152                     continue;
4153                   /* keep other versions installed */
4154                   if (s->repo == solv->installed)
4155                     continue;
4156                   /* keep installcandidates of other jobs */
4157                   if (MAPTST(&installcandidatemap, p))
4158                     continue;
4159                   addrule(solv, -p, 0);                 /* remove by Id */
4160                   queue_push(&solv->ruletojob, i);
4161                   if (weak)
4162                     queue_push(&solv->weakruleq, solv->nrules - 1);
4163                 }
4164             }
4165           FOR_JOB_SELECT(p, pp, select, what)
4166             {
4167               addrule(solv, -p, 0);
4168               queue_push(&solv->ruletojob, i);
4169               if (weak)
4170                 queue_push(&solv->weakruleq, solv->nrules - 1);
4171             }
4172           break;
4173
4174         case SOLVER_UPDATE:
4175           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4176           if (select != SOLVER_SOLVABLE)
4177             break;
4178           s = pool->solvables + what;
4179           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solvable2str(pool, s));
4180           addupdaterule(solv, s, 0);
4181           queue_push(&solv->ruletojob, i);
4182           if (weak)
4183             queue_push(&solv->weakruleq, solv->nrules - 1);
4184           break;
4185         case SOLVER_WEAKENDEPS:
4186           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sweaken deps %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4187           if (select != SOLVER_SOLVABLE)
4188             break;
4189           s = pool->solvables + what;
4190           weaken_solvable_deps(solv, what);
4191           break;
4192         case SOLVER_NOOBSOLETES:
4193           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sno obsolete %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4194           break;
4195         case SOLVER_LOCK:
4196           POOL_DEBUG(SAT_DEBUG_JOB, "job: %slock %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4197           FOR_JOB_SELECT(p, pp, select, what)
4198             {
4199               s = pool->solvables + p;
4200               if (installed && s->repo == installed)
4201                 addrule(solv, p, 0);
4202               else
4203                 addrule(solv, -p, 0);
4204               queue_push(&solv->ruletojob, i);
4205               if (weak)
4206                 queue_push(&solv->weakruleq, solv->nrules - 1);
4207             }
4208           break;
4209         default:
4210           POOL_DEBUG(SAT_DEBUG_JOB, "job: unknown job\n");
4211           break;
4212         }
4213
4214         /*
4215          * debug
4216          */
4217
4218       IF_POOLDEBUG (SAT_DEBUG_JOB)
4219         {
4220           int j;
4221           if (solv->nrules == oldnrules)
4222             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n");
4223           for (j = oldnrules; j < solv->nrules; j++)
4224             {
4225               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
4226               solver_printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
4227             }
4228         }
4229     }
4230   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
4231   solv->jobrules_end = solv->nrules;
4232
4233     /* all rules created
4234      * --------------------------------------------------------------
4235      * prepare for solving
4236      */
4237
4238   /* free unneeded memory */
4239   map_free(&addedmap);
4240   map_free(&installcandidatemap);
4241   queue_free(&q);
4242
4243   /* create weak map */
4244   map_init(&solv->weakrulemap, solv->nrules);
4245   for (i = 0; i < solv->weakruleq.count; i++)
4246     {
4247       p = solv->weakruleq.elements[i];
4248       MAPSET(&solv->weakrulemap, p);
4249     }
4250
4251   /* all new rules are learnt after this point */
4252   solv->learntrules = solv->nrules;
4253
4254   /* create assertion index. it is only used to speed up
4255    * makeruledecsions() a bit */
4256   for (i = 1, r = solv->rules + i; i < solv->nrules; i++, r++)
4257     if (r->p && !r->w2 && (r->d == 0 || r->d == -1))
4258       queue_push(&solv->ruleassertions, i);
4259
4260   /* disable update rules that conflict with our job */
4261   disableupdaterules(solv, job, -1);
4262
4263   /* make decisions based on job/update assertions */
4264   makeruledecisions(solv);
4265
4266   /* create watches chains */
4267   makewatches(solv);
4268
4269   POOL_DEBUG(SAT_DEBUG_STATS, "problems so far: %d\n", solv->problems.count);
4270
4271   /*
4272    * ********************************************
4273    * solve!
4274    * ********************************************
4275    */
4276
4277   run_solver(solv, 1, solv->dontinstallrecommended ? 0 : 1);
4278
4279   queue_init(&redoq);
4280   goterase = 0;
4281   /* disable all erase jobs (including weak "keep uninstalled" rules) */
4282   for (i = solv->jobrules, r = solv->rules + i; i < solv->learntrules; i++, r++)
4283     {
4284       if (r->d < 0)     /* disabled ? */
4285         continue;
4286       if (r->p > 0)     /* install job? */
4287         continue;
4288       disablerule(solv, r);
4289       goterase++;
4290     }
4291
4292   if (goterase)
4293     {
4294       enabledisablelearntrules(solv);
4295       removedisabledconflicts(solv, &redoq);
4296     }
4297
4298   /*
4299    * find recommended packages
4300    */
4301
4302   /* if redoq.count == 0 we already found all recommended in the
4303    * solver run */
4304   if (redoq.count || solv->dontinstallrecommended || !solv->dontshowinstalledrecommended || solv->ignorealreadyrecommended)
4305     {
4306       Id rec, *recp, p, *pp;
4307
4308       /* create map of all recommened packages */
4309       solv->recommends_index = -1;
4310       MAPZERO(&solv->recommendsmap);
4311       for (i = 0; i < solv->decisionq.count; i++)
4312         {
4313           p = solv->decisionq.elements[i];
4314           if (p < 0)
4315             continue;
4316           s = pool->solvables + p;
4317           if (s->recommends)
4318             {
4319               recp = s->repo->idarraydata + s->recommends;
4320               while ((rec = *recp++) != 0)
4321                 {
4322                   FOR_PROVIDES(p, pp, rec)
4323                     if (solv->decisionmap[p] > 0)
4324                       break;
4325                   if (p)
4326                     {
4327                       if (!solv->dontshowinstalledrecommended)
4328                         {
4329                           FOR_PROVIDES(p, pp, rec)
4330                             if (solv->decisionmap[p] > 0)
4331                               MAPSET(&solv->recommendsmap, p);
4332                         }
4333                       continue; /* p != 0: already fulfilled */
4334                     }
4335                   FOR_PROVIDES(p, pp, rec)
4336                     MAPSET(&solv->recommendsmap, p);
4337                 }
4338             }
4339         }
4340       for (i = 1; i < pool->nsolvables; i++)
4341         {
4342           if (solv->decisionmap[i] < 0)
4343             continue;
4344           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
4345             continue;
4346           s = pool->solvables + i;
4347           if (!MAPTST(&solv->recommendsmap, i))
4348             {
4349               if (!s->supplements)
4350                 continue;
4351               if (!pool_installable(pool, s))
4352                 continue;
4353               if (!solver_is_supplementing(solv, s))
4354                 continue;
4355             }
4356           if (solv->dontinstallrecommended)
4357             queue_push(&solv->recommendations, i);
4358           else
4359             queue_pushunique(&solv->recommendations, i);
4360         }
4361       /* we use MODE_SUGGEST here so that repo prio is ignored */
4362       policy_filter_unwanted(solv, &solv->recommendations, 0, POLICY_MODE_SUGGEST);
4363     }
4364
4365   /*
4366    * find suggested packages
4367    */
4368
4369   if (1)
4370     {
4371       Id sug, *sugp, p, *pp;
4372
4373       /* create map of all suggests that are still open */
4374       solv->recommends_index = -1;
4375       MAPZERO(&solv->suggestsmap);
4376       for (i = 0; i < solv->decisionq.count; i++)
4377         {
4378           p = solv->decisionq.elements[i];
4379           if (p < 0)
4380             continue;
4381           s = pool->solvables + p;
4382           if (s->suggests)
4383             {
4384               sugp = s->repo->idarraydata + s->suggests;
4385               while ((sug = *sugp++) != 0)
4386                 {
4387                   FOR_PROVIDES(p, pp, sug)
4388                     if (solv->decisionmap[p] > 0)
4389                       break;
4390                   if (p)
4391                     {
4392                       if (!solv->dontshowinstalledrecommended)
4393                         {
4394                           FOR_PROVIDES(p, pp, sug)
4395                             if (solv->decisionmap[p] > 0)
4396                               MAPSET(&solv->suggestsmap, p);
4397                         }
4398                       continue; /* already fulfilled */
4399                     }
4400                   FOR_PROVIDES(p, pp, sug)
4401                     MAPSET(&solv->suggestsmap, p);
4402                 }
4403             }
4404         }
4405       for (i = 1; i < pool->nsolvables; i++)
4406         {
4407           if (solv->decisionmap[i] < 0)
4408             continue;
4409           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
4410             continue;
4411           s = pool->solvables + i;
4412           if (!MAPTST(&solv->suggestsmap, i))
4413             {
4414               if (!s->enhances)
4415                 continue;
4416               if (!pool_installable(pool, s))
4417                 continue;
4418               if (!solver_is_enhancing(solv, s))
4419                 continue;
4420             }
4421           queue_push(&solv->suggestions, i);
4422         }
4423       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
4424     }
4425
4426   if (redoq.count)
4427     {
4428       /* restore decisionmap */
4429       for (i = 0; i < redoq.count; i += 2)
4430         solv->decisionmap[redoq.elements[i]] = redoq.elements[i + 1];
4431     }
4432
4433     /*
4434      * if unsolvable, prepare solutions
4435      */
4436
4437   if (solv->problems.count)
4438     {
4439       int recocount = solv->recommendations.count;
4440       solv->recommendations.count = 0;  /* so that revert() doesn't mess with it */
4441       queue_empty(&redoq);
4442       for (i = 0; i < solv->decisionq.count; i++)
4443         {
4444           Id p = solv->decisionq.elements[i];
4445           queue_push(&redoq, p);
4446           queue_push(&redoq, solv->decisionq_why.elements[i]);
4447           queue_push(&redoq, solv->decisionmap[p > 0 ? p : -p]);
4448         }
4449       problems_to_solutions(solv, job);
4450       memset(solv->decisionmap, 0, pool->nsolvables * sizeof(Id));
4451       queue_empty(&solv->decisionq);
4452       queue_empty(&solv->decisionq_why);
4453       for (i = 0; i < redoq.count; i += 3)
4454         {
4455           Id p = redoq.elements[i];
4456           queue_push(&solv->decisionq, p);
4457           queue_push(&solv->decisionq_why, redoq.elements[i + 1]);
4458           solv->decisionmap[p > 0 ? p : -p] = redoq.elements[i + 2];
4459         }
4460       solv->recommendations.count = recocount;
4461     }
4462
4463   POOL_DEBUG(SAT_DEBUG_STATS, "final solver statistics: %d learned rules, %d unsolvable\n", solv->stats_learned, solv->stats_unsolvable);
4464   queue_free(&redoq);
4465 }
4466
4467 /***********************************************************************/
4468 /* disk usage computations */
4469
4470 /*-------------------------------------------------------------------
4471  *
4472  * calculate DU changes
4473  */
4474
4475 void
4476 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
4477 {
4478   Map installedmap;
4479
4480   solver_create_state_maps(solv, &installedmap, 0);
4481   pool_calc_duchanges(solv->pool, solv->installed, &installedmap, mps, nmps);
4482   map_free(&installedmap);
4483 }
4484
4485
4486 /*-------------------------------------------------------------------
4487  *
4488  * calculate changes in install size
4489  */
4490
4491 int
4492 solver_calc_installsizechange(Solver *solv)
4493 {
4494   Map installedmap;
4495   int change;
4496
4497   solver_create_state_maps(solv, &installedmap, 0);
4498   change = pool_calc_installsizechange(solv->pool, solv->installed, &installedmap);
4499   map_free(&installedmap);
4500   return change;
4501 }
4502
4503 /* EOF */