src/solver.c

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