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