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   /* cannot be zero by default since zero corresponds to KIND_PACKAGE
2120    * so we initialize it with _KIND_MAX to denote 'all kinds'
2121    * if the application sets this to a specific KIND_, the value is
2122    * incremented by 1 at solver start to make 'if (limittokind)' checks easy
2123    *
2124    * A sure candidate for a more clever implementation
2125    */
2126
2127   solv->limittokind = _KIND_MAX;
2128
2129   return solv;
2130 }
2131
2132
2133 /*
2134  * solver_free
2135  */
2136
2137 void
2138 solver_free(Solver *solv)
2139 {
2140   queue_free(&solv->ruletojob);
2141   queue_free(&solv->decisionq);
2142   queue_free(&solv->decisionq_why);
2143   queue_free(&solv->learnt_why);
2144   queue_free(&solv->learnt_pool);
2145   queue_free(&solv->problems);
2146   queue_free(&solv->suggestions);
2147   queue_free(&solv->branches);
2148   queue_free(&solv->covenantq);
2149
2150   map_free(&solv->recommendsmap);
2151   map_free(&solv->suggestsmap);
2152   map_free(&solv->noupdate);
2153
2154   sat_free(solv->decisionmap);
2155   sat_free(solv->rules);
2156   sat_free(solv->watches);
2157   sat_free(solv->weaksystemrules);
2158   sat_free(solv->obsoletes);
2159   sat_free(solv->obsoletes_data);
2160   sat_free(solv);
2161 }
2162
2163
2164 /*-------------------------------------------------------*/
2165
2166 /*
2167  * run_solver
2168  *
2169  * all rules have been set up, now actually run the solver
2170  *
2171  */
2172
2173 static void
2174 run_solver(Solver *solv, int disablerules, int doweak)
2175 {
2176   Queue dq;
2177   int systemlevel;
2178   int level, olevel;
2179   Rule *r;
2180   int i, j, n;
2181   Solvable *s;
2182   Pool *pool = solv->pool;
2183   Id p, *dp;
2184
2185   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
2186     {
2187       POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
2188       for (i = 0; i < solv->nrules; i++)
2189         printrule(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
2190     }
2191
2192   POOL_DEBUG(SAT_DEBUG_STATS, "initial decisions: %d\n", solv->decisionq.count);
2193
2194   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2195     printdecisions(solv);
2196
2197   /* start SAT algorithm */
2198   level = 1;
2199   systemlevel = level + 1;
2200   POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n");
2201
2202   queue_init(&dq);
2203   for (;;)
2204     {
2205       /*
2206        * propagate
2207        */
2208
2209       if (level == 1)
2210         {
2211           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
2212           if ((r = propagate(solv, level)) != 0)
2213             {
2214               if (analyze_unsolvable(solv, r, disablerules))
2215                 continue;
2216               queue_free(&dq);
2217               return;
2218             }
2219         }
2220
2221       /*
2222        * installed packages
2223        */
2224
2225       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
2226         {
2227           if (!solv->updatesystem)
2228             {
2229               /* try to keep as many packages as possible */
2230               POOL_DEBUG(SAT_DEBUG_STATS, "installing system packages\n");
2231               for (i = solv->installed->start, n = 0; ; i++)
2232                 {
2233                   if (n == solv->installed->nsolvables)
2234                     break;
2235                   if (i == solv->installed->end)
2236                     i = solv->installed->start;
2237                   s = pool->solvables + i;
2238                   if (s->repo != solv->installed)
2239                     continue;
2240                   n++;
2241                   if (solv->decisionmap[i] != 0)
2242                     continue;
2243                   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "keeping %s\n", solvable2str(pool, s));
2244                   olevel = level;
2245                   level = setpropagatelearn(solv, level, i, disablerules);
2246                   if (level == 0)
2247                     {
2248                       queue_free(&dq);
2249                       return;
2250                     }
2251                   if (level <= olevel)
2252                     n = 0;
2253                 }
2254             }
2255           if (solv->weaksystemrules)
2256             {
2257               POOL_DEBUG(SAT_DEBUG_STATS, "installing weak system packages\n");
2258               for (i = solv->installed->start; i < solv->installed->end; i++)
2259                 {
2260                   if (pool->solvables[i].repo != solv->installed)
2261                     continue;
2262                   if (solv->decisionmap[i] > 0 || (solv->decisionmap[i] < 0 && solv->weaksystemrules[i - solv->installed->start] == 0))
2263                     continue;
2264                   /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2265                   if (MAPTST(&solv->noupdate, i - solv->installed->start))
2266                     continue;
2267                   queue_empty(&dq);
2268                   if (solv->weaksystemrules[i - solv->installed->start])
2269                     {
2270                       dp = pool->whatprovidesdata + solv->weaksystemrules[i - solv->installed->start];
2271                       while ((p = *dp++) != 0)
2272                         {
2273                           if (solv->decisionmap[p] > 0)
2274                             break;
2275                           if (solv->decisionmap[p] == 0)
2276                             queue_push(&dq, p);
2277                         }
2278                       if (p)
2279                         continue;       /* update package already installed */
2280                     }
2281                   if (!dq.count && solv->decisionmap[i] != 0)
2282                     continue;
2283                   olevel = level;
2284                   /* FIXME: i is handled a bit different because we do not want
2285                    * to have it pruned just because it is not recommened.
2286                    * we should not prune installed packages instead */
2287                   level = selectandinstall(solv, level, &dq, (solv->decisionmap[i] ? 0 : i), disablerules);
2288                   if (level == 0)
2289                     {
2290                       queue_free(&dq);
2291                       return;
2292                     }
2293                   if (level <= olevel)
2294                     break;
2295                 }
2296               if (i < solv->installed->end)
2297                 continue;
2298             }
2299           systemlevel = level;
2300         }
2301
2302       /*
2303        * decide
2304        */
2305
2306       POOL_DEBUG(SAT_DEBUG_STATS, "deciding unresolved rules\n");
2307       for (i = 1, n = 1; ; i++, n++)
2308         {
2309           if (n == solv->nrules)
2310             break;
2311           if (i == solv->nrules)
2312             i = 1;
2313           r = solv->rules + i;
2314           if (!r->w1)   /* ignore disabled rules */
2315             continue;
2316           queue_empty(&dq);
2317           if (r->d == 0)
2318             {
2319               /* binary or unary rule */
2320               /* need two positive undecided literals */
2321               if (r->p < 0 || r->w2 <= 0)
2322                 continue;
2323               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2324                 continue;
2325               queue_push(&dq, r->p);
2326               queue_push(&dq, r->w2);
2327             }
2328           else
2329             {
2330               /* make sure that
2331                * all negative literals are installed
2332                * no positive literal is installed
2333                * i.e. the rule is not fulfilled and we
2334                * just need to decide on the positive literals
2335                */
2336               if (r->p < 0)
2337                 {
2338                   if (solv->decisionmap[-r->p] <= 0)
2339                     continue;
2340                 }
2341               else
2342                 {
2343                   if (solv->decisionmap[r->p] > 0)
2344                     continue;
2345                   if (solv->decisionmap[r->p] == 0)
2346                     queue_push(&dq, r->p);
2347                 }
2348               dp = pool->whatprovidesdata + r->d;
2349               while ((p = *dp++) != 0)
2350                 {
2351                   if (p < 0)
2352                     {
2353                       if (solv->decisionmap[-p] <= 0)
2354                         break;
2355                     }
2356                   else
2357                     {
2358                       if (solv->decisionmap[p] > 0)
2359                         break;
2360                       if (solv->decisionmap[p] == 0)
2361                         queue_push(&dq, p);
2362                     }
2363                 }
2364               if (p)
2365                 continue;
2366             }
2367           /* dq.count < 2 cannot happen as this means that
2368            * the rule is unit */
2369           assert(dq.count > 1);
2370           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
2371             {
2372               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
2373               printrule(solv, SAT_DEBUG_PROPAGATE, r);
2374             }
2375
2376           olevel = level;
2377           level = selectandinstall(solv, level, &dq, 0, disablerules);
2378           if (level == 0)
2379             {
2380               queue_free(&dq);
2381               return;
2382             }
2383           if (level < systemlevel)
2384             break;
2385           n = 0;
2386         } /* for(), decide */
2387
2388       if (n != solv->nrules)    /* continue if level < systemlevel */
2389         continue;
2390
2391       if (doweak && !solv->problems.count)
2392         {
2393           int qcount;
2394
2395           POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended packages\n");
2396           if (!solv->dosplitprovides && !REGARD_RECOMMENDS_OF_INSTALLED_ITEMS)
2397             {
2398               for (i = 1; i < solv->decisionq.count; i++)
2399                 {
2400                   p = solv->decisionq.elements[i];
2401                   if (p > 0 && pool->solvables[p].repo == solv->installed)
2402                     solv->decisionmap[p] = -solv->decisionmap[p];
2403                 }
2404             }
2405           queue_empty(&dq);
2406           for (i = 1; i < pool->nsolvables; i++)
2407             {
2408               if (solv->decisionmap[i] < 0)
2409                 continue;
2410               if (solv->decisionmap[i] > 0)
2411                 {
2412                   Id *recp, rec, *pp, p;
2413                   s = pool->solvables + i;
2414                   /* installed, check for recommends */
2415                   /* XXX need to special case AND ? */
2416                   if (s->recommends)
2417                     {
2418                       recp = s->repo->idarraydata + s->recommends;
2419                       while ((rec = *recp++) != 0)
2420                         {
2421                           qcount = dq.count;
2422                           FOR_PROVIDES(p, pp, rec)
2423                             {
2424                               if (solv->decisionmap[p] > 0)
2425                                 {
2426                                   dq.count = qcount;
2427                                   break;
2428                                 }
2429                               else if (solv->decisionmap[p] == 0)
2430                                 {
2431                                   queue_pushunique(&dq, p);
2432                                 }
2433                             }
2434                         }
2435                     }
2436                 }
2437               else
2438                 {
2439                   s = pool->solvables + i;
2440                   if (!s->supplements && !s->freshens)
2441                     continue;
2442                   if (!pool_installable(pool, s))
2443                     continue;
2444                   if (solver_is_supplementing(solv, s))
2445                     queue_pushunique(&dq, i);
2446                 }
2447             }
2448           if (!solv->dosplitprovides && !REGARD_RECOMMENDS_OF_INSTALLED_ITEMS)
2449             {
2450               for (i = 1; i < solv->decisionq.count; i++)
2451                 {
2452                   p = solv->decisionq.elements[i];
2453                   if (p > 0 && pool->solvables[p].repo == solv->installed)
2454                     solv->decisionmap[p] = -solv->decisionmap[p];
2455                 }
2456             }
2457           if (dq.count)
2458             {
2459               if (dq.count > 1)
2460                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2461               p = dq.elements[0];
2462               POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2463               level = setpropagatelearn(solv, level, p, 0);
2464               continue;
2465             }
2466         }
2467
2468      if (solv->solution_callback)
2469         {
2470           solv->solution_callback(solv, solv->solution_callback_data);
2471           if (solv->branches.count)
2472             {
2473               int i = solv->branches.count - 1;
2474               int l = -solv->branches.elements[i];
2475               for (; i > 0; i--)
2476                 if (solv->branches.elements[i - 1] < 0)
2477                   break;
2478               p = solv->branches.elements[i];
2479               POOL_DEBUG(SAT_DEBUG_STATS, "branching with %s\n", solvable2str(pool, pool->solvables + p));
2480               queue_empty(&dq);
2481               for (j = i + 1; j < solv->branches.count; j++)
2482                 queue_push(&dq, solv->branches.elements[j]);
2483               solv->branches.count = i;
2484               level = l;
2485               revert(solv, level);
2486               if (dq.count > 1)
2487                 for (j = 0; j < dq.count; j++)
2488                   queue_push(&solv->branches, dq.elements[j]);
2489               olevel = level;
2490               level = setpropagatelearn(solv, level, p, disablerules);
2491               if (level == 0)
2492                 {
2493                   queue_free(&dq);
2494                   return;
2495                 }
2496               continue;
2497             }
2498           /* all branches done, we're finally finished */
2499           break;
2500         }
2501
2502       /* minimization step */
2503      if (solv->branches.count)
2504         {
2505           int l = 0, lasti = -1, lastl = -1;
2506           p = 0;
2507           for (i = solv->branches.count - 1; i >= 0; i--)
2508             {
2509               p = solv->branches.elements[i];
2510               if (p < 0)
2511                 l = -p;
2512               else if (p > 0 && solv->decisionmap[p] > l + 1)
2513                 {
2514                   lasti = i;
2515                   lastl = l;
2516                 }
2517             }
2518           if (lasti >= 0)
2519             {
2520               /* kill old solvable so that we do not loop */
2521               p = solv->branches.elements[lasti];
2522               solv->branches.elements[lasti] = 0;
2523               POOL_DEBUG(SAT_DEBUG_STATS, "minimizing %d -> %d with %s\n", solv->decisionmap[p], l, solvable2str(pool, pool->solvables + p));
2524
2525               level = lastl;
2526               revert(solv, level);
2527               olevel = level;
2528               level = setpropagatelearn(solv, level, p, disablerules);
2529               if (level == 0)
2530                 {
2531                   queue_free(&dq);
2532                   return;
2533                 }
2534               continue;
2535             }
2536         }
2537       break;
2538     }
2539   queue_free(&dq);
2540 }
2541
2542
2543 /*
2544  * refine_suggestion
2545  * at this point, all rules that led to conflicts are disabled.
2546  * we re-enable all rules of a problem set but rule "sug", then
2547  * continue to disable more rules until there as again a solution.
2548  */
2549
2550 /* FIXME: think about conflicting assertions */
2551
2552 static void
2553 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2554 {
2555   Pool *pool = solv->pool;
2556   Rule *r;
2557   int i, j;
2558   Id v;
2559   Queue disabled;
2560   int disabledcnt;
2561
2562   IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2563     {
2564       POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
2565       for (i = 0; problem[i]; i++)
2566         {
2567           if (problem[i] == sug)
2568             POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
2569           printproblem(solv, problem[i]);
2570         }
2571     }
2572   queue_init(&disabled);
2573   queue_empty(refined);
2574   queue_push(refined, sug);
2575
2576   /* re-enable all problem rules with the exception of "sug"(gests) */
2577   revert(solv, 1);
2578   reset_solver(solv);
2579
2580   for (i = 0; problem[i]; i++)
2581     if (problem[i] != sug)
2582       enableproblem(solv, problem[i]);
2583
2584   if (sug < 0)
2585     disableupdaterules(solv, job, -(sug + 1));
2586
2587   for (;;)
2588     {
2589       /* re-enable as many weak rules as possible */
2590       for (i = solv->weakrules; i < solv->learntrules; i++)
2591         {
2592           r = solv->rules + i;
2593           if (!r->w1)
2594             enablerule(solv, r);
2595         }
2596
2597       queue_empty(&solv->problems);
2598       revert(solv, 1);          /* XXX move to reset_solver? */
2599       reset_solver(solv);
2600
2601       if (!solv->problems.count)
2602         run_solver(solv, 0, 0);
2603
2604       if (!solv->problems.count)
2605         {
2606           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
2607           IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2608             printdecisions(solv);
2609           break;                /* great, no more problems */
2610         }
2611       disabledcnt = disabled.count;
2612       /* start with 1 to skip over proof index */
2613       for (i = 1; i < solv->problems.count - 1; i++)
2614         {
2615           /* ignore solutions in refined */
2616           v = solv->problems.elements[i];
2617           if (v == 0)
2618             break;      /* end of problem reached */
2619           for (j = 0; problem[j]; j++)
2620             if (problem[j] != sug && problem[j] == v)
2621               break;
2622           if (problem[j])
2623             continue;
2624           queue_push(&disabled, v);
2625         }
2626       if (disabled.count == disabledcnt)
2627         {
2628           /* no solution found, this was an invalid suggestion! */
2629           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
2630           refined->count = 0;
2631           break;
2632         }
2633       if (disabled.count == disabledcnt + 1)
2634         {
2635           /* just one suggestion, add it to refined list */
2636           v = disabled.elements[disabledcnt];
2637           queue_push(refined, v);
2638           disableproblem(solv, v);
2639           if (v < 0)
2640             disableupdaterules(solv, job, -(v + 1));
2641         }
2642       else
2643         {
2644           /* more than one solution, disable all */
2645           /* do not push anything on refine list */
2646           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2647             {
2648               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
2649               for (i = disabledcnt; i < disabled.count; i++)
2650                 printproblem(solv, disabled.elements[i]);
2651             }
2652           for (i = disabledcnt; i < disabled.count; i++)
2653             disableproblem(solv, disabled.elements[i]);
2654         }
2655     }
2656   /* all done, get us back into the same state as before */
2657   /* enable refined rules again */
2658   for (i = 0; i < disabled.count; i++)
2659     enableproblem(solv, disabled.elements[i]);
2660   /* disable problem rules again */
2661   for (i = 0; problem[i]; i++)
2662     disableproblem(solv, problem[i]);
2663   disableupdaterules(solv, job, -1);
2664   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
2665 }
2666
2667 static void
2668 problems_to_solutions(Solver *solv, Queue *job)
2669 {
2670   Pool *pool = solv->pool;
2671   Queue problems;
2672   Queue solution;
2673   Queue solutions;
2674   Id *problem;
2675   Id why;
2676   int i, j;
2677
2678   if (!solv->problems.count)
2679     return;
2680   queue_clone(&problems, &solv->problems);
2681   queue_init(&solution);
2682   queue_init(&solutions);
2683   /* copy over proof index */
2684   queue_push(&solutions, problems.elements[0]);
2685   problem = problems.elements + 1;
2686   for (i = 1; i < problems.count; i++)
2687     {
2688       Id v = problems.elements[i];
2689       if (v == 0)
2690         {
2691           /* mark end of this problem */
2692           queue_push(&solutions, 0);
2693           queue_push(&solutions, 0);
2694           if (i + 1 == problems.count)
2695             break;
2696           /* copy over proof of next problem */
2697           queue_push(&solutions, problems.elements[i + 1]);
2698           i++;
2699           problem = problems.elements + i + 1;
2700           continue;
2701         }
2702       refine_suggestion(solv, job, problem, v, &solution);
2703       if (!solution.count)
2704         continue;       /* this solution didn't work out */
2705
2706       for (j = 0; j < solution.count; j++)
2707         {
2708           why = solution.elements[j];
2709           /* must be either job descriptor or system rule */
2710           assert(why < 0 || (why >= solv->systemrules && why < solv->weakrules));
2711 #if 0
2712           printproblem(solv, why);
2713 #endif
2714           if (why < 0)
2715             {
2716               /* job descriptor */
2717               queue_push(&solutions, 0);
2718               queue_push(&solutions, -why);
2719             }
2720           else
2721             {
2722               /* system rule, find replacement package */
2723               Id p, rp = 0;
2724               p = solv->installed->start + (why - solv->systemrules);
2725               if (solv->weaksystemrules && solv->weaksystemrules[why - solv->systemrules])
2726                 {
2727                   Id *dp = pool->whatprovidesdata + solv->weaksystemrules[why - solv->systemrules];
2728                   for (; *dp; dp++)
2729                     {
2730                       if (*dp >= solv->installed->start && *dp < solv->installed->start + solv->installed->nsolvables)
2731                         continue;
2732                       if (solv->decisionmap[*dp] > 0)
2733                         {
2734                           rp = *dp;
2735                           break;
2736                         }
2737                     }
2738                 }
2739               queue_push(&solutions, p);
2740               queue_push(&solutions, rp);
2741             }
2742         }
2743       /* mark end of this solution */
2744       queue_push(&solutions, 0);
2745       queue_push(&solutions, 0);
2746     }
2747   queue_free(&solution);
2748   queue_free(&problems);
2749   /* copy queue over to solutions */
2750   queue_free(&solv->problems);
2751   queue_clone(&solv->problems, &solutions);
2752
2753   /* bring solver back into problem state */
2754   revert(solv, 1);              /* XXX move to reset_solver? */
2755   reset_solver(solv);
2756
2757   assert(solv->problems.count == solutions.count);
2758   queue_free(&solutions);
2759 }
2760
2761 Id
2762 solver_next_problem(Solver *solv, Id problem)
2763 {
2764   Id *pp;
2765   if (problem == 0)
2766     return solv->problems.count ? 1 : 0;
2767   pp = solv->problems.elements + problem;
2768   while (pp[0] || pp[1])
2769     {
2770       /* solution */
2771       pp += 2;
2772       while (pp[0] || pp[1])
2773         pp += 2;
2774       pp += 2;
2775     }
2776   pp += 2;
2777   problem = pp - solv->problems.elements;
2778   if (problem >= solv->problems.count)
2779     return 0;
2780   return problem + 1;
2781 }
2782
2783 Id
2784 solver_next_solution(Solver *solv, Id problem, Id solution)
2785 {
2786   Id *pp;
2787   if (solution == 0)
2788     {
2789       solution = problem;
2790       pp = solv->problems.elements + solution;
2791       return pp[0] || pp[1] ? solution : 0;
2792     }
2793   pp = solv->problems.elements + solution;
2794   while (pp[0] || pp[1])
2795     pp += 2;
2796   pp += 2;
2797   solution = pp - solv->problems.elements;
2798   return pp[0] || pp[1] ? solution : 0;
2799 }
2800
2801 Id
2802 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
2803 {
2804   Id *pp;
2805   element = element ? element + 2 : solution;
2806   pp = solv->problems.elements + element;
2807   if (!(pp[0] || pp[1]))
2808     return 0;
2809   *p = pp[0];
2810   *rp = pp[1];
2811   return element;
2812 }
2813
2814
2815 /*
2816  * create obsoletesmap from solver decisions
2817  * required for decision handling
2818  */
2819
2820 Id *
2821 create_decisions_obsoletesmap(Solver *solv)
2822 {
2823   Pool *pool = solv->pool;
2824   Repo *installed = solv->installed;
2825   Id p, *obsoletesmap = NULL;
2826   int i;
2827   Solvable *s;
2828
2829   obsoletesmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
2830   if (installed)
2831     {
2832       for (i = 0; i < solv->decisionq.count; i++)
2833         {
2834           Id *pp, n;
2835
2836           n = solv->decisionq.elements[i];
2837           if (n < 0)
2838             continue;
2839           if (n == SYSTEMSOLVABLE)
2840             continue;
2841           s = pool->solvables + n;
2842           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2843             continue;
2844           FOR_PROVIDES(p, pp, s->name)
2845             if (s->name == pool->solvables[p].name)
2846               {
2847                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2848                   {
2849                     obsoletesmap[p] = n;
2850                     obsoletesmap[n]++;
2851                   }
2852               }
2853         }
2854       for (i = 0; i < solv->decisionq.count; i++)
2855         {
2856           Id obs, *obsp;
2857           Id *pp, n;
2858
2859           n = solv->decisionq.elements[i];
2860           if (n < 0)
2861             continue;
2862           if (n == SYSTEMSOLVABLE)
2863             continue;
2864           s = pool->solvables + n;
2865           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2866             continue;
2867           if (!s->obsoletes)
2868             continue;
2869           obsp = s->repo->idarraydata + s->obsoletes;
2870           while ((obs = *obsp++) != 0)
2871             FOR_PROVIDES(p, pp, obs)
2872               {
2873                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2874                   {
2875                     obsoletesmap[p] = n;
2876                     obsoletesmap[n]++;
2877                   }
2878               }
2879         }
2880     }
2881   return obsoletesmap;
2882 }
2883
2884 /*
2885  * printdecisions
2886  */
2887
2888
2889 void
2890 printdecisions(Solver *solv)
2891 {
2892   Pool *pool = solv->pool;
2893   Repo *installed = solv->installed;
2894   Id p, *obsoletesmap = create_decisions_obsoletesmap( solv );
2895   int i;
2896   Solvable *s;
2897
2898   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- Decisions -----\n");
2899
2900   /* print solvables to be erased */
2901
2902   if (installed)
2903     {
2904       FOR_REPO_SOLVABLES(installed, p, s)
2905         {
2906           if (solv->decisionmap[p] >= 0)
2907             continue;
2908           if (obsoletesmap[p])
2909             continue;
2910           POOL_DEBUG(SAT_DEBUG_RESULT, "erase   %s\n", solvable2str(pool, s));
2911         }
2912     }
2913
2914   /* print solvables to be installed */
2915
2916   for (i = 0; i < solv->decisionq.count; i++)
2917     {
2918       int j;
2919       p = solv->decisionq.elements[i];
2920       if (p < 0)
2921         {
2922             IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2923             {
2924               p = -p;
2925               s = pool->solvables + p;
2926               POOL_DEBUG(SAT_DEBUG_SCHUBI, "level of %s is %d\n", solvable2str(pool, s), p);
2927             }
2928             continue;
2929         }
2930       if (p == SYSTEMSOLVABLE)
2931         {
2932             POOL_DEBUG(SAT_DEBUG_SCHUBI, "SYSTEMSOLVABLE\n");
2933             continue;
2934         }
2935       s = pool->solvables + p;
2936       if (installed && s->repo == installed)
2937         continue;
2938
2939       if (!obsoletesmap[p])
2940         {
2941           POOL_DEBUG(SAT_DEBUG_RESULT, "install %s", solvable2str(pool, s));
2942         }
2943       else
2944         {
2945           POOL_DEBUG(SAT_DEBUG_RESULT, "update  %s", solvable2str(pool, s));
2946           POOL_DEBUG(SAT_DEBUG_RESULT, "  (obsoletes");
2947           for (j = installed->start; j < installed->end; j++)
2948             if (obsoletesmap[j] == p)
2949               POOL_DEBUG(SAT_DEBUG_RESULT, " %s", solvable2str(pool, pool->solvables + j));
2950           POOL_DEBUG(SAT_DEBUG_RESULT, ")");
2951         }
2952       POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
2953     }
2954
2955   sat_free(obsoletesmap);
2956
2957   if (solv->suggestions.count)
2958     {
2959       POOL_DEBUG(SAT_DEBUG_RESULT, "\nsuggested packages:\n");
2960       for (i = 0; i < solv->suggestions.count; i++)
2961         {
2962           s = pool->solvables + solv->suggestions.elements[i];
2963           POOL_DEBUG(SAT_DEBUG_RESULT, "- %s\n", solvable2str(pool, s));
2964         }
2965     }
2966   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- Decisions end -----\n");
2967 }
2968
2969 /* this is basically the reverse of addrpmrulesforsolvable */
2970 SolverProbleminfo
2971 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
2972 {
2973   Pool *pool = solv->pool;
2974   Repo *installed = solv->installed;
2975   Rule *r;
2976   Solvable *s;
2977   int dontfix = 0;
2978   Id p, *pp, req, *reqp, con, *conp, obs, *obsp, *dp;
2979
2980   assert(rid < solv->weakrules);
2981   if (rid >= solv->systemrules)
2982     {
2983       *depp = 0;
2984       *sourcep = solv->installed->start + (rid - solv->systemrules);
2985       *targetp = 0;
2986       return SOLVER_PROBLEM_UPDATE_RULE;
2987     }
2988   if (rid >= solv->jobrules)
2989     {
2990
2991       r = solv->rules + rid;
2992       p = solv->ruletojob.elements[rid - solv->jobrules];
2993       *depp = job->elements[p + 1];
2994       *sourcep = p;
2995       *targetp = job->elements[p];
2996       if (r->d == 0 && r->w2 == 0 && r->p == -SYSTEMSOLVABLE)
2997         return SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP;
2998       return SOLVER_PROBLEM_JOB_RULE;
2999     }
3000   if (rid < 0)
3001     {
3002       /* a rpm rule assertion */
3003       assert(rid != -SYSTEMSOLVABLE);
3004       s = pool->solvables - rid;
3005       if (installed && !solv->fixsystem && s->repo == installed)
3006         dontfix = 1;
3007       assert(!dontfix); /* dontfix packages never have a neg assertion */
3008       /* see why the package is not installable */
3009       if (s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
3010         {
3011           *depp = 0;
3012           *sourcep = -rid;
3013           *targetp = 0;
3014           return SOLVER_PROBLEM_NOT_INSTALLABLE;
3015         }
3016       /* check requires */
3017       assert(s->requires);
3018       reqp = s->repo->idarraydata + s->requires;
3019       while ((req = *reqp++) != 0)
3020         {
3021           if (req == SOLVABLE_PREREQMARKER)
3022             continue;
3023           dp = pool_whatprovides(pool, req);
3024           if (*dp == 0)
3025             break;
3026         }
3027       assert(req);
3028       *depp = req;
3029       *sourcep = -rid;
3030       *targetp = 0;
3031       return SOLVER_PROBLEM_NOTHING_PROVIDES_DEP;
3032     }
3033   r = solv->rules + rid;
3034   assert(r->p < 0);
3035   if (r->d == 0 && r->w2 == 0)
3036     {
3037       /* an assertion. we don't store them as rpm rules, so
3038        * can't happen */
3039       assert(0);
3040     }
3041   s = pool->solvables - r->p;
3042   if (installed && !solv->fixsystem && s->repo == installed)
3043     dontfix = 1;
3044   if (r->d == 0 && r->w2 < 0)
3045     {
3046       /* a package conflict */
3047       Solvable *s2 = pool->solvables - r->w2;
3048       int dontfix2 = 0;
3049
3050       if (installed && !solv->fixsystem && s2->repo == installed)
3051         dontfix2 = 1;
3052
3053       /* if both packages have the same name and at least one of them
3054        * is not installed, they conflict */
3055       if (s->name == s2->name && (!installed || (s->repo != installed || s2->repo != installed)))
3056         {
3057           *depp = 0;
3058           *sourcep = -r->p;
3059           *targetp = -r->w2;
3060           return SOLVER_PROBLEM_SAME_NAME;
3061         }
3062
3063       /* check conflicts in both directions */
3064       if (s->conflicts)
3065         {
3066           conp = s->repo->idarraydata + s->conflicts;
3067           while ((con = *conp++) != 0)
3068             {
3069               FOR_PROVIDES(p, pp, con)
3070                 {
3071                   if (dontfix && pool->solvables[p].repo == installed)
3072                     continue;
3073                   if (p != -r->w2)
3074                     continue;
3075                   *depp = con;
3076                   *sourcep = -r->p;
3077                   *targetp = p;
3078                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3079                 }
3080             }
3081         }
3082       if (s2->conflicts)
3083         {
3084           conp = s2->repo->idarraydata + s2->conflicts;
3085           while ((con = *conp++) != 0)
3086             {
3087               FOR_PROVIDES(p, pp, con)
3088                 {
3089                   if (dontfix2 && pool->solvables[p].repo == installed)
3090                     continue;
3091                   if (p != -r->p)
3092                     continue;
3093                   *depp = con;
3094                   *sourcep = -r->w2;
3095                   *targetp = p;
3096                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3097                 }
3098             }
3099         }
3100       /* check obsoletes in both directions */
3101       if ((!installed || s->repo != installed) && s->obsoletes)
3102         {
3103           obsp = s->repo->idarraydata + s->obsoletes;
3104           while ((obs = *obsp++) != 0)
3105             {
3106               FOR_PROVIDES(p, pp, obs)
3107                 {
3108                   if (p != -r->w2)
3109                     continue;
3110                   *depp = obs;
3111                   *sourcep = -r->p;
3112                   *targetp = p;
3113                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3114                 }
3115             }
3116         }
3117       if ((!installed || s2->repo != installed) && s2->obsoletes)
3118         {
3119           obsp = s2->repo->idarraydata + s2->obsoletes;
3120           while ((obs = *obsp++) != 0)
3121             {
3122               FOR_PROVIDES(p, pp, obs)
3123                 {
3124                   if (p != -r->p)
3125                     continue;
3126                   *depp = obs;
3127                   *sourcep = -r->w2;
3128                   *targetp = p;
3129                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3130                 }
3131             }
3132         }
3133       /* all cases checked, can't happen */
3134       assert(0);
3135     }
3136   /* simple requires */
3137   assert(s->requires);
3138   reqp = s->repo->idarraydata + s->requires;
3139   while ((req = *reqp++) != 0)
3140     {
3141       if (req == SOLVABLE_PREREQMARKER)
3142         continue;
3143       dp = pool_whatprovides(pool, req);
3144       if (r->d == 0)
3145         {
3146           if (*dp == r->w2 && dp[1] == 0)
3147             break;
3148         }
3149       else if (dp - pool->whatprovidesdata == r->d)
3150         break;
3151     }
3152   assert(req);
3153   *depp = req;
3154   *sourcep = -r->p;
3155   *targetp = 0;
3156   return SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE;
3157 }
3158
3159 static void
3160 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
3161 {
3162   Id rid;
3163   Id lreqr, lconr, lsysr, ljobr;
3164   Rule *r;
3165   int reqassert = 0;
3166
3167   lreqr = lconr = lsysr = ljobr = 0;
3168   while ((rid = solv->learnt_pool.elements[idx++]) != 0)
3169     {
3170       if (rid >= solv->learntrules)
3171         findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
3172       else if (rid >= solv->systemrules)
3173         {
3174           if (!*sysrp)
3175             *sysrp = rid;
3176         }
3177       else if (rid >= solv->jobrules)
3178         {
3179           if (!*jobrp)
3180             *jobrp = rid;
3181         }
3182       else if (rid >= 0)
3183         {
3184           r = solv->rules + rid;
3185           if (!r->d && r->w2 < 0)
3186             {
3187               if (!*conrp)
3188                 *conrp = rid;
3189             }
3190           else
3191             {
3192               if (!*reqrp)
3193                 *reqrp = rid;
3194             }
3195         }
3196       else
3197         {
3198           /* assertion, counts as require rule */
3199           /* ignore system solvable as we need useful info */
3200           if (rid == -SYSTEMSOLVABLE)
3201             continue;
3202           if (!*reqrp || !reqassert)
3203             {
3204               *reqrp = rid;
3205               reqassert = 1;
3206             }
3207         }
3208     }
3209   if (!*reqrp && lreqr)
3210     *reqrp = lreqr;
3211   if (!*conrp && lconr)
3212     *conrp = lconr;
3213   if (!*jobrp && ljobr)
3214     *jobrp = ljobr;
3215   if (!*sysrp && lsysr)
3216     *sysrp = lsysr;
3217 }
3218
3219 Id
3220 solver_findproblemrule(Solver *solv, Id problem)
3221 {
3222   Id reqr, conr, sysr, jobr;
3223   Id idx = solv->problems.elements[problem - 1];
3224   reqr = conr = sysr = jobr = 0;
3225   findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
3226   if (reqr)
3227     return reqr;
3228   if (conr)
3229     return conr;
3230   if (sysr)
3231     return sysr;
3232   if (jobr)
3233     return jobr;
3234   assert(0);
3235 }
3236
3237 void
3238 printprobleminfo(Solver *solv, Queue *job, Id problem)
3239 {
3240   Pool *pool = solv->pool;
3241   Id probr;
3242   Id dep, source, target;
3243   Solvable *s, *s2;
3244
3245   probr = solver_findproblemrule(solv, problem);
3246   switch (solver_problemruleinfo(solv, job, probr, &dep, &source, &target))
3247     {
3248     case SOLVER_PROBLEM_UPDATE_RULE:
3249       s = pool_id2solvable(pool, source);
3250       POOL_DEBUG(SAT_DEBUG_RESULT, "problem with installed package %s\n", solvable2str(pool, s));
3251       return;
3252     case SOLVER_PROBLEM_JOB_RULE:
3253       POOL_DEBUG(SAT_DEBUG_RESULT, "conflicting requests\n");
3254       return;
3255     case SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP:
3256       POOL_DEBUG(SAT_DEBUG_RESULT, "nothing provides requested %s\n", dep2str(pool, dep));
3257       return;
3258     case SOLVER_PROBLEM_NOT_INSTALLABLE:
3259       s = pool_id2solvable(pool, source);
3260       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s is not installable\n", solvable2str(pool, s));
3261       return;
3262     case SOLVER_PROBLEM_NOTHING_PROVIDES_DEP:
3263       s = pool_id2solvable(pool, source);
3264       POOL_DEBUG(SAT_DEBUG_RESULT, "nothing provides %s needed by %s\n", dep2str(pool, dep), solvable2str(pool, s));
3265       return;
3266     case SOLVER_PROBLEM_SAME_NAME:
3267       s = pool_id2solvable(pool, source);
3268       s2 = pool_id2solvable(pool, target);
3269       POOL_DEBUG(SAT_DEBUG_RESULT, "cannot install both %s and %s\n", solvable2str(pool, s), solvable2str(pool, s2));
3270       return;
3271     case SOLVER_PROBLEM_PACKAGE_CONFLICT:
3272       s = pool_id2solvable(pool, source);
3273       s2 = pool_id2solvable(pool, target);
3274       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s conflicts with %s provided by %s\n", solvable2str(pool, s), dep2str(pool, dep), solvable2str(pool, s2));
3275       return;
3276     case SOLVER_PROBLEM_PACKAGE_OBSOLETES:
3277       s = pool_id2solvable(pool, source);
3278       s2 = pool_id2solvable(pool, target);
3279       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s obsoletes %s provided by %s\n", solvable2str(pool, s), dep2str(pool, dep), solvable2str(pool, s2));
3280       return;
3281     case SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE:
3282       s = pool_id2solvable(pool, source);
3283       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s requires %s, but none of the providers can be installed\n", solvable2str(pool, s), dep2str(pool, dep));
3284       return;
3285     }
3286 }
3287
3288 void
3289 printsolutions(Solver *solv, Queue *job)
3290 {
3291   Pool *pool = solv->pool;
3292   int pcnt;
3293   Id p, rp, what;
3294   Id problem, solution, element;
3295   Solvable *s, *sd;
3296
3297   POOL_DEBUG(SAT_DEBUG_RESULT, "Encountered problems! Here are the solutions:\n\n");
3298   pcnt = 1;
3299   problem = 0;
3300   while ((problem = solver_next_problem(solv, problem)) != 0)
3301     {
3302       POOL_DEBUG(SAT_DEBUG_RESULT, "Problem %d:\n", pcnt++);
3303       POOL_DEBUG(SAT_DEBUG_RESULT, "====================================\n");
3304       printprobleminfo(solv, job, problem);
3305       POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
3306       solution = 0;
3307       while ((solution = solver_next_solution(solv, problem, solution)) != 0)
3308         {
3309           element = 0;
3310           while ((element = solver_next_solutionelement(solv, problem, solution, element, &p, &rp)) != 0)
3311             {
3312               if (p == 0)
3313                 {
3314                   /* job, rp is index into job queue */
3315                   what = job->elements[rp];
3316                   switch (job->elements[rp - 1])
3317                     {
3318                     case SOLVER_INSTALL_SOLVABLE:
3319                       s = pool->solvables + what;
3320                       if (solv->installed && s->repo == solv->installed)
3321                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not keep %s installed\n", solvable2str(pool, s));
3322                       else
3323                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install %s\n", solvable2str(pool, s));
3324                       break;
3325                     case SOLVER_ERASE_SOLVABLE:
3326                       s = pool->solvables + what;
3327                       if (solv->installed && s->repo == solv->installed)
3328                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall %s\n", solvable2str(pool, s));
3329                       else
3330                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not forbid installation of %s\n", solvable2str(pool, s));
3331                       break;
3332                     case SOLVER_INSTALL_SOLVABLE_NAME:
3333                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install %s\n", id2str(pool, what));
3334                       break;
3335                     case SOLVER_ERASE_SOLVABLE_NAME:
3336                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall %s\n", id2str(pool, what));
3337                       break;
3338                     case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3339                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install a solvable providing %s\n", dep2str(pool, what));
3340                       break;
3341                     case SOLVER_ERASE_SOLVABLE_PROVIDES:
3342                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall all solvables providing %s\n", dep2str(pool, what));
3343                       break;
3344                     case SOLVER_INSTALL_SOLVABLE_UPDATE:
3345                       s = pool->solvables + what;
3346                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install most recent version of %s\n", solvable2str(pool, s));
3347                       break;
3348                     default:
3349                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do something different\n");
3350                       break;
3351                     }
3352                 }
3353               else
3354                 {
3355                   /* policy, replace p with rp */
3356                   s = pool->solvables + p;
3357                   sd = rp ? pool->solvables + rp : 0;
3358                   if (sd)
3359                     {
3360                       int gotone = 0;
3361                       if (!solv->allowdowngrade && evrcmp(pool, s->evr, sd->evr, EVRCMP_MATCH_RELEASE) > 0)
3362                         {
3363                           POOL_DEBUG(SAT_DEBUG_RESULT, "- allow downgrade of %s to %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3364                           gotone = 1;
3365                         }
3366                       if (!solv->allowarchchange && s->name == sd->name && s->arch != sd->arch && policy_illegal_archchange(solv, s, sd))
3367                         {
3368                           POOL_DEBUG(SAT_DEBUG_RESULT, "- allow architecture change of %s to %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3369                           gotone = 1;
3370                         }
3371                       if (!solv->allowvendorchange && s->name == sd->name && s->vendor != sd->vendor && policy_illegal_vendorchange(solv, s, sd))
3372                         {
3373                           if (sd->vendor)
3374                             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));
3375                           else
3376                             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));
3377                           gotone = 1;
3378                         }
3379                       if (!gotone)
3380                         POOL_DEBUG(SAT_DEBUG_RESULT, "- allow replacement of %s with %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3381                     }
3382                   else
3383                     {
3384                       POOL_DEBUG(SAT_DEBUG_RESULT, "- allow deinstallation of %s\n", solvable2str(pool, s));
3385                     }
3386
3387                 }
3388             }
3389           POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
3390         }
3391     }
3392 }
3393
3394
3395 /* create reverse obsoletes map for installed solvables
3396  *
3397  * for each installed solvable find which packages with *different* names
3398  * obsolete the solvable.
3399  * this index is used in policy_findupdatepackages if noupdateprovide is set.
3400  */
3401
3402 static void
3403 create_obsolete_index(Solver *solv)
3404 {
3405   Pool *pool = solv->pool;
3406   Solvable *s;
3407   Repo *installed = solv->installed;
3408   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
3409   int i, n;
3410
3411   if (!installed || !installed->nsolvables)
3412     return;
3413   solv->obsoletes = obsoletes = sat_calloc(installed->end - installed->start, sizeof(Id));
3414   for (i = 1; i < pool->nsolvables; i++)
3415     {
3416       s = pool->solvables + i;
3417       if (s->repo == installed)
3418         continue;
3419       if (!s->obsoletes)
3420         continue;
3421       if (!pool_installable(pool, s))
3422         continue;
3423       obsp = s->repo->idarraydata + s->obsoletes;
3424       while ((obs = *obsp++) != 0)
3425         FOR_PROVIDES(p, pp, obs)
3426           {
3427             if (pool->solvables[p].repo != installed)
3428               continue;
3429             if (pool->solvables[p].name == s->name)
3430               continue;
3431             obsoletes[p - installed->start]++;
3432           }
3433     }
3434   n = 0;
3435   for (i = 0; i < installed->nsolvables; i++)
3436     if (obsoletes[i])
3437       {
3438         n += obsoletes[i] + 1;
3439         obsoletes[i] = n;
3440       }
3441   solv->obsoletes_data = obsoletes_data = sat_calloc(n + 1, sizeof(Id));
3442   POOL_DEBUG(SAT_DEBUG_STATS, "obsoletes data: %d entries\n", n + 1);
3443   for (i = pool->nsolvables - 1; i > 0; i--)
3444     {
3445       s = pool->solvables + i;
3446       if (s->repo == installed)
3447         continue;
3448       if (!s->obsoletes)
3449         continue;
3450       if (!pool_installable(pool, s))
3451         continue;
3452       obsp = s->repo->idarraydata + s->obsoletes;
3453       while ((obs = *obsp++) != 0)
3454         FOR_PROVIDES(p, pp, obs)
3455           {
3456             if (pool->solvables[p].repo != installed)
3457               continue;
3458             if (pool->solvables[p].name == s->name)
3459               continue;
3460             p -= installed->start;
3461             if (obsoletes_data[obsoletes[p]] != i)
3462               obsoletes_data[--obsoletes[p]] = i;
3463           }
3464     }
3465 }
3466
3467
3468 /*-----------------------------------------------------------------*/
3469 /* main() */
3470
3471 /*
3472  *
3473  * solve job queue
3474  *
3475  */
3476
3477 void
3478 solver_solve(Solver *solv, Queue *job)
3479 {
3480   Pool *pool = solv->pool;
3481   Repo *installed = solv->installed;
3482   int i;
3483   int oldnrules;
3484   Map addedmap;                /* '1' == have rpm-rules for solvable */
3485   Id how, what, p, *pp, d;
3486   Queue q;
3487   Solvable *s;
3488
3489   if (solv->limittokind != _KIND_MAX)  /* if application wants to limit, make it non-zero */
3490     solv->limittokind += 1;
3491   else
3492     solv->limittokind = 0;
3493
3494   /* create whatprovides if not already there */
3495   if (!pool->whatprovides)
3496     pool_createwhatprovides(pool);
3497
3498   /* create obsolete index if needed */
3499   if (solv->noupdateprovide)
3500     create_obsolete_index(solv);
3501
3502   /*
3503    * create basic rule set of all involved packages
3504    * use addedmap bitmap to make sure we don't create rules twice
3505    *
3506    */
3507
3508   map_init(&addedmap, pool->nsolvables);
3509   queue_init(&q);
3510
3511   /*
3512    * always install our system solvable
3513    */
3514   MAPSET(&addedmap, SYSTEMSOLVABLE);
3515   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
3516   queue_push(&solv->decisionq_why, 0);
3517   solv->decisionmap[SYSTEMSOLVABLE] = 1;
3518
3519   /*
3520    * create rules for all package that could be involved with the solving
3521    * so called: rpm rules
3522    *
3523    */
3524   if (installed)
3525     {
3526       oldnrules = solv->nrules;
3527       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
3528       FOR_REPO_SOLVABLES(installed, p, s)
3529         addrpmrulesforsolvable(solv, s, &addedmap);
3530       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
3531       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
3532       oldnrules = solv->nrules;
3533       FOR_REPO_SOLVABLES(installed, p, s)
3534         addrpmrulesforupdaters(solv, s, &addedmap, 1);
3535       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
3536     }
3537
3538   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
3539   oldnrules = solv->nrules;
3540   for (i = 0; i < job->count; i += 2)
3541     {
3542       how = job->elements[i];
3543       what = job->elements[i + 1];
3544
3545       switch(how)
3546         {
3547         case SOLVER_INSTALL_SOLVABLE:
3548           addrpmrulesforsolvable(solv, pool->solvables + what, &addedmap);
3549           break;
3550         case SOLVER_INSTALL_SOLVABLE_NAME:
3551         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3552           FOR_PROVIDES(p, pp, what)
3553             {
3554               /* if by name, ensure that the name matches */
3555               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3556                 continue;
3557               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3558             }
3559           break;
3560         case SOLVER_INSTALL_SOLVABLE_UPDATE:
3561           /* dont allow downgrade */
3562           addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
3563           break;
3564         }
3565     }
3566   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
3567
3568   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for recommended/suggested packages ***\n");
3569
3570   oldnrules = solv->nrules;
3571   addrpmrulesforweak(solv, &addedmap);
3572   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
3573
3574   IF_POOLDEBUG (SAT_DEBUG_STATS)
3575     {
3576       int possible = 0, installable = 0;
3577       for (i = 1; i < pool->nsolvables; i++)
3578         {
3579           if (pool_installable(pool, pool->solvables + i))
3580             installable++;
3581           if (MAPTST(&addedmap, i))
3582             possible++;
3583         }
3584       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving (rules has been generated for)\n", possible, installable);
3585     }
3586
3587   /*
3588    * first pass done, we now have all the rpm rules we need.
3589    * unify existing rules before going over all job rules and
3590    * policy rules.
3591    * at this point the system is always solvable,
3592    * as an empty system (remove all packages) is a valid solution
3593    */
3594
3595   unifyrules(solv);     /* remove duplicate rpm rules */
3596   solv->directdecisions = solv->decisionq.count;
3597
3598   POOL_DEBUG(SAT_DEBUG_STATS, "decisions so far: %d\n", solv->decisionq.count);
3599   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
3600     printdecisions (solv);
3601
3602   /*
3603    * now add all job rules
3604    */
3605
3606   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
3607
3608   solv->jobrules = solv->nrules;
3609
3610   for (i = 0; i < job->count; i += 2)
3611     {
3612       oldnrules = solv->nrules;
3613
3614       how = job->elements[i];
3615       what = job->elements[i + 1];
3616       switch(how)
3617         {
3618         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
3619           s = pool->solvables + what;
3620           POOL_DEBUG(SAT_DEBUG_JOB, "job: install solvable %s\n", solvable2str(pool, s));
3621           addrule(solv, what, 0);                       /* install by Id */
3622           queue_push(&solv->ruletojob, i);
3623           break;
3624         case SOLVER_ERASE_SOLVABLE:
3625           s = pool->solvables + what;
3626           POOL_DEBUG(SAT_DEBUG_JOB, "job: erase solvable %s\n", solvable2str(pool, s));
3627           addrule(solv, -what, 0);                      /* remove by Id */
3628           queue_push(&solv->ruletojob, i);
3629           break;
3630         case SOLVER_INSTALL_SOLVABLE_NAME:              /* install by capability */
3631         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3632           if (how == SOLVER_INSTALL_SOLVABLE_NAME)
3633             POOL_DEBUG(SAT_DEBUG_JOB, "job: install name %s\n", id2str(pool, what));
3634           if (how == SOLVER_INSTALL_SOLVABLE_PROVIDES)
3635             POOL_DEBUG(SAT_DEBUG_JOB, "job: install provides %s\n", dep2str(pool, what));
3636           queue_empty(&q);
3637           FOR_PROVIDES(p, pp, what)
3638             {
3639               /* if by name, ensure that the name matches */
3640               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3641                 continue;
3642               queue_push(&q, p);
3643             }
3644           if (!q.count)
3645             {
3646               /* no provider, make this an impossible rule */
3647               queue_push(&q, -SYSTEMSOLVABLE);
3648             }
3649
3650           p = queue_shift(&q);         /* get first provider */
3651           if (!q.count)
3652             d = 0;                     /* single provider ? -> make assertion */
3653           else
3654             d = pool_queuetowhatprovides(pool, &q);   /* get all providers */
3655           addrule(solv, p, d);         /* add 'requires' rule */
3656           queue_push(&solv->ruletojob, i);
3657           break;
3658         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
3659         case SOLVER_ERASE_SOLVABLE_PROVIDES:
3660           if (how == SOLVER_ERASE_SOLVABLE_NAME)
3661             POOL_DEBUG(SAT_DEBUG_JOB, "job: erase name %s\n", id2str(pool, what));
3662           if (how == SOLVER_ERASE_SOLVABLE_PROVIDES)
3663             POOL_DEBUG(SAT_DEBUG_JOB, "job: erase provides %s\n", dep2str(pool, what));
3664           FOR_PROVIDES(p, pp, what)
3665             {
3666               /* if by name, ensure that the name matches */
3667               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
3668                 continue;
3669               addrule(solv, -p, 0);  /* add 'remove' rule */
3670               queue_push(&solv->ruletojob, i);
3671             }
3672           break;
3673         case SOLVER_INSTALL_SOLVABLE_UPDATE:              /* find update for solvable */
3674           s = pool->solvables + what;
3675           POOL_DEBUG(SAT_DEBUG_JOB, "job: update %s\n", solvable2str(pool, s));
3676           addupdaterule(solv, s, 0);
3677           queue_push(&solv->ruletojob, i);
3678           break;
3679         }
3680       IF_POOLDEBUG (SAT_DEBUG_JOB)
3681         {
3682           int j;
3683           if (solv->nrules == oldnrules)
3684             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created");
3685           for (j = oldnrules; j < solv->nrules; j++)
3686             {
3687               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
3688               printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
3689             }
3690         }
3691     }
3692   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
3693
3694   /*
3695    * now add system rules
3696    *
3697    */
3698
3699   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add system rules ***\n");
3700
3701
3702   solv->systemrules = solv->nrules;
3703
3704   /*
3705    * create rules for updating installed solvables
3706    *
3707    */
3708
3709   if (installed && !solv->allowuninstall)
3710     {                                  /* loop over all installed solvables */
3711       /* we create all update rules, but disable some later on depending on the job */
3712       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3713         {
3714           /* no system rules for patch atoms */
3715           if (s->freshens && !s->supplements)
3716             {
3717               const char *name = id2str(pool, s->name);
3718               if (name[0] == 'a' && !strncmp(name, "atom:", 5))
3719                 {
3720                   addrule(solv, 0, 0);
3721                   continue;
3722                 }
3723             }
3724           if (s->repo == installed)
3725             addupdaterule(solv, s, 0);  /* allowall = 0 */
3726           else
3727             addrule(solv, 0, 0);        /* create dummy rule */
3728         }
3729       /* consistency check: we added a rule for _every_ system solvable */
3730       assert(solv->nrules - solv->systemrules == installed->end - installed->start);
3731     }
3732
3733   /* create special weak system rules */
3734   /* those are used later on to keep a version of the installed packages in
3735      best effort mode */
3736   if (installed && installed->nsolvables)
3737     {
3738       solv->weaksystemrules = sat_calloc(installed->end - installed->start, sizeof(Id));
3739       FOR_REPO_SOLVABLES(installed, p, s)
3740         {
3741           policy_findupdatepackages(solv, s, &q, 1);
3742           if (q.count)
3743             solv->weaksystemrules[p - installed->start] = pool_queuetowhatprovides(pool, &q);
3744         }
3745     }
3746
3747   /* free unneeded memory */
3748   map_free(&addedmap);
3749   queue_free(&q);
3750
3751   solv->weakrules = solv->nrules;
3752
3753   /* try real hard to keep packages installed */
3754   if (0)
3755     {
3756       FOR_REPO_SOLVABLES(installed, p, s)
3757         {
3758           /* FIXME: can't work with refine_suggestion! */
3759           /* need to always add the rule but disable it */
3760           if (MAPTST(&solv->noupdate, p - installed->start))
3761             continue;
3762           d = solv->weaksystemrules[p - installed->start];
3763           addrule(solv, p, d);
3764         }
3765     }
3766
3767   /* all new rules are learnt after this point */
3768   solv->learntrules = solv->nrules;
3769
3770   /* disable system rules that conflict with our job */
3771   disableupdaterules(solv, job, -1);
3772
3773   /* make decisions based on job/system assertions */
3774   makeruledecisions(solv);
3775
3776   /* create watches chains */
3777   makewatches(solv);
3778
3779   POOL_DEBUG(SAT_DEBUG_STATS, "problems so far: %d\n", solv->problems.count);
3780
3781   /* solve! */
3782   run_solver(solv, 1, 1);
3783
3784   /* find suggested packages */
3785   if (!solv->problems.count)
3786     {
3787       Id sug, *sugp, p, *pp;
3788
3789       /* create map of all suggests that are still open */
3790       solv->recommends_index = -1;
3791       MAPZERO(&solv->suggestsmap);
3792       for (i = 0; i < solv->decisionq.count; i++)
3793         {
3794           p = solv->decisionq.elements[i];
3795           if (p < 0)
3796             continue;
3797           s = pool->solvables + p;
3798           if (s->suggests)
3799             {
3800               sugp = s->repo->idarraydata + s->suggests;
3801               while ((sug = *sugp++) != 0)
3802                 {
3803                   FOR_PROVIDES(p, pp, sug)
3804                     if (solv->decisionmap[p] > 0)
3805                       break;
3806                   if (p)
3807                     continue;   /* already fulfilled */
3808                   FOR_PROVIDES(p, pp, sug)
3809                     MAPSET(&solv->suggestsmap, p);
3810                 }
3811             }
3812         }
3813       for (i = 1; i < pool->nsolvables; i++)
3814         {
3815           if (solv->decisionmap[i] != 0)
3816             continue;
3817           s = pool->solvables + i;
3818           if (!MAPTST(&solv->suggestsmap, i))
3819             {
3820               if (!s->enhances)
3821                 continue;
3822               if (!pool_installable(pool, s))
3823                 continue;
3824               if (!solver_is_enhancing(solv, s))
3825                 continue;
3826             }
3827           queue_push(&solv->suggestions, i);
3828         }
3829       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
3830     }
3831
3832   if (solv->problems.count)
3833     problems_to_solutions(solv, job);
3834 }