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