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