src/solver.c

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