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 #include "sat_debug.h"
  26
  27 #define RULES_BLOCK 63
  28
  29
  30 int
  31 solver_dep_installed(Solver *solv, Id dep)
  32 {
  33   /* disable for now, splitprovides don't work anyway and it breaks
  34      a testcase */
  35 #if 0
  36   Pool *pool = solv->pool;
  37   Id p, *pp;
  38
  39   if (ISRELDEP(dep))
  40     {
  41       Reldep *rd = GETRELDEP(pool, dep);
  42       if (rd->flags == REL_AND)
  43         {
  44           if (!solver_dep_installed(solv, rd->name))
  45             return 0;
  46           return solver_dep_installed(solv, rd->evr);
  47         }
  48       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
  49         return solver_dep_installed(solv, rd->evr);
  50     }
  51   FOR_PROVIDES(p, pp, dep)
  52     {
  53       if (p == SYSTEMSOLVABLE || (solv->installed && pool->solvables[p].repo == solv->installed))
  54         return 1;
  55     }
  56 #endif
  57   return 0;
  58 }
  59
  60
  61 /* this mirrors solver_dep_fulfilled but uses map m instead of the decisionmap */
  62 static inline int
  63 dep_possible(Solver *solv, Id dep, Map *m)
  64 {
  65   Pool *pool = solv->pool;
  66   Id p, *pp;
  67
  68   if (ISRELDEP(dep))
  69     {
  70       Reldep *rd = GETRELDEP(pool, dep);
  71       if (rd->flags == REL_AND)
  72         {
  73           if (!dep_possible(solv, rd->name, m))
  74             return 0;
  75           return dep_possible(solv, rd->evr, m);
  76         }
  77       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
  78         return solver_dep_installed(solv, rd->evr);
  79     }
  80   FOR_PROVIDES(p, pp, dep)
  81     {
  82       if (MAPTST(m, p))
  83         return 1;
  84     }
  85   return 0;
  86 }
  87
  88 /*-----------------------------------------------------------------*/
  89
  90 /*
  91  * print rules
  92  */
  93
  94 static void
  95 printruleelement(Solver *solv, Rule *r, Id v)
  96 {
  97   Pool *pool = solv->pool;
  98   Solvable *s;
  99   if (v < 0)
 100     {
 101       s = pool->solvables + -v;
 102       sat_debug (ALWAYS, "    !%s [%d]", solvable2str(pool, s), -v);
 103     }
 104   else
 105     {
 106       s = pool->solvables + v;
 107       sat_debug (ALWAYS, "    %s [%d]", solvable2str(pool, s), v);
 108     }
 109   if (r)
 110     {
 111       if (r->w1 == v)
 112         sat_debug (ALWAYS, " (w1)");
 113       if (r->w2 == v)
 114         sat_debug (ALWAYS, " (w2)");
 115     }
 116   if (solv->decisionmap[s - pool->solvables] > 0)
 117     sat_debug (ALWAYS, " Install.level%d", solv->decisionmap[s - pool->solvables]);
 118   if (solv->decisionmap[s - pool->solvables] < 0)
 119     sat_debug (ALWAYS, " Conflict.level%d", -solv->decisionmap[s - pool->solvables]);
 120   sat_debug (ALWAYS, "\n");
 121 }
 122
 123
 124 /*
 125  * print rule
 126  */
 127
 128 static void
 129 printrule(Solver *solv, Rule *r)
 130 {
 131   int i;
 132   Id v;
 133
 134   if (r >= solv->rules && r < solv->rules + solv->nrules)   /* r is a solver rule */
 135     sat_debug (ALWAYS, "Rule #%d:", (int)(r - solv->rules));
 136   else
 137     sat_debug (ALWAYS, "Rule:");                       /* r is any rule */
 138   if (r && r->w1 == 0)
 139     sat_debug (ALWAYS, " (disabled)");
 140   sat_debug (ALWAYS, "\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, r, v);
 156     }
 157   sat_debug (ALWAYS, "    next: %d %d\n", r->n1, r->n2);
 158 }
 159
 160 static void
 161 printruleclass(Solver *solv, Rule *r)
 162 {
 163   if (r - solv->rules >= solv->learntrules)
 164     sat_debug (ALWAYS, "LEARNT ");
 165   else if (r - solv->rules >= solv->weakrules)
 166     sat_debug (ALWAYS, "WEAK ");
 167   else if (r - solv->rules >= solv->systemrules)
 168     sat_debug (ALWAYS, "SYSTEM ");
 169   else if (r - solv->rules >= solv->jobrules)
 170     sat_debug (ALWAYS, "JOB ");
 171   printrule(solv, r);
 172 }
 173
 174
 175 /*-----------------------------------------------------------------*/
 176
 177 /*
 178  * Rule handling
 179  */
 180
 181 static Pool *unifyrules_sortcmp_data;
 182
 183 /*
 184  * compare rules for unification sort
 185  */
 186
 187 static int
 188 unifyrules_sortcmp(const void *ap, const void *bp)
 189 {
 190   Pool *pool = unifyrules_sortcmp_data;
 191   Rule *a = (Rule *)ap;
 192   Rule *b = (Rule *)bp;
 193   Id *ad, *bd;
 194   int x;
 195
 196   x = a->p - b->p;
 197   if (x)
 198     return x;                          /* p differs */
 199
 200   /* identical p */
 201   if (a->d == 0 && b->d == 0)
 202     return a->w2 - b->w2;              /* assertion: return w2 diff */
 203
 204   if (a->d == 0)                       /* a is assertion, b not */
 205     {
 206       x = a->w2 - pool->whatprovidesdata[b->d];
 207       return x ? x : -1;
 208     }
 209
 210   if (b->d == 0)                       /* b is assertion, a not */
 211     {
 212       x = pool->whatprovidesdata[a->d] - b->w2;
 213       return x ? x : 1;
 214     }
 215
 216   /* compare whatprovidesdata */
 217   ad = pool->whatprovidesdata + a->d;
 218   bd = pool->whatprovidesdata + b->d;
 219   while (*bd)
 220     if ((x = *ad++ - *bd++) != 0)
 221       return x;
 222   return *ad;
 223 }
 224
 225
 226 /*
 227  * unify rules
 228  */
 229
 230 static void
 231 unifyrules(Solver *solv)
 232 {
 233   int i, j;
 234   Rule *ir, *jr;
 235
 236   if (solv->nrules <= 1)               /* nothing to unify */
 237     return;
 238
 239   sat_debug (DEBUG_4, "----- unifyrules -----\n");
 240
 241   /* sort rules first */
 242   unifyrules_sortcmp_data = solv->pool;
 243   qsort(solv->rules + 1, solv->nrules - 1, sizeof(Rule), unifyrules_sortcmp);
 244
 245   /* prune rules
 246    * i = unpruned
 247    * j = pruned
 248    */
 249   jr = 0;
 250   for (i = j = 1, ir = solv->rules + 1; i < solv->nrules; i++, ir++)
 251     {
 252       if (jr && !unifyrules_sortcmp(ir, jr))
 253         continue;                      /* prune! */
 254       jr = solv->rules + j++;          /* keep! */
 255       if (ir != jr)
 256         *jr = *ir;
 257     }
 258
 259   /* reduced count from nrules to j rules */
 260   sat_debug (DEBUG_1, "pruned rules from %d to %d\n", solv->nrules, j);
 261
 262   /* adapt rule buffer */
 263   solv->nrules = j;
 264   solv->rules = (Rule *)xrealloc(solv->rules, ((solv->nrules + RULES_BLOCK) & ~RULES_BLOCK) * sizeof(Rule));
 265 #if 1
 266   if (sat_debug_level() >= DEBUG_1)
 267     {
 268       int binr = 0;
 269       int lits = 0;
 270       Id *dp;
 271       Rule *r;
 272
 273       for (i = 1; i < solv->nrules; i++)
 274         {
 275           r = solv->rules + i;
 276           if (r->d == 0)
 277             binr++;
 278           else
 279             {
 280               dp = solv->pool->whatprovidesdata + r->d;
 281               while (*dp++)
 282                 lits++;
 283             }
 284         }
 285       sat_debug (DEBUG_1, "  binary: %d\n", binr);
 286       sat_debug (DEBUG_1,"  normal: %d, %d literals\n", solv->nrules - 1 - binr, lits);
 287     }
 288 #endif
 289   sat_debug (DEBUG_4, "----- 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   Rule *r = 0;
 353   Id *dp = 0;
 354
 355   int n = 0;                           /* number of literals in rule - 1
 356                                           0 = direct assertion (single literal)
 357                                           1 = binary rule
 358                                         */
 359
 360   /* it often happenes that requires lead to adding the same rpm rule
 361    * multiple times, so we prune those duplicates right away to make
 362    * the work for unifyrules a bit easier */
 363
 364   if (solv->nrules && !solv->jobrules)
 365     {
 366       r = solv->rules + solv->nrules - 1;   /* get the last added rule */
 367       if (r->p == p && r->d == d && d != 0)   /* identical and not user requested */
 368         return r;
 369     }
 370
 371   if (d < 0)
 372     {
 373       /* always a binary rule */
 374       if (p == d)
 375         return 0;                      /* ignore self conflict */
 376       n = 1;
 377     }
 378   else if (d > 0)
 379     {
 380       for (dp = solv->pool->whatprovidesdata + d; *dp; dp++, n++)
 381         if (*dp == -p)
 382           return 0;                     /* rule is self-fulfilling */
 383       if (n == 1)
 384         d = dp[-1];
 385     }
 386
 387   if (n == 0 && !solv->jobrules)
 388     {
 389       /* this is a rpm rule assertion, we do not have to allocate it */
 390       /* it can be identified by a level of 1 and a zero reason */
 391       /* we must not drop those rules from the decisionq when rewinding! */
 392       if (p >= 0)
 393         abort();
 394       if (solv->decisionmap[-p] > 0 || solv->decisionmap[-p] < -1)
 395         abort();
 396       if (solv->decisionmap[-p])
 397         return 0;       /* already got that one */
 398       queue_push(&solv->decisionq, p);
 399       queue_push(&solv->decisionq_why, 0);
 400       solv->decisionmap[-p] = -1;
 401       return 0;
 402     }
 403   if (n == 1 && p > d)
 404     {
 405       /* smallest literal first so we can find dups */
 406       n = p;
 407       p = d;
 408       d = n;
 409       n = 1;                           /* re-set n, was used as temp var */
 410     }
 411
 412   /* check if the last added rule is exactly the same as what we're looking for. */
 413   if (r && n == 1 && !r->d && r->p == p && r->w2 == d)
 414     return r;
 415
 416   if (r && n > 1 && r->d && r->p == p)
 417     {
 418       Id *dp2;
 419       if (d == r->d)
 420         return r;
 421       dp2 = solv->pool->whatprovidesdata + r->d;
 422       for (dp = solv->pool->whatprovidesdata + d; *dp; dp++, dp2++)
 423         if (*dp != *dp2)
 424           break;
 425       if (*dp == *dp2)
 426         return r;
 427    }
 428
 429   /*
 430    * allocate new rule
 431    */
 432
 433   /* check and extend rule buffer */
 434   if ((solv->nrules & RULES_BLOCK) == 0)
 435     {
 436       solv->rules = (Rule *)xrealloc(solv->rules, (solv->nrules + (RULES_BLOCK + 1)) * sizeof(Rule));
 437     }
 438
 439   r = solv->rules + solv->nrules++;    /* point to rule space */
 440
 441   r->p = p;
 442   if (n == 0)
 443     {
 444       /* direct assertion, no watch needed */
 445       r->d = 0;
 446       r->w1 = p;
 447       r->w2 = 0;
 448     }
 449   else if (n == 1)
 450     {
 451       /* binary rule */
 452       r->d = 0;
 453       r->w1 = p;
 454       r->w2 = d;
 455     }
 456   else
 457     {
 458       r->d = d;
 459       r->w1 = p;
 460       r->w2 = solv->pool->whatprovidesdata[d];
 461     }
 462   r->n1 = 0;
 463   r->n2 = 0;
 464
 465   if (sat_debug_level() >= DEBUG_3)
 466     {
 467       sat_debug (DEBUG_4, "  Add rule: ");
 468       printrule (solv, r);
 469     }
 470
 471   return r;
 472 }
 473
 474 static inline void
 475 disablerule(Solver *solv, Rule *r)
 476 {
 477   r->w1 = 0;
 478 }
 479
 480 static inline void
 481 enablerule(Solver *solv, Rule *r)
 482 {
 483   if (r->d == 0 || r->w2 != r->p)
 484     r->w1 = r->p;
 485   else
 486     r->w1 = solv->pool->whatprovidesdata[r->d];
 487 }
 488
 489
 490 /**********************************************************************************/
 491
 492 /* a problem is an item on the solver's problem list. It can either be >0, in that
 493  * case it is a system (upgrade) rule, or it can be <0, which makes it refer to a job
 494  * consisting of multiple job rules.
 495  */
 496
 497 static void
 498 disableproblem(Solver *solv, Id v)
 499 {
 500   Rule *r;
 501   int i;
 502   Id *jp;
 503
 504   if (v > 0)
 505     {
 506       disablerule(solv, solv->rules + v);
 507       return;
 508     }
 509   v = -(v + 1);
 510   jp = solv->ruletojob.elements;
 511   for (i = solv->jobrules, r = solv->rules + i; i < solv->systemrules; i++, r++, jp++)
 512     if (*jp == v)
 513       disablerule(solv, r);
 514 }
 515
 516 static void
 517 enableproblem(Solver *solv, Id v)
 518 {
 519   Rule *r;
 520   int i;
 521   Id *jp;
 522
 523   if (v > 0)
 524     {
 525       enablerule(solv, solv->rules + v);
 526       return;
 527     }
 528   v = -(v + 1);
 529   jp = solv->ruletojob.elements;
 530   for (i = solv->jobrules, r = solv->rules + i; i < solv->systemrules; i++, r++, jp++)
 531     if (*jp == v)
 532       enablerule(solv, r);
 533 }
 534
 535 static void
 536 printproblem(Solver *solv, Id v)
 537 {
 538   int i;
 539   Rule *r;
 540   Id *jp;
 541
 542   if (v > 0)
 543     printrule(solv, solv->rules + v);
 544   else
 545     {
 546       v = -(v + 1);
 547       sat_debug (ALWAYS, "JOB %d\n", v);
 548       jp = solv->ruletojob.elements;
 549       for (i = solv->jobrules, r = solv->rules + i; i < solv->systemrules; i++, r++, jp++)
 550         if (*jp == v)
 551           {
 552             sat_debug (ALWAYS, " -");
 553             printrule(solv, r);
 554           }
 555       sat_debug (ALWAYS, "ENDJOB\n");
 556     }
 557 }
 558
 559
 560
 561 /************************************************************************/
 562
 563 /* go through system and job rules and add direct assertions
 564  * to the decisionqueue. If we find a conflict, disable rules and
 565  * add them to problem queue.
 566  * (disablerules is always true for the cases when we get called)
 567  */
 568 static void
 569 makeruledecisions(Solver *solv)
 570 {
 571   int i, ri;
 572   Rule *r, *rr;
 573   Id v, vv;
 574   int decisionstart;
 575
 576   sat_debug (DEBUG_4, "----- makeruledecisions ; size decisionq: %d -----\n",solv->decisionq.count);
 577
 578   decisionstart = solv->decisionq.count;
 579   /* rpm rules don't have assertions, so we can start with the job
 580    * rules */
 581   for (ri = solv->jobrules, r = solv->rules + ri; ri < solv->nrules; ri++, r++)
 582     {
 583       if (!r->w1 || r->w2)      /* disabled or no assertion */
 584         continue;
 585       v = r->p;
 586       vv = v > 0 ? v : -v;
 587       if (solv->decisionmap[vv] == 0)
 588         {
 589           queue_push(&solv->decisionq, v);
 590           queue_push(&solv->decisionq_why, r - solv->rules);
 591           solv->decisionmap[vv] = v > 0 ? 1 : -1;
 592           if (sat_debug_level() >= DEBUG_4)
 593             {
 594               Solvable *s = solv->pool->solvables + vv;
 595               if (v < 0)
 596                 sat_debug (ALWAYS, "removing  %s\n", solvable2str(solv->pool, s));
 597               else
 598                 sat_debug (ALWAYS, "installing  %s\n", solvable2str(solv->pool, s));
 599             }
 600           continue;
 601         }
 602       if (v > 0 && solv->decisionmap[vv] > 0)
 603         continue;
 604       if (v < 0 && solv->decisionmap[vv] < 0)
 605         continue;
 606       /* found a conflict! */
 607       if (ri >= solv->learntrules)
 608         {
 609           /* cannot happen, as this would mean that the problem
 610            * was not solvable, so we wouldn't have created the
 611            * learnt rule at all */
 612           abort();
 613         }
 614       /* if we are weak, just disable ourself */
 615       if (ri >= solv->weakrules)
 616         {
 617           sat_debug (ALWAYS, "conflict, but I am weak, disabling ");
 618           printrule(solv, r);
 619           disablerule(solv, r);
 620           continue;
 621         }
 622
 623       /* only job and system rules left */
 624       for (i = 0; i < solv->decisionq.count; i++)
 625         if (solv->decisionq.elements[i] == -v)
 626           break;
 627       if (i == solv->decisionq.count)
 628         abort();
 629       if (solv->decisionq_why.elements[i] == 0)
 630         {
 631           /* conflict with rpm rule, need only disable our rule */
 632           if (v < 0 && v != -SYSTEMSOLVABLE)
 633             abort();
 634           /* record proof */
 635           queue_push(&solv->problems, solv->learnt_pool.count);
 636           queue_push(&solv->learnt_pool, ri);
 637           queue_push(&solv->learnt_pool, v != -SYSTEMSOLVABLE ? -v : v);
 638           queue_push(&solv->learnt_pool, 0);
 639           sat_debug (ALWAYS, "conflict with rpm rule, disabling rule #%d\n", ri);
 640           if (ri < solv->systemrules)
 641             v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
 642           else
 643             v = ri;
 644           queue_push(&solv->problems, v);
 645           disableproblem(solv, v);
 646           queue_push(&solv->problems, 0);
 647           continue;
 648         }
 649       /* record proof */
 650       queue_push(&solv->problems, solv->learnt_pool.count);
 651       queue_push(&solv->learnt_pool, ri);
 652       queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]);
 653       queue_push(&solv->learnt_pool, 0);
 654
 655       /* conflict with another job or system rule */
 656       sat_debug (ALWAYS, "conflicting system/job rules over literal %d\n", vv);
 657       /* push all of our rules asserting this literal on the problem stack */
 658       for (i = solv->jobrules, rr = solv->rules + i; i < solv->nrules; i++, rr++)
 659         {
 660           if (!rr->w1 || rr->w2)
 661             continue;
 662           if (rr->p != vv && rr->p != -vv)
 663             continue;
 664           sat_debug (ALWAYS, " - disabling rule #%d\n", i);
 665           v = i;
 666           if (i < solv->systemrules)
 667             v = -(solv->ruletojob.elements[i - solv->jobrules] + 1);
 668           queue_push(&solv->problems, v);
 669           disableproblem(solv, v);
 670         }
 671       queue_push(&solv->problems, 0);
 672
 673       /* start over */
 674       while (solv->decisionq.count > decisionstart)
 675         {
 676           v = solv->decisionq.elements[--solv->decisionq.count];
 677           --solv->decisionq_why.count;
 678           vv = v > 0 ? v : -v;
 679           solv->decisionmap[vv] = 0;
 680         }
 681       ri = solv->jobrules - 1;
 682       r = solv->rules + ri;
 683     }
 684
 685     sat_debug (DEBUG_4, "----- makeruledecisions end; size decisionq: %d -----\n",solv->decisionq.count);
 686 }
 687
 688 /*
 689  * we have enabled or disabled some of our rules. We now reenable all
 690  * of our learnt rules but the ones that were learnt from rules that
 691  * are now disabled.
 692  */
 693 static void
 694 enabledisablelearntrules(Solver *solv)
 695 {
 696   Rule *r;
 697   Id why, *whyp;
 698   int i;
 699
 700   sat_debug (DEBUG_1, "enabledisablelearntrules called\n");
 701   for (i = solv->learntrules, r = solv->rules + i; i < solv->nrules; i++, r++)
 702     {
 703       whyp = solv->learnt_pool.elements + solv->learnt_why.elements[i - solv->learntrules];
 704       while ((why = *whyp++) != 0)
 705         {
 706           if (why < 0 || why >= i)
 707             abort();            /* cannot reference newer learnt rules */
 708           if (!solv->rules[why].w1)
 709             break;
 710         }
 711       /* why != 0: we found a disabled rule, disable the learnt rule */
 712       if (why && r->w1)
 713         {
 714           if (sat_debug_level() >= DEBUG_1)
 715             {
 716               sat_debug (DEBUG_1, "disabling learnt ");
 717               printrule(solv, r);
 718             }
 719           disablerule(solv, r);
 720         }
 721       else if (!why && !r->w1)
 722         {
 723           if (sat_debug_level() >= DEBUG_1)
 724             {
 725               sat_debug (DEBUG_1, "re-enabling learnt ");
 726               printrule(solv, r);
 727             }
 728           enablerule(solv, r);
 729         }
 730     }
 731 }
 732
 733
 734 /* FIXME: bad code ahead, replace as soon as possible */
 735 static void
 736 disableupdaterules(Solver *solv, Queue *job, int jobidx)
 737 {
 738   Pool *pool = solv->pool;
 739   int i, j;
 740   Id how, what, p, *pp;
 741   Solvable *s;
 742   Repo *installed;
 743   Rule *r;
 744   Id lastjob = -1;
 745
 746   installed = solv->installed;
 747   if (!installed)
 748     return;
 749
 750   if (jobidx != -1)
 751     {
 752       how = job->elements[jobidx];
 753       switch(how)
 754         {
 755         case SOLVER_INSTALL_SOLVABLE:
 756         case SOLVER_ERASE_SOLVABLE:
 757         case SOLVER_ERASE_SOLVABLE_NAME:
 758         case SOLVER_ERASE_SOLVABLE_PROVIDES:
 759           break;
 760         default:
 761           return;
 762         }
 763     }
 764   /* go through all enabled job rules */
 765   MAPZERO(&solv->noupdate);
 766   for (i = solv->jobrules; i < solv->systemrules; i++)
 767     {
 768       r = solv->rules + i;
 769       if (!r->w1)       /* disabled? */
 770         continue;
 771       j = solv->ruletojob.elements[i - solv->jobrules];
 772       if (j == lastjob)
 773         continue;
 774       lastjob = j;
 775       how = job->elements[j];
 776       what = job->elements[j + 1];
 777       switch(how)
 778         {
 779         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
 780           s = pool->solvables + what;
 781           FOR_PROVIDES(p, pp, s->name)
 782             {
 783               if (pool->solvables[p].name != s->name)
 784                 continue;
 785               if (pool->solvables[p].repo == installed)
 786                 MAPSET(&solv->noupdate, p - installed->start);
 787             }
 788           break;
 789         case SOLVER_ERASE_SOLVABLE:
 790           s = pool->solvables + what;
 791           if (s->repo == installed)
 792             MAPSET(&solv->noupdate, what - installed->start);
 793           break;
 794         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
 795         case SOLVER_ERASE_SOLVABLE_PROVIDES:
 796           FOR_PROVIDES(p, pp, what)
 797             {
 798               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
 799                 continue;
 800               if (pool->solvables[p].repo == installed)
 801                 MAPSET(&solv->noupdate, p - installed->start);
 802             }
 803           break;
 804         default:
 805           break;
 806         }
 807     }
 808
 809   /* fixup update rule status */
 810   if (solv->allowuninstall)
 811     return;             /* no update rules at all */
 812
 813   if (jobidx != -1)
 814     {
 815       /* we just disabled job #jobidx. enable all update rules
 816        * that aren't disabled by the remaining job rules */
 817       how = job->elements[jobidx];
 818       what = job->elements[jobidx + 1];
 819       switch(how)
 820         {
 821         case SOLVER_INSTALL_SOLVABLE:
 822           s = pool->solvables + what;
 823           FOR_PROVIDES(p, pp, s->name)
 824             {
 825               if (pool->solvables[p].name != s->name)
 826                 continue;
 827               if (pool->solvables[p].repo != installed)
 828                 continue;
 829               if (MAPTST(&solv->noupdate, p - installed->start))
 830                 continue;
 831               r = solv->rules + solv->systemrules + (p - installed->start);
 832               if (r->w1)
 833                 continue;
 834               enablerule(solv, r);
 835               if (sat_debug_level() >= DEBUG_1)
 836                 {
 837                   sat_debug (DEBUG_1, "@@@ re-enabling ");
 838                   printrule(solv, r);
 839                 }
 840             }
 841           break;
 842         case SOLVER_ERASE_SOLVABLE:
 843           s = pool->solvables + what;
 844           if (s->repo != installed)
 845             break;
 846           if (MAPTST(&solv->noupdate, what - installed->start))
 847             break;
 848           r = solv->rules + solv->systemrules + (what - installed->start);
 849           if (r->w1)
 850             break;
 851           enablerule(solv, r);
 852           if (sat_debug_level() >= DEBUG_1)
 853             {
 854               sat_debug (DEBUG_1, "@@@ re-enabling ");
 855               printrule(solv, r);
 856             }
 857           break;
 858         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
 859         case SOLVER_ERASE_SOLVABLE_PROVIDES:
 860           FOR_PROVIDES(p, pp, what)
 861             {
 862               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
 863                 continue;
 864               if (pool->solvables[p].repo != installed)
 865                 continue;
 866               if (MAPTST(&solv->noupdate, p - installed->start))
 867                 continue;
 868               r = solv->rules + solv->systemrules + (p - installed->start);
 869               if (r->w1)
 870                 continue;
 871               enablerule(solv, r);
 872               if (sat_debug_level() >= DEBUG_1)
 873                 {
 874                   sat_debug (DEBUG_1, "@@@ re-enabling ");
 875                   printrule(solv, r);
 876                 }
 877             }
 878           break;
 879         default:
 880           break;
 881         }
 882       return;
 883     }
 884
 885   for (i = 0; i < installed->nsolvables; i++)
 886     {
 887       r = solv->rules + solv->systemrules + i;
 888       if (r->w1 && MAPTST(&solv->noupdate, i))
 889         disablerule(solv, r);   /* was enabled, need to disable */
 890     }
 891 }
 892
 893
 894 /*
 895  * add (install) rules for solvable
 896  * for unfulfilled requirements, conflicts, obsoletes,....
 897  * add a negative assertion for solvables that are not installable
 898  */
 899
 900 static void
 901 addrpmrulesforsolvable(Solver *solv, Solvable *s, Map *m)
 902 {
 903   Pool *pool = solv->pool;
 904   Repo *installed = solv->installed;
 905   Queue q;
 906   Id qbuf[64];
 907   int i;
 908   int dontfix;
 909   Id req, *reqp;
 910   Id con, *conp;
 911   Id obs, *obsp;
 912   Id rec, *recp;
 913   Id sug, *sugp;
 914   Id p, *pp;
 915   Id *dp;
 916   Id n;
 917
 918   sat_debug (DEBUG_4, "----- addrpmrulesforsolvable -----\n");
 919
 920   queue_init_buffer(&q, qbuf, sizeof(qbuf)/sizeof(*qbuf));
 921   queue_push(&q, s - pool->solvables);  /* push solvable Id */
 922
 923   while (q.count)
 924     {
 925       /*
 926        * n: Id of solvable
 927        * s: Pointer to solvable
 928        */
 929
 930       n = queue_shift(&q);
 931       if (MAPTST(m, n))                /* continue if already done */
 932         continue;
 933
 934       MAPSET(m, n);
 935       s = pool->solvables + n;         /* s = Solvable in question */
 936
 937       dontfix = 0;
 938       if (installed                     /* Installed system available */
 939           && !solv->fixsystem           /* NOT repair errors in rpm dependency graph */
 940           && s->repo == installed)      /* solvable is installed? */
 941       {
 942         dontfix = 1;                   /* dont care about broken rpm deps */
 943       }
 944
 945       if (!dontfix && s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
 946         {
 947           sat_debug (DEBUG_1, "package %s [%d] is not installable\n", solvable2str(pool, s), (Id)(s - pool->solvables));
 948           addrule(solv, -n, 0);         /* uninstallable */
 949         }
 950
 951       /*-----------------------------------------
 952        * check requires of s
 953        */
 954
 955       if (s->requires)
 956         {
 957           reqp = s->repo->idarraydata + s->requires;
 958           while ((req = *reqp++) != 0) /* go throw all requires */
 959             {
 960               if (req == SOLVABLE_PREREQMARKER)   /* skip the marker */
 961                 continue;
 962
 963               dp = pool_whatprovides(pool, req);
 964
 965               if (*dp == SYSTEMSOLVABLE)        /* always installed */
 966                 continue;
 967
 968               if (dontfix)
 969                 {
 970                   /* the strategy here is to not insist on dependencies
 971                    * that are already broken. so if we find one provider
 972                    * that was already installed, we know that the
 973                    * dependency was not broken before so we enforce it */
 974                   for (i = 0; (p = dp[i]) != 0; i++)    /* for all providers */
 975                     {
 976                       if (pool->solvables[p].repo == installed)
 977                         break;          /* provider was installed */
 978                     }
 979                   if (!p)               /* previously broken dependency */
 980                     {
 981                       sat_debug (DEBUG_1, "ignoring broken requires %s of installed package %s\n", dep2str(pool, req), solvable2str(pool, s));
 982                       continue;
 983                     }
 984                 }
 985
 986               if (!*dp)
 987                 {
 988                   /* nothing provides req! */
 989                   sat_debug (DEBUG_1, "package %s [%d] is not installable (%s)\n", solvable2str(pool, s), (Id)(s - pool->solvables), dep2str(pool, req));
 990                   addrule(solv, -n, 0); /* mark requestor as uninstallable */
 991                   continue;
 992                 }
 993
 994               if (sat_debug_level() >= DEBUG_2)
 995                 {
 996                   sat_debug (DEBUG_2,"  %s requires %s\n", solvable2str(pool, s), dep2str(pool, req));
 997                   for (i = 0; dp[i]; i++)
 998                     sat_debug (DEBUG_2, "   provided by %s\n", solvable2str(pool, pool->solvables + dp[i]));
 999                 }
1000
1001               /* add 'requires' dependency */
1002               /* rule: (-requestor|provider1|provider2|...|providerN) */
1003               addrule(solv, -n, dp - pool->whatprovidesdata);
1004
1005               /* descend the dependency tree */
1006               for (; *dp; dp++)   /* loop through all providers */
1007                 {
1008                   if (!MAPTST(m, *dp))
1009                     queue_push(&q, *dp);
1010                 }
1011
1012             } /* while, requirements of n */
1013
1014         } /* if, requirements */
1015
1016       /* that's all we check for src packages */
1017       if (s->arch == ARCH_SRC || s->arch == ARCH_NOSRC)
1018         continue;
1019
1020       /*-----------------------------------------
1021        * check conflicts of s
1022        */
1023
1024       if (s->conflicts)
1025         {
1026           conp = s->repo->idarraydata + s->conflicts;
1027           while ((con = *conp++) != 0)
1028             {
1029               FOR_PROVIDES(p, pp, con)
1030                 {
1031                    /* dontfix: dont care about conflicts with already installed packs */
1032                   if (dontfix && pool->solvables[p].repo == installed)
1033                     continue;
1034                  /* rule: -n|-p: either solvable _or_ provider of conflict */
1035                   addrule(solv, -n, -p);
1036                 }
1037             }
1038         }
1039
1040       /*-----------------------------------------
1041        * check obsoletes if not installed
1042        */
1043       if (!installed || pool->solvables[n].repo != installed)
1044         {                              /* not installed */
1045           if (s->obsoletes)
1046             {
1047               obsp = s->repo->idarraydata + s->obsoletes;
1048               while ((obs = *obsp++) != 0)
1049                 {
1050                   FOR_PROVIDES(p, pp, obs)
1051                     addrule(solv, -n, -p);
1052                 }
1053             }
1054           FOR_PROVIDES(p, pp, s->name)
1055             {
1056               if (s->name == pool->solvables[p].name)
1057                 addrule(solv, -n, -p);
1058             }
1059         }
1060
1061       /*-----------------------------------------
1062        * add recommends to the rule list
1063        */
1064       if (s->recommends)
1065         {
1066           recp = s->repo->idarraydata + s->recommends;
1067           while ((rec = *recp++) != 0)
1068             {
1069               FOR_PROVIDES(p, pp, rec)
1070                 if (!MAPTST(m, p))
1071                   queue_push(&q, p);
1072             }
1073         }
1074       if (s->suggests)
1075         {
1076           sugp = s->repo->idarraydata + s->suggests;
1077           while ((sug = *sugp++) != 0)
1078             {
1079               FOR_PROVIDES(p, pp, sug)
1080                 if (!MAPTST(m, p))
1081                   queue_push(&q, p);
1082             }
1083         }
1084     }
1085   queue_free(&q);
1086   sat_debug (DEBUG_4, "----- addrpmrulesforsolvable end -----\n");
1087
1088 }
1089
1090 static void
1091 addrpmrulesforweak(Solver *solv, Map *m)
1092 {
1093   Pool *pool = solv->pool;
1094   Solvable *s;
1095   Id sup, *supp;
1096   int i, n;
1097
1098   sat_debug (DEBUG_4, "----- addrpmrulesforweak -----\n");
1099   for (i = n = 1; n < pool->nsolvables; i++, n++)
1100     {
1101       if (i == pool->nsolvables)
1102         i = 1;
1103       if (MAPTST(m, i))
1104         continue;
1105       s = pool->solvables + i;
1106       if (!pool_installable(pool, s))
1107         continue;
1108       sup = 0;
1109       if (s->supplements)
1110         {
1111           supp = s->repo->idarraydata + s->supplements;
1112           while ((sup = *supp++) != ID_NULL)
1113             if (dep_possible(solv, sup, m))
1114               break;
1115         }
1116       if (!sup && s->freshens)
1117         {
1118           supp = s->repo->idarraydata + s->freshens;
1119           while ((sup = *supp++) != ID_NULL)
1120             if (dep_possible(solv, sup, m))
1121               break;
1122         }
1123       if (!sup && s->enhances)
1124         {
1125           supp = s->repo->idarraydata + s->enhances;
1126           while ((sup = *supp++) != ID_NULL)
1127             if (dep_possible(solv, sup, m))
1128               break;
1129         }
1130       if (!sup)
1131         continue;
1132       addrpmrulesforsolvable(solv, s, m);
1133       n = 0;
1134     }
1135   sat_debug (DEBUG_4, "----- addrpmrulesforweak end -----\n");
1136 }
1137
1138 static void
1139 addrpmrulesforupdaters(Solver *solv, Solvable *s, Map *m, int allowall)
1140 {
1141   Pool *pool = solv->pool;
1142   int i;
1143   Queue qs;
1144   Id qsbuf[64];
1145
1146   sat_debug (DEBUG_4, "----- addrpmrulesforupdaters -----\n");
1147
1148   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1149   policy_findupdatepackages(solv, s, &qs, allowall);
1150   if (!MAPTST(m, s - pool->solvables))  /* add rule for s if not already done */
1151     addrpmrulesforsolvable(solv, s, m);
1152   for (i = 0; i < qs.count; i++)
1153     if (!MAPTST(m, qs.elements[i]))
1154       addrpmrulesforsolvable(solv, pool->solvables + qs.elements[i], m);
1155   queue_free(&qs);
1156
1157   sat_debug (DEBUG_1, "----- addrpmrulesforupdaters -----\n");
1158
1159 }
1160
1161 /*
1162  * add rule for update
1163  *   (A|A1|A2|A3...)  An = update candidates for A
1164  *
1165  * s = (installed) solvable
1166  */
1167
1168 static void
1169 addupdaterule(Solver *solv, Solvable *s, int allowall)
1170 {
1171   /* installed packages get a special upgrade allowed rule */
1172   Pool *pool = solv->pool;
1173   Id d;
1174   Queue qs;
1175   Id qsbuf[64];
1176
1177   sat_debug (DEBUG_4, "-----  addupdaterule -----\n");
1178
1179   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1180   policy_findupdatepackages(solv, s, &qs, allowall);
1181   if (qs.count == 0)                   /* no updaters found */
1182     d = 0;
1183   else
1184     d = pool_queuetowhatprovides(pool, &qs);    /* intern computed queue */
1185   queue_free(&qs);
1186   addrule(solv, s - pool->solvables, d);        /* allow update of s */
1187   sat_debug (DEBUG_4, "-----  addupdaterule end -----\n");
1188 }
1189
1190
1191 /*-----------------------------------------------------------------*/
1192 /* watches */
1193
1194
1195 /*
1196  * makewatches
1197  *
1198  * initial setup for all watches
1199  */
1200
1201 static void
1202 makewatches(Solver *solv)
1203 {
1204   Rule *r;
1205   int i;
1206   int nsolvables = solv->pool->nsolvables;
1207
1208   xfree(solv->watches);
1209                                        /* lower half for removals, upper half for installs */
1210   solv->watches = (Id *)xcalloc(2 * nsolvables, sizeof(Id));
1211 #if 1
1212   /* do it reverse so rpm rules get triggered first */
1213   for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
1214 #else
1215   for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
1216 #endif
1217     {
1218       if (!r->w1                       /* rule is disabled */
1219           || !r->w2)                   /* rule is assertion */
1220         continue;
1221
1222       /* see addwatches(solv, r) */
1223       r->n1 = solv->watches[nsolvables + r->w1];
1224       solv->watches[nsolvables + r->w1] = r - solv->rules;
1225
1226       r->n2 = solv->watches[nsolvables + r->w2];
1227       solv->watches[nsolvables + r->w2] = r - solv->rules;
1228     }
1229 }
1230
1231
1232 /*
1233  * add watches (for rule)
1234  */
1235
1236 static void
1237 addwatches(Solver *solv, Rule *r)
1238 {
1239   int nsolvables = solv->pool->nsolvables;
1240
1241   r->n1 = solv->watches[nsolvables + r->w1];
1242   solv->watches[nsolvables + r->w1] = r - solv->rules;
1243
1244   r->n2 = solv->watches[nsolvables + r->w2];
1245   solv->watches[nsolvables + r->w2] = r - solv->rules;
1246 }
1247
1248
1249 /*-----------------------------------------------------------------*/
1250 /* rule propagation */
1251
1252 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
1253
1254 /*
1255  * propagate
1256  *
1257  * propagate decision to all rules
1258  */
1259
1260 static Rule *
1261 propagate(Solver *solv, int level)
1262 {
1263   Pool *pool = solv->pool;
1264   Id *rp, *nrp;
1265   Rule *r;
1266   Id p, pkg, ow;
1267   Id *dp;
1268   Id *decisionmap = solv->decisionmap;
1269   Id *watches = solv->watches + pool->nsolvables;
1270
1271   sat_debug (DEBUG_4, "----- propagate -----\n");
1272
1273   while (solv->propagate_index < solv->decisionq.count)
1274     {
1275       /* negate because our watches trigger if literal goes FALSE */
1276       pkg = -solv->decisionq.elements[solv->propagate_index++];
1277       if (sat_debug_level() >= DEBUG_4)
1278         {
1279           sat_debug (DEBUG_4, "popagate for decision %d level %d\n", -pkg, level);
1280           printruleelement(solv, 0, -pkg);
1281         }
1282
1283       for (rp = watches + pkg; *rp; rp = nrp)
1284         {
1285           r = solv->rules + *rp;
1286
1287           if (sat_debug_level() >= DEBUG_4)
1288             {
1289               sat_debug (DEBUG_4,"  watch triggered ");
1290               printrule(solv, r);
1291             }
1292
1293           if (pkg == r->w1)
1294             {
1295               ow = r->w2;
1296               nrp = &r->n1;
1297             }
1298           else
1299             {
1300               ow = r->w1;
1301               nrp = &r->n2;
1302             }
1303           /* if clause is TRUE, nothing to do */
1304           if (DECISIONMAP_TRUE(ow))
1305             continue;
1306
1307           if (r->d)
1308             {
1309               /* not a binary clause, check if we need to move our watch */
1310               /* search for a literal that is not ow and not false */
1311               /* (true is also ok, in that case the rule is fulfilled) */
1312               if (r->p && r->p != ow && !DECISIONMAP_TRUE(-r->p))
1313                 p = r->p;
1314               else
1315                 for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
1316                   if (p != ow && !DECISIONMAP_TRUE(-p))
1317                     break;
1318               if (p)
1319                 {
1320                   /* p is free to watch, move watch to p */
1321                   if (sat_debug_level() >= DEBUG_4)
1322                     {
1323                       if (p > 0)
1324                         sat_debug (DEBUG_4, "    -> move w%d to %s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables + p));
1325                       else
1326                         sat_debug (DEBUG_4,"    -> move w%d to !%s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables - p));
1327                     }
1328                   *rp = *nrp;
1329                   nrp = rp;
1330                   if (pkg == r->w1)
1331                     {
1332                       r->w1 = p;
1333                       r->n1 = watches[p];
1334                     }
1335                   else
1336                     {
1337                       r->w2 = p;
1338                       r->n2 = watches[p];
1339                     }
1340                   watches[p] = r - solv->rules;
1341                   continue;
1342                 }
1343             }
1344           /* unit clause found, set other watch to TRUE */
1345           if (DECISIONMAP_TRUE(-ow))
1346             return r;           /* eek, a conflict! */
1347           if (sat_debug_level() >= DEBUG_2)
1348             {
1349               sat_debug (DEBUG_2, "unit ");
1350               printrule(solv, r);
1351             }
1352           if (ow > 0)
1353             decisionmap[ow] = level;
1354           else
1355             decisionmap[-ow] = -level;
1356           queue_push(&solv->decisionq, ow);
1357           queue_push(&solv->decisionq_why, r - solv->rules);
1358           if (sat_debug_level() >= DEBUG_4)
1359             {
1360               Solvable *s = pool->solvables + (ow > 0 ? ow : -ow);
1361               if (ow > 0)
1362                 sat_debug (DEBUG_4, "  -> decided to install %s\n", solvable2str(pool, s));
1363               else
1364                 sat_debug (DEBUG_4, "  -> decided to conflict %s\n", solvable2str(pool, s));
1365             }
1366         }
1367     }
1368   sat_debug (DEBUG_4, "----- propagate end-----\n");
1369
1370   return 0;     /* all is well */
1371 }
1372
1373
1374 /*-----------------------------------------------------------------*/
1375 /* Analysis */
1376
1377 /*
1378  * analyze
1379  *   and learn
1380  */
1381
1382 static int
1383 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *why)
1384 {
1385   Pool *pool = solv->pool;
1386   Queue r;
1387   int rlevel = 1;
1388   Map seen;             /* global? */
1389   Id v, vv, *dp;
1390   int l, i, idx;
1391   int num = 0;
1392   int learnt_why = solv->learnt_pool.count;
1393   Id *decisionmap = solv->decisionmap;
1394
1395   queue_init(&r);
1396
1397   sat_debug (DEBUG_1, "ANALYZE at %d ----------------------\n", level);
1398   map_init(&seen, pool->nsolvables);
1399   idx = solv->decisionq.count;
1400   for (;;)
1401     {
1402       if (sat_debug_level() >= DEBUG_2)
1403         printruleclass(solv, c);
1404       queue_push(&solv->learnt_pool, c - solv->rules);
1405       dp = c->d ? pool->whatprovidesdata + c->d : 0;
1406       for (i = -1; ; i++)
1407         {
1408           if (i == -1)
1409             v = c->p;
1410           else if (c->d == 0)
1411             v = i ? 0 : c->w2;
1412           else
1413             v = *dp++;
1414           if (v == 0)
1415             break;
1416           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1417               continue;
1418           vv = v > 0 ? v : -v;
1419           if (MAPTST(&seen, vv))
1420             continue;
1421           l = solv->decisionmap[vv];
1422           if (l < 0)
1423             l = -l;
1424           if (l == 1)
1425             {
1426 #if 0
1427               int j;
1428               for (j = 0; j < solv->decisionq.count; j++)
1429                 if (solv->decisionq.elements[j] == v)
1430                   break;
1431               if (j == solv->decisionq.count)
1432                 abort();
1433               queue_push(&rulq, -(j + 1));
1434 #endif
1435               continue;                 /* initial setting */
1436             }
1437           MAPSET(&seen, vv);
1438           if (l == level)
1439             num++;                      /* need to do this one as well */
1440           else
1441             {
1442               queue_push(&r, v);
1443               if (sat_debug_level() >= DEBUG_4)
1444                 {
1445                   sat_debug (DEBUG_4, "PUSH %d ", v);
1446                   printruleelement(solv, 0, v);
1447                 }
1448               if (l > rlevel)
1449                 rlevel = l;
1450             }
1451         }
1452       sat_debug (DEBUG_4, "num = %d\n", num);
1453       if (num <= 0)
1454         abort();
1455       for (;;)
1456         {
1457           v = solv->decisionq.elements[--idx];
1458           vv = v > 0 ? v : -v;
1459           if (MAPTST(&seen, vv))
1460             break;
1461         }
1462       c = solv->rules + solv->decisionq_why.elements[idx];
1463       MAPCLR(&seen, vv);
1464       if (--num == 0)
1465         break;
1466     }
1467   *pr = -v;
1468   if (r.count == 0)
1469     *dr = 0;
1470   else if (r.count == 1 && r.elements[0] < 0)
1471     *dr = r.elements[0];
1472   else
1473     *dr = pool_queuetowhatprovides(pool, &r);
1474   if (sat_debug_level() >= DEBUG_1)
1475     {
1476       sat_debug (DEBUG_1, "learned rule for level %d (am %d)\n", rlevel, level);
1477       printruleelement(solv, 0, -v);
1478       for (i = 0; i < r.count; i++)
1479         {
1480           v = r.elements[i];
1481           printruleelement(solv, 0, v);
1482         }
1483     }
1484   map_free(&seen);
1485   queue_push(&solv->learnt_pool, 0);
1486   if (sat_debug_level() >= DEBUG_4)
1487     {
1488       for (i = learnt_why; solv->learnt_pool.elements[i]; i++)
1489         {
1490           sat_debug (DEBUG_4, "learnt_why ");
1491           printrule(solv, solv->rules + solv->learnt_pool.elements[i]);
1492         }
1493     }
1494   if (why)
1495     *why = learnt_why;
1496   return rlevel;
1497 }
1498
1499
1500 /*
1501  * reset_solver
1502  * reset the solver decisions to right after the rpm rules.
1503  * called after rules have been enabled/disabled
1504  */
1505
1506 static void
1507 reset_solver(Solver *solv)
1508 {
1509   int i;
1510   Id v;
1511
1512   enabledisablelearntrules(solv);
1513
1514   /* redo all direct rpm rule decisions */
1515   /* we break at the first decision with a why attached, this is
1516    * either a job/system rule assertion or a propagated decision */
1517   for (i = 0; i < solv->decisionq.count; i++)
1518     {
1519       v = solv->decisionq.elements[i];
1520       solv->decisionmap[v > 0 ? v : -v] = 0;
1521     }
1522   for (i = 0; i < solv->decisionq_why.count; i++)
1523     if (solv->decisionq_why.elements[i])
1524       break;
1525     else
1526       {
1527         v = solv->decisionq.elements[i];
1528         solv->decisionmap[v > 0 ? v : -v] = v > 0 ? 1 : -1;
1529       }
1530
1531   sat_debug (DEBUG_2, "decisions done reduced from %d to %d\n", solv->decisionq.count, i);
1532
1533   solv->decisionq_why.count = i;
1534   solv->decisionq.count = i;
1535   solv->recommends_index = -1;
1536   solv->propagate_index = 0;
1537
1538   /* redo all job/system decisions */
1539   makeruledecisions(solv);
1540   sat_debug (DEBUG_2, "decisions so far: %d\n", solv->decisionq.count);
1541   /* recreate watch chains */
1542   makewatches(solv);
1543 }
1544
1545
1546 /*
1547  * analyze_unsolvable_rule
1548  */
1549
1550 static void
1551 analyze_unsolvable_rule(Solver *solv, Rule *r)
1552 {
1553   int i;
1554   Id why = r - solv->rules;
1555   if (sat_debug_level() >= DEBUG_2)
1556      printruleclass(solv, r);
1557   if (solv->learntrules && why >= solv->learntrules)
1558     {
1559       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1560         analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i]);
1561       return;
1562     }
1563   /* do not add rpm rules to problem */
1564   if (why < solv->jobrules)
1565     return;
1566   /* turn rule into problem */
1567   if (why >= solv->jobrules && why < solv->systemrules)
1568     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
1569   /* return if problem already countains our rule */
1570   if (solv->problems.count)
1571     {
1572       for (i = solv->problems.count - 1; i >= 0; i--)
1573         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
1574           break;
1575         else if (solv->problems.elements[i] == why)
1576           return;
1577     }
1578   queue_push(&solv->problems, why);
1579 }
1580
1581
1582 /*
1583  * analyze_unsolvable
1584  *
1585  * return: 1 - disabled some rules, try again
1586  *         0 - hopeless
1587  */
1588
1589 static int
1590 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
1591 {
1592   Pool *pool = solv->pool;
1593   Rule *r;
1594   Map seen;             /* global to speed things up? */
1595   Id v, vv, *dp, why;
1596   int l, i, idx;
1597   Id *decisionmap = solv->decisionmap;
1598   int oldproblemcount;
1599   int oldlearntpoolcount;
1600   int lastweak;
1601
1602   sat_debug (DEBUG_2, "ANALYZE UNSOLVABLE ----------------------\n");
1603   oldproblemcount = solv->problems.count;
1604   oldlearntpoolcount = solv->learnt_pool.count;
1605
1606   /* make room for proof index */
1607   /* must update it later, as analyze_unsolvable_rule would confuse
1608    * it with a rule index if we put the real value in already */
1609   queue_push(&solv->problems, 0);
1610
1611   r = cr;
1612   map_init(&seen, pool->nsolvables);
1613   queue_push(&solv->learnt_pool, r - solv->rules);
1614   analyze_unsolvable_rule(solv, r);
1615   dp = r->d ? pool->whatprovidesdata + r->d : 0;
1616   for (i = -1; ; i++)
1617     {
1618       if (i == -1)
1619         v = r->p;
1620       else if (r->d == 0)
1621         v = i ? 0 : r->w2;
1622       else
1623         v = *dp++;
1624       if (v == 0)
1625         break;
1626       if (DECISIONMAP_TRUE(v))  /* the one true literal */
1627           continue;
1628       vv = v > 0 ? v : -v;
1629       l = solv->decisionmap[vv];
1630       if (l < 0)
1631         l = -l;
1632       MAPSET(&seen, vv);
1633     }
1634   idx = solv->decisionq.count;
1635   while (idx > 0)
1636     {
1637       v = solv->decisionq.elements[--idx];
1638       vv = v > 0 ? v : -v;
1639       if (!MAPTST(&seen, vv))
1640         continue;
1641       why = solv->decisionq_why.elements[idx];
1642       if (!why)
1643         {
1644           /* level 1 and no why, must be an rpm assertion */
1645           if (sat_debug_level() >= DEBUG_4)
1646             {
1647               sat_debug (DEBUG_4, "RPM ");
1648               printruleelement(solv, 0, v);
1649             }
1650           /* this is the only positive rpm assertion */
1651           if (v == SYSTEMSOLVABLE)
1652             v = -v;
1653           if (v >= 0)
1654             abort();
1655           queue_push(&solv->learnt_pool, v);
1656           continue;
1657         }
1658       r = solv->rules + why;
1659       queue_push(&solv->learnt_pool, why);
1660       analyze_unsolvable_rule(solv, r);
1661       dp = r->d ? pool->whatprovidesdata + r->d : 0;
1662       for (i = -1; ; i++)
1663         {
1664           if (i == -1)
1665             v = r->p;
1666           else if (r->d == 0)
1667             v = i ? 0 : r->w2;
1668           else
1669             v = *dp++;
1670           if (v == 0)
1671             break;
1672           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1673               continue;
1674           vv = v > 0 ? v : -v;
1675           l = solv->decisionmap[vv];
1676           if (l < 0)
1677             l = -l;
1678           MAPSET(&seen, vv);
1679         }
1680     }
1681   map_free(&seen);
1682   queue_push(&solv->problems, 0);       /* mark end of this problem */
1683
1684   lastweak = 0;
1685   if (solv->weakrules != solv->learntrules)
1686     {
1687       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
1688         {
1689           why = solv->problems.elements[i];
1690           if (why < solv->weakrules || why >= solv->learntrules)
1691             continue;
1692           if (!lastweak || lastweak < why)
1693             lastweak = why;
1694         }
1695     }
1696   if (lastweak)
1697     {
1698       /* disable last weak rule */
1699       solv->problems.count = oldproblemcount;
1700       solv->learnt_pool.count = oldlearntpoolcount;
1701       r = solv->rules + lastweak;
1702       sat_debug (ALWAYS, "disabling weak ");
1703       printrule(solv, r);
1704       disablerule(solv, r);
1705       reset_solver(solv);
1706       return 1;
1707     }
1708
1709   /* finish proof */
1710   queue_push(&solv->learnt_pool, 0);
1711   solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
1712
1713   if (disablerules)
1714     {
1715       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
1716         disableproblem(solv, solv->problems.elements[i]);
1717       reset_solver(solv);
1718       return 1;
1719     }
1720   sat_debug (DEBUG_1, "UNSOLVABLE\n");
1721   return 0;
1722 }
1723
1724
1725 /*-----------------------------------------------------------------*/
1726 /* Decision revert */
1727
1728 /*
1729  * revert
1730  * revert decision at level
1731  */
1732
1733 static void
1734 revert(Solver *solv, int level)
1735 {
1736   Id v, vv;
1737   while (solv->decisionq.count)
1738     {
1739       v = solv->decisionq.elements[solv->decisionq.count - 1];
1740       vv = v > 0 ? v : -v;
1741       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1742         break;
1743       sat_debug (DEBUG_4, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1744       solv->decisionmap[vv] = 0;
1745       solv->decisionq.count--;
1746       solv->decisionq_why.count--;
1747       solv->propagate_index = solv->decisionq.count;
1748     }
1749   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
1750     {
1751       solv->branches.count--;
1752       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
1753         solv->branches.count--;
1754     }
1755   solv->recommends_index = -1;
1756 }
1757
1758
1759 /*
1760  * watch2onhighest - put watch2 on literal with highest level
1761  */
1762
1763 static inline void
1764 watch2onhighest(Solver *solv, Rule *r)
1765 {
1766   int l, wl = 0;
1767   Id v, *dp;
1768
1769   if (!r->d)
1770     return;     /* binary rule, both watches are set */
1771   dp = solv->pool->whatprovidesdata + r->d;
1772   while ((v = *dp++) != 0)
1773     {
1774       l = solv->decisionmap[v < 0 ? -v : v];
1775       if (l < 0)
1776         l = -l;
1777       if (l > wl)
1778         {
1779           r->w2 = dp[-1];
1780           wl = l;
1781         }
1782     }
1783 }
1784
1785
1786 /*
1787  * setpropagatelearn
1788  *
1789  * add free decision to decision q, increase level
1790  * propagate decision, return if no conflict.
1791  * in conflict case, analyze conflict rule, add resulting
1792  * rule to learnt rule set, make decision from learnt
1793  * rule (always unit) and re-propagate.
1794  */
1795
1796 static int
1797 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
1798 {
1799   Rule *r;
1800   Id p, d;
1801   int l, why;
1802
1803   if (decision)
1804     {
1805       level++;
1806       if (decision > 0)
1807         solv->decisionmap[decision] = level;
1808       else
1809         solv->decisionmap[-decision] = -level;
1810       queue_push(&solv->decisionq, decision);
1811       queue_push(&solv->decisionq_why, 0);
1812     }
1813   for (;;)
1814     {
1815       r = propagate(solv, level);
1816       if (!r)
1817         break;
1818       if (level == 1)
1819         return analyze_unsolvable(solv, r, disablerules);
1820       sat_debug (ALWAYS, "conflict with rule #%d\n", (int)(r - solv->rules));
1821       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
1822       if (l >= level || l <= 0)
1823         abort();
1824       sat_debug (ALWAYS, "reverting decisions (level %d -> %d)\n", level, l);
1825       level = l;
1826       revert(solv, level);
1827       r = addrule(solv, p, d);       /* p requires d */
1828       if (!r)
1829         abort();
1830       if (solv->learnt_why.count != (r - solv->rules) - solv->learntrules)
1831         {
1832           sat_debug (ALWAYS, "%d %d\n", solv->learnt_why.count, (int)(r - solv->rules) - solv->learntrules);
1833           abort();
1834         }
1835       queue_push(&solv->learnt_why, why);
1836       if (d)
1837         {
1838           /* at least 2 literals, needs watches */
1839           watch2onhighest(solv, r);
1840           addwatches(solv, r);
1841         }
1842       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
1843       queue_push(&solv->decisionq, p);
1844       queue_push(&solv->decisionq_why, r - solv->rules);
1845       if (sat_debug_level() >= DEBUG_2)
1846         {
1847           sat_debug (DEBUG_2, "decision: ");
1848           printruleelement(solv, 0, p);
1849           sat_debug (DEBUG_2, "new rule: ");
1850           printrule(solv, r);
1851         }
1852     }
1853   return level;
1854 }
1855
1856
1857 /*
1858  * install best package from the queue. We add an extra package, inst, if
1859  * provided. See comment in weak install section.
1860  */
1861 static int
1862 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
1863 {
1864   Pool *pool = solv->pool;
1865   Id p;
1866   int i;
1867
1868   if (dq->count > 1 || inst)
1869     policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
1870
1871   i = 0;
1872   if (dq->count > 1)
1873     {
1874       /* choose the supplemented one */
1875       for (i = 0; i < dq->count; i++)
1876         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
1877           break;
1878       if (i == dq->count)
1879         {
1880           for (i = 1; i < dq->count; i++)
1881             queue_push(&solv->branches, dq->elements[i]);
1882           queue_push(&solv->branches, -level);
1883           i = 0;
1884         }
1885     }
1886   p = dq->elements[i];
1887
1888   sat_debug (DEBUG_4, "installing %s\n", solvable2str(pool, pool->solvables + p));
1889
1890   return setpropagatelearn(solv, level, p, disablerules);
1891 }
1892
1893
1894 /*-----------------------------------------------------------------*/
1895 /* Main solver interface */
1896
1897
1898 /*
1899  * solver_create
1900  * create solver structure
1901  *
1902  * pool: all available solvables
1903  * installed: installed Solvables
1904  *
1905  *
1906  * Upon solving, rules are created to flag the Solvables
1907  * of the 'installed' Repo as installed.
1908  */
1909
1910 Solver *
1911 solver_create(Pool *pool, Repo *installed)
1912 {
1913   Solver *solv;
1914   solv = (Solver *)xcalloc(1, sizeof(Solver));
1915   solv->pool = pool;
1916   solv->installed = installed;
1917
1918   queue_init(&solv->ruletojob);
1919   queue_init(&solv->decisionq);
1920   queue_init(&solv->decisionq_why);
1921   queue_init(&solv->problems);
1922   queue_init(&solv->suggestions);
1923   queue_init(&solv->learnt_why);
1924   queue_init(&solv->learnt_pool);
1925   queue_init(&solv->branches);
1926
1927   map_init(&solv->recommendsmap, pool->nsolvables);
1928   map_init(&solv->suggestsmap, pool->nsolvables);
1929   map_init(&solv->noupdate, installed ? installed->end - installed->start : 0);
1930   solv->recommends_index = 0;
1931
1932   solv->decisionmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
1933   solv->rules = (Rule *)xmalloc((solv->nrules + (RULES_BLOCK + 1)) * sizeof(Rule));
1934   memset(solv->rules, 0, sizeof(Rule));
1935   solv->nrules = 1;
1936
1937   return solv;
1938 }
1939
1940
1941 /*
1942  * solver_free
1943  */
1944
1945 void
1946 solver_free(Solver *solv)
1947 {
1948   queue_free(&solv->ruletojob);
1949   queue_free(&solv->decisionq);
1950   queue_free(&solv->decisionq_why);
1951   queue_free(&solv->learnt_why);
1952   queue_free(&solv->learnt_pool);
1953   queue_free(&solv->problems);
1954   queue_free(&solv->suggestions);
1955   queue_free(&solv->branches);
1956
1957   map_free(&solv->recommendsmap);
1958   map_free(&solv->suggestsmap);
1959   map_free(&solv->noupdate);
1960   xfree(solv->decisionmap);
1961   xfree(solv->rules);
1962   xfree(solv->watches);
1963   xfree(solv->weaksystemrules);
1964   xfree(solv->obsoletes);
1965   xfree(solv->obsoletes_data);
1966   xfree(solv);
1967 }
1968
1969
1970 /*-------------------------------------------------------*/
1971
1972 /*
1973  * run_solver
1974  *
1975  * all rules have been set up, now actually run the solver
1976  *
1977  */
1978
1979 static void
1980 run_solver(Solver *solv, int disablerules, int doweak)
1981 {
1982   Queue dq;
1983   int systemlevel;
1984   int level, olevel;
1985   Rule *r;
1986   int i, j, n;
1987   Solvable *s;
1988   Pool *pool = solv->pool;
1989   Id p, *dp;
1990
1991   if (sat_debug_level() >= DEBUG_4)
1992     {
1993       sat_debug (DEBUG_4, "number of rules: %d\n", solv->nrules);
1994       for (i = 0; i < solv->nrules; i++)
1995         printrule(solv, solv->rules + i);
1996     }
1997
1998   /* create watches chains */
1999   makewatches(solv);
2000
2001   sat_debug (DEBUG_1, "initial decisions: %d\n", solv->decisionq.count);
2002   if (sat_debug_level() >= DEBUG_4)
2003     printdecisions(solv);
2004
2005   /* start SAT algorithm */
2006   level = 1;
2007   systemlevel = level + 1;
2008   sat_debug (DEBUG_1, "solving...\n");
2009
2010   queue_init(&dq);
2011   for (;;)
2012     {
2013       /*
2014        * propagate
2015        */
2016
2017       if (level == 1)
2018         {
2019           sat_debug (DEBUG_1, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
2020           if ((r = propagate(solv, level)) != 0)
2021             {
2022               if (analyze_unsolvable(solv, r, disablerules))
2023                 continue;
2024               queue_free(&dq);
2025               return;
2026             }
2027         }
2028
2029       /*
2030        * installed packages
2031        */
2032
2033       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
2034         {
2035           if (!solv->updatesystem)
2036             {
2037               /* try to keep as many packages as possible */
2038               sat_debug (DEBUG_1, "installing system packages\n");
2039               for (i = solv->installed->start, n = 0; ; i++)
2040                 {
2041                   if (n == solv->installed->nsolvables)
2042                     break;
2043                   if (i == solv->installed->end)
2044                     i = solv->installed->start;
2045                   s = pool->solvables + i;
2046                   if (s->repo != solv->installed)
2047                     continue;
2048                   n++;
2049                   if (solv->decisionmap[i] != 0)
2050                     continue;
2051                   sat_debug (DEBUG_4, "keeping %s\n", solvable2str(pool, s));
2052                   olevel = level;
2053                   level = setpropagatelearn(solv, level, i, disablerules);
2054                   if (level == 0)
2055                     {
2056                       queue_free(&dq);
2057                       return;
2058                     }
2059                   if (level <= olevel)
2060                     n = 0;
2061                 }
2062             }
2063           if (solv->weaksystemrules)
2064             {
2065               sat_debug (DEBUG_1, "installing weak system packages\n");
2066               for (i = solv->installed->start; i < solv->installed->end; i++)
2067                 {
2068                   if (pool->solvables[i].repo != solv->installed)
2069                     continue;
2070                   if (solv->decisionmap[i] > 0 || (solv->decisionmap[i] < 0 && solv->weaksystemrules[i - solv->installed->start] == 0))
2071                     continue;
2072                   /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2073                   if (MAPTST(&solv->noupdate, i - solv->installed->start))
2074                     continue;
2075                   queue_empty(&dq);
2076                   if (solv->weaksystemrules[i - solv->installed->start])
2077                     {
2078                       dp = pool->whatprovidesdata + solv->weaksystemrules[i - solv->installed->start];
2079                       while ((p = *dp++) != 0)
2080                         {
2081                           if (solv->decisionmap[p] > 0)
2082                             break;
2083                           if (solv->decisionmap[p] == 0)
2084                             queue_push(&dq, p);
2085                         }
2086                       if (p)
2087                         continue;       /* update package already installed */
2088                     }
2089                   if (!dq.count && solv->decisionmap[i] != 0)
2090                     continue;
2091                   olevel = level;
2092                   /* FIXME: i is handled a bit different because we do not want
2093                    * to have it pruned just because it is not recommened.
2094                    * we should not prune installed packages instead */
2095                   level = selectandinstall(solv, level, &dq, (solv->decisionmap[i] ? 0 : i), disablerules);
2096                   if (level == 0)
2097                     {
2098                       queue_free(&dq);
2099                       return;
2100                     }
2101                   if (level <= olevel)
2102                     break;
2103                 }
2104               if (i < solv->installed->end)
2105                 continue;
2106             }
2107           systemlevel = level;
2108         }
2109
2110       /*
2111        * decide
2112        */
2113
2114       sat_debug (DEBUG_1, "deciding unresolved rules\n");
2115       for (i = 1, n = 1; ; i++, n++)
2116         {
2117           if (n == solv->nrules)
2118             break;
2119           if (i == solv->nrules)
2120             i = 1;
2121           r = solv->rules + i;
2122           if (!r->w1)
2123             continue;
2124           queue_empty(&dq);
2125           if (r->d == 0)
2126             {
2127               /* binary or unary rule */
2128               /* need two positive undecided literals */
2129               if (r->p < 0 || r->w2 <= 0)
2130                 continue;
2131               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2132                 continue;
2133               queue_push(&dq, r->p);
2134               queue_push(&dq, r->w2);
2135             }
2136           else
2137             {
2138               /* make sure that
2139                * all negative literals are installed
2140                * no positive literal is installed
2141                * i.e. the rule is not fulfilled and we
2142                * just need to decide on the positive literals
2143                */
2144               if (r->p < 0)
2145                 {
2146                   if (solv->decisionmap[-r->p] <= 0)
2147                     continue;
2148                 }
2149               else
2150                 {
2151                   if (solv->decisionmap[r->p] > 0)
2152                     continue;
2153                   if (solv->decisionmap[r->p] == 0)
2154                     queue_push(&dq, r->p);
2155                 }
2156               dp = pool->whatprovidesdata + r->d;
2157               while ((p = *dp++) != 0)
2158                 {
2159                   if (p < 0)
2160                     {
2161                       if (solv->decisionmap[-p] <= 0)
2162                         break;
2163                     }
2164                   else
2165                     {
2166                       if (solv->decisionmap[p] > 0)
2167                         break;
2168                       if (solv->decisionmap[p] == 0)
2169                         queue_push(&dq, p);
2170                     }
2171                 }
2172               if (p)
2173                 continue;
2174             }
2175           if (dq.count < 2)
2176             {
2177               /* cannot happen as this means that
2178                * the rule is unit */
2179               printrule(solv, r);
2180               abort();
2181             }
2182           if (sat_debug_level() >= DEBUG_3)
2183             printrule(solv, r);
2184
2185           olevel = level;
2186           level = selectandinstall(solv, level, &dq, 0, disablerules);
2187           if (level == 0)
2188             {
2189               queue_free(&dq);
2190               return;
2191             }
2192           if (level < systemlevel)
2193             break;
2194           n = 0;
2195         } /* for(), decide */
2196
2197       if (n != solv->nrules)    /* continue if level < systemlevel */
2198         continue;
2199
2200       if (doweak && !solv->problems.count)
2201         {
2202           int qcount;
2203
2204           sat_debug (DEBUG_1, "installing recommended packages\n");
2205           if (0)
2206             {
2207               for (i = 0; i < solv->decisionq.count; i++)
2208                 {
2209                   p = solv->decisionq.elements[i];
2210                   if (p > 0 && pool->solvables[p].repo == solv->installed)
2211                     solv->decisionmap[p] = -solv->decisionmap[p];
2212                 }
2213             }
2214           queue_empty(&dq);
2215           for (i = 1; i < pool->nsolvables; i++)
2216             {
2217               if (solv->decisionmap[i] < 0)
2218                 continue;
2219               if (solv->decisionmap[i] > 0)
2220                 {
2221                   Id *recp, rec, *pp, p;
2222                   s = pool->solvables + i;
2223                   /* installed, check for recommends */
2224                   /* XXX need to special case AND ? */
2225                   if (s->recommends)
2226                     {
2227                       recp = s->repo->idarraydata + s->recommends;
2228                       while ((rec = *recp++) != 0)
2229                         {
2230                           qcount = dq.count;
2231                           FOR_PROVIDES(p, pp, rec)
2232                             {
2233                               if (solv->decisionmap[p] > 0)
2234                                 {
2235                                   dq.count = qcount;
2236                                   break;
2237                                 }
2238                               else if (solv->decisionmap[p] == 0)
2239                                 {
2240                                   queue_pushunique(&dq, p);
2241                                 }
2242                             }
2243                         }
2244                     }
2245                 }
2246               else
2247                 {
2248                   s = pool->solvables + i;
2249                   if (!s->supplements && !s->freshens)
2250                     continue;
2251                   if (!pool_installable(pool, s))
2252                     continue;
2253                   if (solver_is_supplementing(solv, s))
2254                     queue_pushunique(&dq, i);
2255                 }
2256             }
2257           if (0)
2258             {
2259               for (i = 0; i < solv->decisionq.count; i++)
2260                 {
2261                   p = solv->decisionq.elements[i];
2262                   if (p > 0 && pool->solvables[p].repo == solv->installed)
2263                     solv->decisionmap[p] = -solv->decisionmap[p];
2264                 }
2265             }
2266           if (dq.count)
2267             {
2268               if (dq.count > 1)
2269                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2270               p = dq.elements[0];
2271               sat_debug (DEBUG_1, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2272               level = setpropagatelearn(solv, level, p, 0);
2273               continue;
2274             }
2275         }
2276
2277      if (solv->solution_callback)
2278         {
2279           solv->solution_callback(solv, solv->solution_callback_data);
2280           if (solv->branches.count)
2281             {
2282               int i = solv->branches.count - 1;
2283               int l = -solv->branches.elements[i];
2284               for (; i > 0; i--)
2285                 if (solv->branches.elements[i - 1] < 0)
2286                   break;
2287               p = solv->branches.elements[i];
2288               sat_debug (DEBUG_1, "branching with %s\n", solvable2str(pool, pool->solvables + p));
2289               queue_empty(&dq);
2290               for (j = i + 1; j < solv->branches.count; j++)
2291                 queue_push(&dq, solv->branches.elements[j]);
2292               solv->branches.count = i;
2293               level = l;
2294               revert(solv, level);
2295               if (dq.count > 1)
2296                 for (j = 0; j < dq.count; j++)
2297                   queue_push(&solv->branches, dq.elements[j]);
2298               olevel = level;
2299               level = setpropagatelearn(solv, level, p, disablerules);
2300               if (level == 0)
2301                 {
2302                   queue_free(&dq);
2303                   return;
2304                 }
2305               continue;
2306             }
2307           /* all branches done, we're finally finished */
2308           break;
2309         }
2310
2311       /* minimization step */
2312      if (solv->branches.count)
2313         {
2314           int l = 0, lasti = -1, lastl = -1;
2315           p = 0;
2316           for (i = solv->branches.count - 1; i >= 0; i--)
2317             {
2318               p = solv->branches.elements[i];
2319               if (p < 0)
2320                 l = -p;
2321               else if (p > 0 && solv->decisionmap[p] > l + 1)
2322                 {
2323                   lasti = i;
2324                   lastl = l;
2325                 }
2326             }
2327           if (lasti >= 0)
2328             {
2329               /* kill old solvable so that we do not loop */
2330               p = solv->branches.elements[lasti];
2331               solv->branches.elements[lasti] = 0;
2332               sat_debug (DEBUG_1, "minimizing %d -> %d with %s\n", solv->decisionmap[p], l, solvable2str(pool, pool->solvables + p));
2333
2334               level = lastl;
2335               revert(solv, level);
2336               olevel = level;
2337               level = setpropagatelearn(solv, level, p, disablerules);
2338               if (level == 0)
2339                 {
2340                   queue_free(&dq);
2341                   return;
2342                 }
2343               continue;
2344             }
2345         }
2346       break;
2347     }
2348   queue_free(&dq);
2349 }
2350
2351
2352 /*
2353  * refine_suggestion
2354  * at this point, all rules that led to conflicts are disabled.
2355  * we re-enable all rules of a problem set but rule "sug", then
2356  * continue to disable more rules until there as again a solution.
2357  */
2358
2359 /* FIXME: think about conflicting assertions */
2360
2361 static void
2362 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2363 {
2364   Rule *r;
2365   int i, j;
2366   Id v;
2367   Queue disabled;
2368   int disabledcnt;
2369
2370   if (sat_debug_level() >= DEBUG_1)
2371     {
2372       sat_debug (DEBUG_1, "refine_suggestion start\n");
2373       for (i = 0; problem[i]; i++)
2374         {
2375           if (problem[i] == sug)
2376             sat_debug (DEBUG_1, "=> ");
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           sat_debug (DEBUG_1, "no more problems!\n");
2413           if (sat_debug_level() >= DEBUG_4)
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           sat_debug (DEBUG_1, "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 (sat_debug_level() >= DEBUG_2)
2453             {
2454               sat_debug (DEBUG_2, "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   sat_debug (DEBUG_1,"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           sat_debug (ALWAYS, "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           sat_debug (ALWAYS, "install %s", solvable2str(pool, s));
2719         }
2720       else
2721         {
2722           sat_debug (ALWAYS, "update  %s", solvable2str(pool, s));
2723           sat_debug (ALWAYS, "  (obsoletes");
2724           for (j = installed->start; j < installed->end; j++)
2725             if (obsoletesmap[j] == p)
2726               sat_debug (ALWAYS," %s", solvable2str(pool, pool->solvables + j));
2727           sat_debug (ALWAYS,")");
2728         }
2729       sat_debug (ALWAYS, "\n");
2730     }
2731
2732   xfree(obsoletesmap);
2733
2734   if (solv->suggestions.count)
2735     {
2736       sat_debug (ALWAYS, "\nsuggested packages:\n");
2737       for (i = 0; i < solv->suggestions.count; i++)
2738         {
2739           s = pool->solvables + solv->suggestions.elements[i];
2740           sat_debug (ALWAYS, "- %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               sat_debug (ALWAYS, "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               sat_debug (ALWAYS, "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               sat_debug (ALWAYS, "no solvable exists with name %s\n", dep2str(pool, what));
2824               break;
2825             case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2826               sat_debug (ALWAYS, "no solvable provides %s\n", dep2str(pool, what));
2827               break;
2828             default:
2829               sat_debug (ALWAYS, "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           sat_debug (ALWAYS, "some job/system/learnt rule\n");
2844           printrule(solv, 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               sat_debug (ALWAYS, "package %s requires %s, but no package provides it\n", solvable2str(pool, s), dep2str(pool, req));
2862               count++;
2863             }
2864         }
2865       if (!count)
2866         sat_debug (ALWAYS, "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       sat_debug (ALWAYS, "some learnt rule...\n");
2874       printrule(solv, r);
2875       return;
2876     }
2877   if (rn >= solv->systemrules)
2878     {
2879       /* system rule, ignore for now */
2880       sat_debug (ALWAYS, "some system rule...\n");
2881       printrule(solv, r);
2882       return;
2883     }
2884   if (rn >= solv->jobrules)
2885     {
2886       /* job rule, ignore for now */
2887       sat_debug (ALWAYS, "some job rule...\n");
2888       printrule(solv, 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           sat_debug (ALWAYS, "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           sat_debug (ALWAYS, "req not found\n");
2934           abort();
2935         }
2936       sat_debug (ALWAYS, "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   sat_debug (ALWAYS, "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       sat_debug (ALWAYS, "Problem %d:\n", pcnt++);
2955       sat_debug (ALWAYS, "====================================\n");
2956       printprobleminfo(solv, job, problem);
2957       sat_debug (ALWAYS, "\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                         sat_debug (ALWAYS, "- do not keep %s installed\n", solvable2str(pool, s));
2974                       else
2975                         sat_debug (ALWAYS, "- 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                         sat_debug (ALWAYS, "- do not deinstall %s\n", solvable2str(pool, s));
2981                       else
2982                         sat_debug (ALWAYS, "- do not forbid installation of %s\n", solvable2str(pool, s));
2983                       break;
2984                     case SOLVER_INSTALL_SOLVABLE_NAME:
2985                       sat_debug (ALWAYS, "- do not install %s\n", id2str(pool, what));
2986                       break;
2987                     case SOLVER_ERASE_SOLVABLE_NAME:
2988                       sat_debug (ALWAYS, "- do not deinstall %s\n", id2str(pool, what));
2989                       break;
2990                     case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2991                       sat_debug (ALWAYS, "- do not install a solvable providing %s\n", dep2str(pool, what));
2992                       break;
2993                     case SOLVER_ERASE_SOLVABLE_PROVIDES:
2994                       sat_debug (ALWAYS, "- 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                       sat_debug (ALWAYS, "- do not install most recent version of %s\n", solvable2str(pool, s));
2999                       break;
3000                     default:
3001                       sat_debug (ALWAYS, "- 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                           sat_debug (ALWAYS, "- 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                           sat_debug (ALWAYS, "- 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                             sat_debug (ALWAYS, "- 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                             sat_debug (ALWAYS, "- 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                         sat_debug (ALWAYS, "- allow replacement of %s with %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3033                     }
3034                   else
3035                     {
3036                       sat_debug (ALWAYS, "- allow deinstallation of %s\n", solvable2str(pool, s));
3037                     }
3038
3039                 }
3040             }
3041           sat_debug (ALWAYS, "\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   sat_debug (DEBUG_1, "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       sat_debug (DEBUG_4, "*** create rpm rules for installed solvables ***\n");
3170       FOR_REPO_SOLVABLES(installed, p, s)
3171         addrpmrulesforsolvable(solv, s, &addedmap);
3172       sat_debug (DEBUG_1, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
3173       sat_debug (DEBUG_4, "*** 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       sat_debug (DEBUG_1, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
3178     }
3179
3180   sat_debug (DEBUG_4, "*** 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   sat_debug (DEBUG_1, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
3209
3210   sat_debug (DEBUG_4, "*** create rpm rules for recommended/suggested packages ***\n");
3211
3212   oldnrules = solv->nrules;
3213   addrpmrulesforweak(solv, &addedmap);
3214   sat_debug (DEBUG_1, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
3215
3216 #if 1
3217   if (sat_debug_level() >= DEBUG_1)
3218     {
3219       int possible = 0, installable = 0;
3220       for (i = 1; i < pool->nsolvables; i++)
3221         {
3222           if (pool_installable(pool, pool->solvables + i))
3223             installable++;
3224           if (MAPTST(&addedmap, i))
3225             possible++;
3226         }
3227       sat_debug (DEBUG_1, "%d of %d installable solvables considered for solving\n", possible, installable);
3228     }
3229 #endif
3230
3231   /*
3232    * first pass done, we now have all the rpm rules we need.
3233    * unify existing rules before going over all job rules and
3234    * policy rules.
3235    * at this point the system is always solvable,
3236    * as an empty system (remove all packages) is a valid solution
3237    */
3238
3239   unifyrules(solv);     /* remove duplicate rpm rules */
3240
3241   sat_debug (DEBUG_1, "decisions so far: %d\n", solv->decisionq.count);
3242   if (sat_debug_level() >= DEBUG_4)
3243     printdecisions (solv);
3244
3245   /*
3246    * now add all job rules
3247    */
3248
3249   sat_debug (DEBUG_4, "*** Add JOB rules ***\n");
3250
3251   solv->jobrules = solv->nrules;
3252
3253   for (i = 0; i < job->count; i += 2)
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           sat_debug (DEBUG_1, "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           sat_debug (DEBUG_1, "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             sat_debug (DEBUG_1, "job: install name %s\n", id2str(pool, what));
3275           if (how == SOLVER_INSTALL_SOLVABLE_PROVIDES)
3276             sat_debug (DEBUG_1, "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             sat_debug (DEBUG_1, "job: erase name %s\n", id2str(pool, what));
3303           if (how == SOLVER_ERASE_SOLVABLE_PROVIDES)
3304             sat_debug (DEBUG_1, "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           sat_debug (DEBUG_1, "job: update %s\n", solvable2str(pool, s));
3317           addupdaterule(solv, s, 0);
3318           queue_push(&solv->ruletojob, i);
3319           break;
3320         }
3321     }
3322
3323   if (solv->ruletojob.count != solv->nrules - solv->jobrules)
3324     abort();
3325
3326   /*
3327    * now add system rules
3328    *
3329    */
3330
3331   sat_debug (DEBUG_4, "*** Add system rules ***\n");
3332
3333
3334   solv->systemrules = solv->nrules;
3335
3336   /*
3337    * create rules for updating installed solvables
3338    *
3339    */
3340
3341   if (installed && !solv->allowuninstall)
3342     {                                  /* loop over all installed solvables */
3343       /* we create all update rules, but disable some later on depending on the job */
3344       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3345         if (s->repo == installed)
3346           addupdaterule(solv, s, 0); /* allowall = 0 */
3347         else
3348           addupdaterule(solv, 0, 0);    /* create dummy rule;  allowall = 0  */
3349       /* consistency check: we added a rule for _every_ system solvable */
3350       if (solv->nrules - solv->systemrules != installed->end - installed->start)
3351         abort();
3352     }
3353
3354   /* create special weak system rules */
3355   /* those are used later on to keep a version of the installed packages in
3356      best effort mode */
3357   if (installed && installed->nsolvables)
3358     {
3359       solv->weaksystemrules = xcalloc(installed->end - installed->start, sizeof(Id));
3360       FOR_REPO_SOLVABLES(installed, p, s)
3361         {
3362           policy_findupdatepackages(solv, s, &q, 1);
3363           if (q.count)
3364             solv->weaksystemrules[p - installed->start] = pool_queuetowhatprovides(pool, &q);
3365         }
3366     }
3367
3368   /* free unneeded memory */
3369   map_free(&addedmap);
3370   queue_free(&q);
3371
3372   solv->weakrules = solv->nrules;
3373
3374   /* try real hard to keep packages installed */
3375   if (0)
3376     {
3377       FOR_REPO_SOLVABLES(installed, p, s)
3378         {
3379           /* FIXME: can't work with refine_suggestion! */
3380           /* need to always add the rule but disable it */
3381           if (MAPTST(&solv->noupdate, p - installed->start))
3382             continue;
3383           d = solv->weaksystemrules[p - installed->start];
3384           addrule(solv, p, d);
3385         }
3386     }
3387
3388   /* all new rules are learnt after this point */
3389   solv->learntrules = solv->nrules;
3390
3391   /*
3392    * solve !
3393    *
3394    */
3395
3396   disableupdaterules(solv, job, -1);
3397   makeruledecisions(solv);
3398
3399   sat_debug (DEBUG_1, "problems so far: %d\n", solv->problems.count);
3400
3401   run_solver(solv, 1, 1);
3402
3403   /* find suggested packages */
3404   if (!solv->problems.count)
3405     {
3406       Id sug, *sugp, p, *pp;
3407
3408       /* create map of all suggests that are still open */
3409       solv->recommends_index = -1;
3410       MAPZERO(&solv->suggestsmap);
3411       for (i = 0; i < solv->decisionq.count; i++)
3412         {
3413           p = solv->decisionq.elements[i];
3414           if (p < 0)
3415             continue;
3416           s = pool->solvables + p;
3417           if (s->suggests)
3418             {
3419               sugp = s->repo->idarraydata + s->suggests;
3420               while ((sug = *sugp++) != 0)
3421                 {
3422                   FOR_PROVIDES(p, pp, sug)
3423                     if (solv->decisionmap[p] > 0)
3424                       break;
3425                   if (p)
3426                     continue;   /* already fulfilled */
3427                   FOR_PROVIDES(p, pp, sug)
3428                     MAPSET(&solv->suggestsmap, p);
3429                 }
3430             }
3431         }
3432       for (i = 1; i < pool->nsolvables; i++)
3433         {
3434           if (solv->decisionmap[i] != 0)
3435             continue;
3436           s = pool->solvables + i;
3437           if (!MAPTST(&solv->suggestsmap, i))
3438             {
3439               if (!s->enhances)
3440                 continue;
3441               if (!pool_installable(pool, s))
3442                 continue;
3443               if (!solver_is_enhancing(solv, s))
3444                 continue;
3445             }
3446           queue_push(&solv->suggestions, i);
3447         }
3448       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
3449     }
3450
3451   if (solv->problems.count)
3452     problems_to_solutions(solv, job);
3453 }
3454