satsolver 0.16.3
|
00001 /* 00002 * Copyright (c) 2007-2008, Novell Inc. 00003 * 00004 * This program is licensed under the BSD license, read LICENSE.BSD 00005 * for further information 00006 */ 00007 00008 /* 00009 * solver.c 00010 * 00011 * SAT based dependency solver 00012 */ 00013 00014 #include <stdio.h> 00015 #include <stdlib.h> 00016 #include <unistd.h> 00017 #include <string.h> 00018 #include <assert.h> 00019 00020 #include "solver.h" 00021 #include "bitmap.h" 00022 #include "pool.h" 00023 #include "util.h" 00024 #include "policy.h" 00025 #include "solverdebug.h" 00026 00027 #define RULES_BLOCK 63 00028 00029 /******************************************************************** 00030 * 00031 * dependency check helpers 00032 * 00033 */ 00034 00035 /*------------------------------------------------------------------- 00036 * handle split provides 00037 */ 00038 00039 int 00040 solver_splitprovides(Solver *solv, Id dep) 00041 { 00042 Pool *pool = solv->pool; 00043 Id p, pp; 00044 Reldep *rd; 00045 Solvable *s; 00046 00047 if (!solv->dosplitprovides || !solv->installed) 00048 return 0; 00049 if (!ISRELDEP(dep)) 00050 return 0; 00051 rd = GETRELDEP(pool, dep); 00052 if (rd->flags != REL_WITH) 00053 return 0; 00054 FOR_PROVIDES(p, pp, dep) 00055 { 00056 s = pool->solvables + p; 00057 if (s->repo == solv->installed && s->name == rd->name) 00058 return 1; 00059 } 00060 return 0; 00061 } 00062 00063 00064 /*------------------------------------------------------------------- 00065 * solver_dep_installed 00066 */ 00067 00068 int 00069 solver_dep_installed(Solver *solv, Id dep) 00070 { 00071 #if 0 00072 Pool *pool = solv->pool; 00073 Id p, pp; 00074 00075 if (ISRELDEP(dep)) 00076 { 00077 Reldep *rd = GETRELDEP(pool, dep); 00078 if (rd->flags == REL_AND) 00079 { 00080 if (!solver_dep_installed(solv, rd->name)) 00081 return 0; 00082 return solver_dep_installed(solv, rd->evr); 00083 } 00084 if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED) 00085 return solver_dep_installed(solv, rd->evr); 00086 } 00087 FOR_PROVIDES(p, pp, dep) 00088 { 00089 if (p == SYSTEMSOLVABLE || (solv->installed && pool->solvables[p].repo == solv->installed)) 00090 return 1; 00091 } 00092 #endif 00093 return 0; 00094 } 00095 00096 00097 00098 /************************************************************************/ 00099 00100 /* 00101 * make assertion rules into decisions 00102 * 00103 * Go through rules and add direct assertions to the decisionqueue. 00104 * If we find a conflict, disable rules and add them to problem queue. 00105 */ 00106 00107 static void 00108 makeruledecisions(Solver *solv) 00109 { 00110 Pool *pool = solv->pool; 00111 int i, ri, ii; 00112 Rule *r, *rr; 00113 Id v, vv; 00114 int decisionstart; 00115 00116 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions ; size decisionq: %d -----\n",solv->decisionq.count); 00117 00118 /* The system solvable is always installed first */ 00119 assert(solv->decisionq.count == 0); 00120 queue_push(&solv->decisionq, SYSTEMSOLVABLE); 00121 queue_push(&solv->decisionq_why, 0); 00122 solv->decisionmap[SYSTEMSOLVABLE] = 1; /* installed at level '1' */ 00123 00124 decisionstart = solv->decisionq.count; 00125 for (ii = 0; ii < solv->ruleassertions.count; ii++) 00126 { 00127 ri = solv->ruleassertions.elements[ii]; 00128 r = solv->rules + ri; 00129 00130 if (r->d < 0 || !r->p || r->w2) /* disabled, dummy or no assertion */ 00131 continue; 00132 /* do weak rules in phase 2 */ 00133 if (ri < solv->learntrules && MAPTST(&solv->weakrulemap, ri)) 00134 continue; 00135 00136 v = r->p; 00137 vv = v > 0 ? v : -v; 00138 00139 if (!solv->decisionmap[vv]) /* if not yet decided */ 00140 { 00141 /* 00142 * decide ! 00143 */ 00144 queue_push(&solv->decisionq, v); 00145 queue_push(&solv->decisionq_why, r - solv->rules); 00146 solv->decisionmap[vv] = v > 0 ? 1 : -1; 00147 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE) 00148 { 00149 Solvable *s = solv->pool->solvables + vv; 00150 if (v < 0) 00151 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "conflicting %s (assertion)\n", solvable2str(solv->pool, s)); 00152 else 00153 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "installing %s (assertion)\n", solvable2str(solv->pool, s)); 00154 } 00155 continue; 00156 } 00157 /* 00158 * check previous decision: is it sane ? 00159 */ 00160 00161 if (v > 0 && solv->decisionmap[vv] > 0) /* ok to install */ 00162 continue; 00163 if (v < 0 && solv->decisionmap[vv] < 0) /* ok to remove */ 00164 continue; 00165 00166 /* 00167 * found a conflict! 00168 * 00169 * The rule (r) we're currently processing says something 00170 * different (v = r->p) than a previous decision (decisionmap[abs(v)]) 00171 * on this literal 00172 */ 00173 00174 if (ri >= solv->learntrules) 00175 { 00176 /* conflict with a learnt rule */ 00177 /* can happen when packages cannot be installed for 00178 * multiple reasons. */ 00179 /* we disable the learnt rule in this case */ 00180 solver_disablerule(solv, r); 00181 continue; 00182 } 00183 00184 /* 00185 * find the decision which is the "opposite" of the rule 00186 */ 00187 00188 for (i = 0; i < solv->decisionq.count; i++) 00189 if (solv->decisionq.elements[i] == -v) 00190 break; 00191 assert(i < solv->decisionq.count); /* assert that we found it */ 00192 00193 /* 00194 * conflict with system solvable ? 00195 */ 00196 00197 if (v == -SYSTEMSOLVABLE) { 00198 /* conflict with system solvable */ 00199 queue_push(&solv->problems, solv->learnt_pool.count); 00200 queue_push(&solv->learnt_pool, ri); 00201 queue_push(&solv->learnt_pool, 0); 00202 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with system solvable, disabling rule #%d\n", ri); 00203 if (ri >= solv->jobrules && ri < solv->jobrules_end) 00204 v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1); 00205 else 00206 v = ri; 00207 queue_push(&solv->problems, v); 00208 queue_push(&solv->problems, 0); 00209 solver_disableproblem(solv, v); 00210 continue; 00211 } 00212 00213 assert(solv->decisionq_why.elements[i] > 0); 00214 00215 /* 00216 * conflict with an rpm rule ? 00217 */ 00218 00219 if (solv->decisionq_why.elements[i] < solv->rpmrules_end) 00220 { 00221 /* conflict with rpm rule assertion */ 00222 queue_push(&solv->problems, solv->learnt_pool.count); 00223 queue_push(&solv->learnt_pool, ri); 00224 queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]); 00225 queue_push(&solv->learnt_pool, 0); 00226 assert(v > 0 || v == -SYSTEMSOLVABLE); 00227 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with rpm rule, disabling rule #%d\n", ri); 00228 if (ri >= solv->jobrules && ri < solv->jobrules_end) 00229 v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1); 00230 else 00231 v = ri; 00232 queue_push(&solv->problems, v); 00233 queue_push(&solv->problems, 0); 00234 solver_disableproblem(solv, v); 00235 continue; 00236 } 00237 00238 /* 00239 * conflict with another job or update/feature rule 00240 */ 00241 00242 /* record proof */ 00243 queue_push(&solv->problems, solv->learnt_pool.count); 00244 queue_push(&solv->learnt_pool, ri); 00245 queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]); 00246 queue_push(&solv->learnt_pool, 0); 00247 00248 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflicting update/job assertions over literal %d\n", vv); 00249 00250 /* 00251 * push all of our rules (can only be feature or job rules) 00252 * asserting this literal on the problem stack 00253 */ 00254 00255 for (i = solv->featurerules, rr = solv->rules + i; i < solv->learntrules; i++, rr++) 00256 { 00257 if (rr->d < 0 /* disabled */ 00258 || rr->w2) /* or no assertion */ 00259 continue; 00260 if (rr->p != vv /* not affecting the literal */ 00261 && rr->p != -vv) 00262 continue; 00263 if (MAPTST(&solv->weakrulemap, i)) /* weak: silently ignore */ 00264 continue; 00265 00266 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, " - disabling rule #%d\n", i); 00267 00268 solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, solv->rules + i); 00269 00270 v = i; 00271 /* is is a job rule ? */ 00272 if (i >= solv->jobrules && i < solv->jobrules_end) 00273 v = -(solv->ruletojob.elements[i - solv->jobrules] + 1); 00274 00275 queue_push(&solv->problems, v); 00276 solver_disableproblem(solv, v); 00277 } 00278 queue_push(&solv->problems, 0); 00279 00280 /* 00281 * start over 00282 * (back up from decisions) 00283 */ 00284 while (solv->decisionq.count > decisionstart) 00285 { 00286 v = solv->decisionq.elements[--solv->decisionq.count]; 00287 --solv->decisionq_why.count; 00288 vv = v > 0 ? v : -v; 00289 solv->decisionmap[vv] = 0; 00290 } 00291 ii = -1; /* restarts loop at 0 */ 00292 } 00293 00294 /* 00295 * phase 2: now do the weak assertions 00296 */ 00297 for (ii = 0; ii < solv->ruleassertions.count; ii++) 00298 { 00299 ri = solv->ruleassertions.elements[ii]; 00300 r = solv->rules + ri; 00301 if (r->d < 0 || r->w2) /* disabled or no assertion */ 00302 continue; 00303 if (ri >= solv->learntrules || !MAPTST(&solv->weakrulemap, ri)) /* skip non-weak */ 00304 continue; 00305 v = r->p; 00306 vv = v > 0 ? v : -v; 00307 /* 00308 * decide ! 00309 * (if not yet decided) 00310 */ 00311 if (!solv->decisionmap[vv]) 00312 { 00313 queue_push(&solv->decisionq, v); 00314 queue_push(&solv->decisionq_why, r - solv->rules); 00315 solv->decisionmap[vv] = v > 0 ? 1 : -1; 00316 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE) 00317 { 00318 Solvable *s = solv->pool->solvables + vv; 00319 if (v < 0) 00320 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "conflicting %s (weak assertion)\n", solvable2str(solv->pool, s)); 00321 else 00322 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "installing %s (weak assertion)\n", solvable2str(solv->pool, s)); 00323 } 00324 continue; 00325 } 00326 /* 00327 * previously decided, sane ? 00328 */ 00329 if (v > 0 && solv->decisionmap[vv] > 0) 00330 continue; 00331 if (v < 0 && solv->decisionmap[vv] < 0) 00332 continue; 00333 00334 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "assertion conflict, but I am weak, disabling "); 00335 solver_printrule(solv, SAT_DEBUG_UNSOLVABLE, r); 00336 00337 if (ri >= solv->jobrules && ri < solv->jobrules_end) 00338 v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1); 00339 else 00340 v = ri; 00341 solver_disableproblem(solv, v); 00342 if (v < 0) 00343 solver_reenablepolicyrules(solv, -(v + 1)); 00344 } 00345 00346 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions end; size decisionq: %d -----\n",solv->decisionq.count); 00347 } 00348 00349 00350 /*------------------------------------------------------------------- 00351 * enable/disable learnt rules 00352 * 00353 * we have enabled or disabled some of our rules. We now reenable all 00354 * of our learnt rules except the ones that were learnt from rules that 00355 * are now disabled. 00356 */ 00357 static void 00358 enabledisablelearntrules(Solver *solv) 00359 { 00360 Pool *pool = solv->pool; 00361 Rule *r; 00362 Id why, *whyp; 00363 int i; 00364 00365 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "enabledisablelearntrules called\n"); 00366 for (i = solv->learntrules, r = solv->rules + i; i < solv->nrules; i++, r++) 00367 { 00368 whyp = solv->learnt_pool.elements + solv->learnt_why.elements[i - solv->learntrules]; 00369 while ((why = *whyp++) != 0) 00370 { 00371 assert(why > 0 && why < i); 00372 if (solv->rules[why].d < 0) 00373 break; 00374 } 00375 /* why != 0: we found a disabled rule, disable the learnt rule */ 00376 if (why && r->d >= 0) 00377 { 00378 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS) 00379 { 00380 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "disabling "); 00381 solver_printruleclass(solv, SAT_DEBUG_SOLUTIONS, r); 00382 } 00383 solver_disablerule(solv, r); 00384 } 00385 else if (!why && r->d < 0) 00386 { 00387 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS) 00388 { 00389 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "re-enabling "); 00390 solver_printruleclass(solv, SAT_DEBUG_SOLUTIONS, r); 00391 } 00392 solver_enablerule(solv, r); 00393 } 00394 } 00395 } 00396 00397 00398 /********************************************************************/ 00399 /* watches */ 00400 00401 00402 /*------------------------------------------------------------------- 00403 * makewatches 00404 * 00405 * initial setup for all watches 00406 */ 00407 00408 static void 00409 makewatches(Solver *solv) 00410 { 00411 Rule *r; 00412 int i; 00413 int nsolvables = solv->pool->nsolvables; 00414 00415 sat_free(solv->watches); 00416 /* lower half for removals, upper half for installs */ 00417 solv->watches = sat_calloc(2 * nsolvables, sizeof(Id)); 00418 #if 1 00419 /* do it reverse so rpm rules get triggered first (XXX: obsolete?) */ 00420 for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--) 00421 #else 00422 for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++) 00423 #endif 00424 { 00425 if (!r->w2) /* assertions do not need watches */ 00426 continue; 00427 00428 /* see addwatches_rule(solv, r) */ 00429 r->n1 = solv->watches[nsolvables + r->w1]; 00430 solv->watches[nsolvables + r->w1] = r - solv->rules; 00431 00432 r->n2 = solv->watches[nsolvables + r->w2]; 00433 solv->watches[nsolvables + r->w2] = r - solv->rules; 00434 } 00435 } 00436 00437 00438 /*------------------------------------------------------------------- 00439 * 00440 * add watches (for a new learned rule) 00441 * sets up watches for a single rule 00442 * 00443 * see also makewatches() above. 00444 */ 00445 00446 static inline void 00447 addwatches_rule(Solver *solv, Rule *r) 00448 { 00449 int nsolvables = solv->pool->nsolvables; 00450 00451 r->n1 = solv->watches[nsolvables + r->w1]; 00452 solv->watches[nsolvables + r->w1] = r - solv->rules; 00453 00454 r->n2 = solv->watches[nsolvables + r->w2]; 00455 solv->watches[nsolvables + r->w2] = r - solv->rules; 00456 } 00457 00458 00459 /********************************************************************/ 00460 /* 00461 * rule propagation 00462 */ 00463 00464 00465 /* shortcuts to check if a literal (positive or negative) assignment 00466 * evaluates to 'true' or 'false' 00467 */ 00468 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0)) 00469 #define DECISIONMAP_FALSE(p) ((p) > 0 ? (decisionmap[p] < 0) : (decisionmap[-p] > 0)) 00470 #define DECISIONMAP_UNDEF(p) (decisionmap[(p) > 0 ? (p) : -(p)] == 0) 00471 00472 /*------------------------------------------------------------------- 00473 * 00474 * propagate 00475 * 00476 * make decision and propagate to all rules 00477 * 00478 * Evaluate each term affected by the decision (linked through watches) 00479 * If we find unit rules we make new decisions based on them 00480 * 00481 * Everything's fixed there, it's just finding rules that are 00482 * unit. 00483 * 00484 * return : 0 = everything is OK 00485 * rule = conflict found in this rule 00486 */ 00487 00488 static Rule * 00489 propagate(Solver *solv, int level) 00490 { 00491 Pool *pool = solv->pool; 00492 Id *rp, *next_rp; /* rule pointer, next rule pointer in linked list */ 00493 Rule *r; /* rule */ 00494 Id p, pkg, other_watch; 00495 Id *dp; 00496 Id *decisionmap = solv->decisionmap; 00497 00498 Id *watches = solv->watches + pool->nsolvables; /* place ptr in middle */ 00499 00500 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate -----\n"); 00501 00502 /* foreach non-propagated decision */ 00503 while (solv->propagate_index < solv->decisionq.count) 00504 { 00505 /* 00506 * 'pkg' was just decided 00507 * negate because our watches trigger if literal goes FALSE 00508 */ 00509 pkg = -solv->decisionq.elements[solv->propagate_index++]; 00510 00511 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE) 00512 { 00513 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagate for decision %d level %d\n", -pkg, level); 00514 solver_printruleelement(solv, SAT_DEBUG_PROPAGATE, 0, -pkg); 00515 } 00516 00517 /* foreach rule where 'pkg' is now FALSE */ 00518 for (rp = watches + pkg; *rp; rp = next_rp) 00519 { 00520 r = solv->rules + *rp; 00521 if (r->d < 0) 00522 { 00523 /* rule is disabled, goto next */ 00524 if (pkg == r->w1) 00525 next_rp = &r->n1; 00526 else 00527 next_rp = &r->n2; 00528 continue; 00529 } 00530 00531 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE) 00532 { 00533 POOL_DEBUG(SAT_DEBUG_PROPAGATE," watch triggered "); 00534 solver_printrule(solv, SAT_DEBUG_PROPAGATE, r); 00535 } 00536 00537 /* 'pkg' was just decided (was set to FALSE) 00538 * 00539 * now find other literal watch, check clause 00540 * and advance on linked list 00541 */ 00542 if (pkg == r->w1) 00543 { 00544 other_watch = r->w2; 00545 next_rp = &r->n1; 00546 } 00547 else 00548 { 00549 other_watch = r->w1; 00550 next_rp = &r->n2; 00551 } 00552 00553 /* 00554 * This term is already true (through the other literal) 00555 * so we have nothing to do 00556 */ 00557 if (DECISIONMAP_TRUE(other_watch)) 00558 continue; 00559 00560 /* 00561 * The other literal is FALSE or UNDEF 00562 * 00563 */ 00564 00565 if (r->d) 00566 { 00567 /* Not a binary clause, try to move our watch. 00568 * 00569 * Go over all literals and find one that is 00570 * not other_watch 00571 * and not FALSE 00572 * 00573 * (TRUE is also ok, in that case the rule is fulfilled) 00574 */ 00575 if (r->p /* we have a 'p' */ 00576 && r->p != other_watch /* which is not watched */ 00577 && !DECISIONMAP_FALSE(r->p)) /* and not FALSE */ 00578 { 00579 p = r->p; 00580 } 00581 else /* go find a 'd' to make 'true' */ 00582 { 00583 /* foreach p in 'd' 00584 we just iterate sequentially, doing it in another order just changes the order of decisions, not the decisions itself 00585 */ 00586 for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;) 00587 { 00588 if (p != other_watch /* which is not watched */ 00589 && !DECISIONMAP_FALSE(p)) /* and not FALSE */ 00590 break; 00591 } 00592 } 00593 00594 if (p) 00595 { 00596 /* 00597 * if we found some p that is UNDEF or TRUE, move 00598 * watch to it 00599 */ 00600 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE) 00601 { 00602 if (p > 0) 00603 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " -> move w%d to %s\n", (pkg == r->w1 ? 1 : 2), solvid2str(pool, p)); 00604 else 00605 POOL_DEBUG(SAT_DEBUG_PROPAGATE," -> move w%d to !%s\n", (pkg == r->w1 ? 1 : 2), solvid2str(pool, -p)); 00606 } 00607 00608 *rp = *next_rp; 00609 next_rp = rp; 00610 00611 if (pkg == r->w1) 00612 { 00613 r->w1 = p; 00614 r->n1 = watches[p]; 00615 } 00616 else 00617 { 00618 r->w2 = p; 00619 r->n2 = watches[p]; 00620 } 00621 watches[p] = r - solv->rules; 00622 continue; 00623 } 00624 /* search failed, thus all unwatched literals are FALSE */ 00625 00626 } /* not binary */ 00627 00628 /* 00629 * unit clause found, set literal other_watch to TRUE 00630 */ 00631 00632 if (DECISIONMAP_FALSE(other_watch)) /* check if literal is FALSE */ 00633 return r; /* eek, a conflict! */ 00634 00635 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE) 00636 { 00637 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " unit "); 00638 solver_printrule(solv, SAT_DEBUG_PROPAGATE, r); 00639 } 00640 00641 if (other_watch > 0) 00642 decisionmap[other_watch] = level; /* install! */ 00643 else 00644 decisionmap[-other_watch] = -level; /* remove! */ 00645 00646 queue_push(&solv->decisionq, other_watch); 00647 queue_push(&solv->decisionq_why, r - solv->rules); 00648 00649 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE) 00650 { 00651 if (other_watch > 0) 00652 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " -> decided to install %s\n", solvid2str(pool, other_watch)); 00653 else 00654 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " -> decided to conflict %s\n", solvid2str(pool, -other_watch)); 00655 } 00656 00657 } /* foreach rule involving 'pkg' */ 00658 00659 } /* while we have non-decided decisions */ 00660 00661 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate end-----\n"); 00662 00663 return 0; /* all is well */ 00664 } 00665 00666 00667 /********************************************************************/ 00668 /* Analysis */ 00669 00670 /*------------------------------------------------------------------- 00671 * 00672 * analyze 00673 * and learn 00674 */ 00675 00676 static int 00677 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp) 00678 { 00679 Pool *pool = solv->pool; 00680 Queue r; 00681 int rlevel = 1; 00682 Map seen; /* global? */ 00683 Id d, v, vv, *dp, why; 00684 int l, i, idx; 00685 int num = 0, l1num = 0; 00686 int learnt_why = solv->learnt_pool.count; 00687 Id *decisionmap = solv->decisionmap; 00688 00689 queue_init(&r); 00690 00691 POOL_DEBUG(SAT_DEBUG_ANALYZE, "ANALYZE at %d ----------------------\n", level); 00692 map_init(&seen, pool->nsolvables); 00693 idx = solv->decisionq.count; 00694 for (;;) 00695 { 00696 IF_POOLDEBUG (SAT_DEBUG_ANALYZE) 00697 solver_printruleclass(solv, SAT_DEBUG_ANALYZE, c); 00698 queue_push(&solv->learnt_pool, c - solv->rules); 00699 d = c->d < 0 ? -c->d - 1 : c->d; 00700 dp = d ? pool->whatprovidesdata + d : 0; 00701 /* go through all literals of the rule */ 00702 for (i = -1; ; i++) 00703 { 00704 if (i == -1) 00705 v = c->p; 00706 else if (d == 0) 00707 v = i ? 0 : c->w2; 00708 else 00709 v = *dp++; 00710 if (v == 0) 00711 break; 00712 00713 if (DECISIONMAP_TRUE(v)) /* the one true literal */ 00714 continue; 00715 vv = v > 0 ? v : -v; 00716 if (MAPTST(&seen, vv)) 00717 continue; 00718 l = solv->decisionmap[vv]; 00719 if (l < 0) 00720 l = -l; 00721 MAPSET(&seen, vv); 00722 if (l == 1) 00723 l1num++; /* need to do this one in level1 pass */ 00724 else if (l == level) 00725 num++; /* need to do this one as well */ 00726 else 00727 { 00728 queue_push(&r, v); /* not level1 or conflict level, add to new rule */ 00729 if (l > rlevel) 00730 rlevel = l; 00731 } 00732 } 00733 l1retry: 00734 if (!num && !--l1num) 00735 break; /* all level 1 literals done */ 00736 for (;;) 00737 { 00738 assert(idx > 0); 00739 v = solv->decisionq.elements[--idx]; 00740 vv = v > 0 ? v : -v; 00741 if (MAPTST(&seen, vv)) 00742 break; 00743 } 00744 MAPCLR(&seen, vv); 00745 if (num && --num == 0) 00746 { 00747 *pr = -v; /* so that v doesn't get lost */ 00748 if (!l1num) 00749 break; 00750 POOL_DEBUG(SAT_DEBUG_ANALYZE, "got %d involved level 1 decisions\n", l1num); 00751 for (i = 0; i < r.count; i++) 00752 { 00753 v = r.elements[i]; 00754 MAPCLR(&seen, v > 0 ? v : -v); 00755 } 00756 /* only level 1 marks left */ 00757 l1num++; 00758 goto l1retry; 00759 } 00760 why = solv->decisionq_why.elements[idx]; 00761 if (why <= 0) /* just in case, maybe for SYSTEMSOLVABLE */ 00762 goto l1retry; 00763 c = solv->rules + why; 00764 } 00765 map_free(&seen); 00766 00767 if (r.count == 0) 00768 *dr = 0; 00769 else if (r.count == 1 && r.elements[0] < 0) 00770 *dr = r.elements[0]; 00771 else 00772 *dr = pool_queuetowhatprovides(pool, &r); 00773 IF_POOLDEBUG (SAT_DEBUG_ANALYZE) 00774 { 00775 POOL_DEBUG(SAT_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level); 00776 solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, *pr); 00777 for (i = 0; i < r.count; i++) 00778 solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, r.elements[i]); 00779 } 00780 /* push end marker on learnt reasons stack */ 00781 queue_push(&solv->learnt_pool, 0); 00782 if (whyp) 00783 *whyp = learnt_why; 00784 solv->stats_learned++; 00785 return rlevel; 00786 } 00787 00788 00789 /*------------------------------------------------------------------- 00790 * 00791 * solver_reset 00792 * 00793 * reset the solver decisions to right after the rpm rules. 00794 * called after rules have been enabled/disabled 00795 */ 00796 00797 void 00798 solver_reset(Solver *solv) 00799 { 00800 Pool *pool = solv->pool; 00801 int i; 00802 Id v; 00803 00804 /* rewind all decisions */ 00805 for (i = solv->decisionq.count - 1; i >= 0; i--) 00806 { 00807 v = solv->decisionq.elements[i]; 00808 solv->decisionmap[v > 0 ? v : -v] = 0; 00809 } 00810 solv->decisionq_why.count = 0; 00811 solv->decisionq.count = 0; 00812 solv->recommends_index = -1; 00813 solv->propagate_index = 0; 00814 solv->recommendations.count = 0; 00815 solv->branches.count = 0; 00816 00817 /* adapt learnt rule status to new set of enabled/disabled rules */ 00818 enabledisablelearntrules(solv); 00819 00820 /* redo all job/update decisions */ 00821 makeruledecisions(solv); 00822 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count); 00823 } 00824 00825 00826 /*------------------------------------------------------------------- 00827 * 00828 * analyze_unsolvable_rule 00829 */ 00830 00831 static void 00832 analyze_unsolvable_rule(Solver *solv, Rule *r, Id *lastweakp, Map *rseen) 00833 { 00834 Pool *pool = solv->pool; 00835 int i; 00836 Id why = r - solv->rules; 00837 00838 IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE) 00839 solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r); 00840 if (solv->learntrules && why >= solv->learntrules) 00841 { 00842 if (MAPTST(rseen, why - solv->learntrules)) 00843 return; 00844 MAPSET(rseen, why - solv->learntrules); 00845 for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++) 00846 if (solv->learnt_pool.elements[i] > 0) 00847 analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], lastweakp, rseen); 00848 return; 00849 } 00850 if (MAPTST(&solv->weakrulemap, why)) 00851 if (!*lastweakp || why > *lastweakp) 00852 *lastweakp = why; 00853 /* do not add rpm rules to problem */ 00854 if (why < solv->rpmrules_end) 00855 return; 00856 /* turn rule into problem */ 00857 if (why >= solv->jobrules && why < solv->jobrules_end) 00858 why = -(solv->ruletojob.elements[why - solv->jobrules] + 1); 00859 /* normalize dup/infarch rules */ 00860 if (why > solv->infarchrules && why < solv->infarchrules_end) 00861 { 00862 Id name = pool->solvables[-solv->rules[why].p].name; 00863 while (why > solv->infarchrules && pool->solvables[-solv->rules[why - 1].p].name == name) 00864 why--; 00865 } 00866 if (why > solv->duprules && why < solv->duprules_end) 00867 { 00868 Id name = pool->solvables[-solv->rules[why].p].name; 00869 while (why > solv->duprules && pool->solvables[-solv->rules[why - 1].p].name == name) 00870 why--; 00871 } 00872 00873 /* return if problem already countains our rule */ 00874 if (solv->problems.count) 00875 { 00876 for (i = solv->problems.count - 1; i >= 0; i--) 00877 if (solv->problems.elements[i] == 0) /* end of last problem reached? */ 00878 break; 00879 else if (solv->problems.elements[i] == why) 00880 return; 00881 } 00882 queue_push(&solv->problems, why); 00883 } 00884 00885 00886 /*------------------------------------------------------------------- 00887 * 00888 * analyze_unsolvable 00889 * 00890 * return: 1 - disabled some rules, try again 00891 * 0 - hopeless 00892 */ 00893 00894 static int 00895 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules) 00896 { 00897 Pool *pool = solv->pool; 00898 Rule *r; 00899 Map seen; /* global to speed things up? */ 00900 Id d, v, vv, *dp, why; 00901 int l, i, idx; 00902 Id *decisionmap = solv->decisionmap; 00903 int oldproblemcount; 00904 int oldlearntpoolcount; 00905 Id lastweak; 00906 Map rseen; 00907 00908 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n"); 00909 solv->stats_unsolvable++; 00910 oldproblemcount = solv->problems.count; 00911 oldlearntpoolcount = solv->learnt_pool.count; 00912 00913 /* make room for proof index */ 00914 /* must update it later, as analyze_unsolvable_rule would confuse 00915 * it with a rule index if we put the real value in already */ 00916 queue_push(&solv->problems, 0); 00917 00918 r = cr; 00919 map_init(&seen, pool->nsolvables); 00920 map_init(&rseen, solv->learntrules ? solv->nrules - solv->learntrules : 0); 00921 queue_push(&solv->learnt_pool, r - solv->rules); 00922 lastweak = 0; 00923 analyze_unsolvable_rule(solv, r, &lastweak, &rseen); 00924 d = r->d < 0 ? -r->d - 1 : r->d; 00925 dp = d ? pool->whatprovidesdata + d : 0; 00926 for (i = -1; ; i++) 00927 { 00928 if (i == -1) 00929 v = r->p; 00930 else if (d == 0) 00931 v = i ? 0 : r->w2; 00932 else 00933 v = *dp++; 00934 if (v == 0) 00935 break; 00936 if (DECISIONMAP_TRUE(v)) /* the one true literal */ 00937 continue; 00938 vv = v > 0 ? v : -v; 00939 l = solv->decisionmap[vv]; 00940 if (l < 0) 00941 l = -l; 00942 MAPSET(&seen, vv); 00943 } 00944 idx = solv->decisionq.count; 00945 while (idx > 0) 00946 { 00947 v = solv->decisionq.elements[--idx]; 00948 vv = v > 0 ? v : -v; 00949 if (!MAPTST(&seen, vv)) 00950 continue; 00951 why = solv->decisionq_why.elements[idx]; 00952 assert(why > 0); 00953 queue_push(&solv->learnt_pool, why); 00954 r = solv->rules + why; 00955 analyze_unsolvable_rule(solv, r, &lastweak, &rseen); 00956 d = r->d < 0 ? -r->d - 1 : r->d; 00957 dp = d ? pool->whatprovidesdata + d : 0; 00958 for (i = -1; ; i++) 00959 { 00960 if (i == -1) 00961 v = r->p; 00962 else if (d == 0) 00963 v = i ? 0 : r->w2; 00964 else 00965 v = *dp++; 00966 if (v == 0) 00967 break; 00968 if (DECISIONMAP_TRUE(v)) /* the one true literal */ 00969 continue; 00970 vv = v > 0 ? v : -v; 00971 l = solv->decisionmap[vv]; 00972 if (l < 0) 00973 l = -l; 00974 MAPSET(&seen, vv); 00975 } 00976 } 00977 map_free(&seen); 00978 map_free(&rseen); 00979 queue_push(&solv->problems, 0); /* mark end of this problem */ 00980 00981 if (lastweak) 00982 { 00983 Id v; 00984 /* disable last weak rule */ 00985 solv->problems.count = oldproblemcount; 00986 solv->learnt_pool.count = oldlearntpoolcount; 00987 if (lastweak >= solv->jobrules && lastweak < solv->jobrules_end) 00988 v = -(solv->ruletojob.elements[lastweak - solv->jobrules] + 1); 00989 else 00990 v = lastweak; 00991 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling "); 00992 solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, solv->rules + lastweak); 00993 if (lastweak >= solv->choicerules && lastweak < solv->choicerules_end) 00994 solver_disablechoicerules(solv, solv->rules + lastweak); 00995 solver_disableproblem(solv, v); 00996 if (v < 0) 00997 solver_reenablepolicyrules(solv, -(v + 1)); 00998 solver_reset(solv); 00999 return 1; 01000 } 01001 01002 /* finish proof */ 01003 queue_push(&solv->learnt_pool, 0); 01004 solv->problems.elements[oldproblemcount] = oldlearntpoolcount; 01005 01006 if (disablerules) 01007 { 01008 for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++) 01009 solver_disableproblem(solv, solv->problems.elements[i]); 01010 /* XXX: might want to enable all weak rules again */ 01011 solver_reset(solv); 01012 return 1; 01013 } 01014 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "UNSOLVABLE\n"); 01015 return 0; 01016 } 01017 01018 01019 /********************************************************************/ 01020 /* Decision revert */ 01021 01022 /*------------------------------------------------------------------- 01023 * 01024 * revert 01025 * revert decision at level 01026 */ 01027 01028 static void 01029 revert(Solver *solv, int level) 01030 { 01031 Pool *pool = solv->pool; 01032 Id v, vv; 01033 while (solv->decisionq.count) 01034 { 01035 v = solv->decisionq.elements[solv->decisionq.count - 1]; 01036 vv = v > 0 ? v : -v; 01037 if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level) 01038 break; 01039 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]); 01040 if (v > 0 && solv->recommendations.count && v == solv->recommendations.elements[solv->recommendations.count - 1]) 01041 solv->recommendations.count--; 01042 solv->decisionmap[vv] = 0; 01043 solv->decisionq.count--; 01044 solv->decisionq_why.count--; 01045 solv->propagate_index = solv->decisionq.count; 01046 } 01047 while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level) 01048 { 01049 solv->branches.count--; 01050 while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0) 01051 solv->branches.count--; 01052 } 01053 solv->recommends_index = -1; 01054 } 01055 01056 01057 /*------------------------------------------------------------------- 01058 * 01059 * watch2onhighest - put watch2 on literal with highest level 01060 */ 01061 01062 static inline void 01063 watch2onhighest(Solver *solv, Rule *r) 01064 { 01065 int l, wl = 0; 01066 Id d, v, *dp; 01067 01068 d = r->d < 0 ? -r->d - 1 : r->d; 01069 if (!d) 01070 return; /* binary rule, both watches are set */ 01071 dp = solv->pool->whatprovidesdata + d; 01072 while ((v = *dp++) != 0) 01073 { 01074 l = solv->decisionmap[v < 0 ? -v : v]; 01075 if (l < 0) 01076 l = -l; 01077 if (l > wl) 01078 { 01079 r->w2 = dp[-1]; 01080 wl = l; 01081 } 01082 } 01083 } 01084 01085 01086 /*------------------------------------------------------------------- 01087 * 01088 * setpropagatelearn 01089 * 01090 * add free decision (solvable to install) to decisionq 01091 * increase level and propagate decision 01092 * return if no conflict. 01093 * 01094 * in conflict case, analyze conflict rule, add resulting 01095 * rule to learnt rule set, make decision from learnt 01096 * rule (always unit) and re-propagate. 01097 * 01098 * returns the new solver level or 0 if unsolvable 01099 * 01100 */ 01101 01102 static int 01103 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules, Id ruleid) 01104 { 01105 Pool *pool = solv->pool; 01106 Rule *r; 01107 Id p = 0, d = 0; 01108 int l, why; 01109 01110 assert(ruleid >= 0); 01111 if (decision) 01112 { 01113 level++; 01114 if (decision > 0) 01115 solv->decisionmap[decision] = level; 01116 else 01117 solv->decisionmap[-decision] = -level; 01118 queue_push(&solv->decisionq, decision); 01119 queue_push(&solv->decisionq_why, -ruleid); /* <= 0 -> free decision */ 01120 } 01121 for (;;) 01122 { 01123 r = propagate(solv, level); 01124 if (!r) 01125 break; 01126 if (level == 1) 01127 return analyze_unsolvable(solv, r, disablerules); 01128 POOL_DEBUG(SAT_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules)); 01129 l = analyze(solv, level, r, &p, &d, &why); /* learnt rule in p and d */ 01130 assert(l > 0 && l < level); 01131 POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l); 01132 level = l; 01133 revert(solv, level); 01134 r = solver_addrule(solv, p, d); 01135 assert(r); 01136 assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules); 01137 queue_push(&solv->learnt_why, why); 01138 if (d) 01139 { 01140 /* at least 2 literals, needs watches */ 01141 watch2onhighest(solv, r); 01142 addwatches_rule(solv, r); 01143 } 01144 else 01145 { 01146 /* learnt rule is an assertion */ 01147 queue_push(&solv->ruleassertions, r - solv->rules); 01148 } 01149 /* the new rule is unit by design */ 01150 solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level; 01151 queue_push(&solv->decisionq, p); 01152 queue_push(&solv->decisionq_why, r - solv->rules); 01153 IF_POOLDEBUG (SAT_DEBUG_ANALYZE) 01154 { 01155 POOL_DEBUG(SAT_DEBUG_ANALYZE, "decision: "); 01156 solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, p); 01157 POOL_DEBUG(SAT_DEBUG_ANALYZE, "new rule: "); 01158 solver_printrule(solv, SAT_DEBUG_ANALYZE, r); 01159 } 01160 } 01161 return level; 01162 } 01163 01164 01165 /*------------------------------------------------------------------- 01166 * 01167 * select and install 01168 * 01169 * install best package from the queue. We add an extra package, inst, if 01170 * provided. See comment in weak install section. 01171 * 01172 * returns the new solver level or 0 if unsolvable 01173 * 01174 */ 01175 01176 static int 01177 selectandinstall(Solver *solv, int level, Queue *dq, int disablerules, Id ruleid) 01178 { 01179 Pool *pool = solv->pool; 01180 Id p; 01181 int i; 01182 01183 if (dq->count > 1) 01184 policy_filter_unwanted(solv, dq, POLICY_MODE_CHOOSE); 01185 if (dq->count > 1) 01186 { 01187 /* XXX: didn't we already do that? */ 01188 /* XXX: shouldn't we prefer installed packages? */ 01189 /* XXX: move to policy.c? */ 01190 /* choose the supplemented one */ 01191 for (i = 0; i < dq->count; i++) 01192 if (solver_is_supplementing(solv, pool->solvables + dq->elements[i])) 01193 { 01194 dq->elements[0] = dq->elements[i]; 01195 dq->count = 1; 01196 break; 01197 } 01198 } 01199 if (dq->count > 1) 01200 { 01201 /* multiple candidates, open a branch */ 01202 for (i = 1; i < dq->count; i++) 01203 queue_push(&solv->branches, dq->elements[i]); 01204 queue_push(&solv->branches, -level); 01205 } 01206 p = dq->elements[0]; 01207 01208 POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvid2str(pool, p)); 01209 01210 return setpropagatelearn(solv, level, p, disablerules, ruleid); 01211 } 01212 01213 01214 /********************************************************************/ 01215 /* Main solver interface */ 01216 01217 01218 /*------------------------------------------------------------------- 01219 * 01220 * solver_create 01221 * create solver structure 01222 * 01223 * pool: all available solvables 01224 * installed: installed Solvables 01225 * 01226 * 01227 * Upon solving, rules are created to flag the Solvables 01228 * of the 'installed' Repo as installed. 01229 */ 01230 01231 Solver * 01232 solver_create(Pool *pool) 01233 { 01234 Solver *solv; 01235 solv = (Solver *)sat_calloc(1, sizeof(Solver)); 01236 solv->pool = pool; 01237 solv->installed = pool->installed; 01238 01239 transaction_init(&solv->trans, pool); 01240 queue_init(&solv->ruletojob); 01241 queue_init(&solv->decisionq); 01242 queue_init(&solv->decisionq_why); 01243 queue_init(&solv->problems); 01244 queue_init(&solv->suggestions); 01245 queue_init(&solv->recommendations); 01246 queue_init(&solv->orphaned); 01247 queue_init(&solv->learnt_why); 01248 queue_init(&solv->learnt_pool); 01249 queue_init(&solv->branches); 01250 queue_init(&solv->covenantq); 01251 queue_init(&solv->weakruleq); 01252 queue_init(&solv->ruleassertions); 01253 01254 map_init(&solv->recommendsmap, pool->nsolvables); 01255 map_init(&solv->suggestsmap, pool->nsolvables); 01256 map_init(&solv->noupdate, solv->installed ? solv->installed->end - solv->installed->start : 0); 01257 solv->recommends_index = 0; 01258 01259 solv->decisionmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id)); 01260 solv->nrules = 1; 01261 solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK); 01262 memset(solv->rules, 0, sizeof(Rule)); 01263 01264 return solv; 01265 } 01266 01267 01268 /*------------------------------------------------------------------- 01269 * 01270 * solver_free 01271 */ 01272 01273 void 01274 solver_free(Solver *solv) 01275 { 01276 transaction_free(&solv->trans); 01277 queue_free(&solv->job); 01278 queue_free(&solv->ruletojob); 01279 queue_free(&solv->decisionq); 01280 queue_free(&solv->decisionq_why); 01281 queue_free(&solv->learnt_why); 01282 queue_free(&solv->learnt_pool); 01283 queue_free(&solv->problems); 01284 queue_free(&solv->solutions); 01285 queue_free(&solv->suggestions); 01286 queue_free(&solv->recommendations); 01287 queue_free(&solv->orphaned); 01288 queue_free(&solv->branches); 01289 queue_free(&solv->covenantq); 01290 queue_free(&solv->weakruleq); 01291 queue_free(&solv->ruleassertions); 01292 01293 map_free(&solv->recommendsmap); 01294 map_free(&solv->suggestsmap); 01295 map_free(&solv->noupdate); 01296 map_free(&solv->weakrulemap); 01297 map_free(&solv->noobsoletes); 01298 01299 map_free(&solv->updatemap); 01300 map_free(&solv->fixmap); 01301 map_free(&solv->dupmap); 01302 map_free(&solv->dupinvolvedmap); 01303 map_free(&solv->droporphanedmap); 01304 map_free(&solv->cleandepsmap); 01305 01306 sat_free(solv->decisionmap); 01307 sat_free(solv->rules); 01308 sat_free(solv->watches); 01309 sat_free(solv->obsoletes); 01310 sat_free(solv->obsoletes_data); 01311 sat_free(solv->multiversionupdaters); 01312 sat_free(solv->choicerules_ref); 01313 sat_free(solv); 01314 } 01315 01316 01317 /*------------------------------------------------------------------- 01318 * 01319 * solver_run_sat 01320 * 01321 * all rules have been set up, now actually run the solver 01322 * 01323 */ 01324 01325 void 01326 solver_run_sat(Solver *solv, int disablerules, int doweak) 01327 { 01328 Queue dq; /* local decisionqueue */ 01329 Queue dqs; /* local decisionqueue for supplements */ 01330 int systemlevel; 01331 int level, olevel; 01332 Rule *r; 01333 int i, j, n; 01334 Solvable *s; 01335 Pool *pool = solv->pool; 01336 Id p, *dp; 01337 int minimizationsteps; 01338 int installedpos = solv->installed ? solv->installed->start : 0; 01339 01340 IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION) 01341 { 01342 POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules); 01343 for (i = 1; i < solv->nrules; i++) 01344 solver_printruleclass(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i); 01345 } 01346 01347 POOL_DEBUG(SAT_DEBUG_SOLVER, "initial decisions: %d\n", solv->decisionq.count); 01348 01349 IF_POOLDEBUG (SAT_DEBUG_SCHUBI) 01350 solver_printdecisions(solv); 01351 01352 /* start SAT algorithm */ 01353 level = 1; 01354 systemlevel = level + 1; 01355 POOL_DEBUG(SAT_DEBUG_SOLVER, "solving...\n"); 01356 01357 queue_init(&dq); 01358 queue_init(&dqs); 01359 01360 /* 01361 * here's the main loop: 01362 * 1) propagate new decisions (only needed once) 01363 * 2) fulfill jobs 01364 * 3) try to keep installed packages 01365 * 4) fulfill all unresolved rules 01366 * 5) install recommended packages 01367 * 6) minimalize solution if we had choices 01368 * if we encounter a problem, we rewind to a safe level and restart 01369 * with step 1 01370 */ 01371 01372 minimizationsteps = 0; 01373 for (;;) 01374 { 01375 /* 01376 * initial propagation of the assertions 01377 */ 01378 if (level == 1) 01379 { 01380 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d; size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count); 01381 if ((r = propagate(solv, level)) != 0) 01382 { 01383 if (analyze_unsolvable(solv, r, disablerules)) 01384 continue; 01385 queue_free(&dq); 01386 queue_free(&dqs); 01387 return; 01388 } 01389 } 01390 01391 /* 01392 * resolve jobs first 01393 */ 01394 if (level < systemlevel) 01395 { 01396 POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving job rules\n"); 01397 for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++) 01398 { 01399 Id l; 01400 if (r->d < 0) /* ignore disabled rules */ 01401 continue; 01402 queue_empty(&dq); 01403 FOR_RULELITERALS(l, dp, r) 01404 { 01405 if (l < 0) 01406 { 01407 if (solv->decisionmap[-l] <= 0) 01408 break; 01409 } 01410 else 01411 { 01412 if (solv->decisionmap[l] > 0) 01413 break; 01414 if (solv->decisionmap[l] == 0) 01415 queue_push(&dq, l); 01416 } 01417 } 01418 if (l || !dq.count) 01419 continue; 01420 /* prune to installed if not updating */ 01421 if (dq.count > 1 && solv->installed && !solv->updatemap_all) 01422 { 01423 int j, k; 01424 for (j = k = 0; j < dq.count; j++) 01425 { 01426 Solvable *s = pool->solvables + dq.elements[j]; 01427 if (s->repo == solv->installed) 01428 { 01429 dq.elements[k++] = dq.elements[j]; 01430 if (solv->updatemap.size && MAPTST(&solv->updatemap, dq.elements[j] - solv->installed->start)) 01431 { 01432 k = 0; /* package wants to be updated, do not prune */ 01433 break; 01434 } 01435 } 01436 } 01437 if (k) 01438 dq.count = k; 01439 } 01440 olevel = level; 01441 level = selectandinstall(solv, level, &dq, disablerules, i); 01442 if (level == 0) 01443 { 01444 queue_free(&dq); 01445 queue_free(&dqs); 01446 return; 01447 } 01448 if (level <= olevel) 01449 break; 01450 } 01451 systemlevel = level + 1; 01452 if (i < solv->jobrules_end) 01453 continue; 01454 } 01455 01456 01457 /* 01458 * installed packages 01459 */ 01460 if (level < systemlevel && solv->installed && solv->installed->nsolvables && !solv->installed->disabled) 01461 { 01462 Repo *installed = solv->installed; 01463 int pass; 01464 01465 POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving installed packages\n"); 01466 /* we use two passes if we need to update packages 01467 * to create a better user experience */ 01468 for (pass = solv->updatemap.size ? 0 : 1; pass < 2; pass++) 01469 { 01470 int passlevel = level; 01471 /* start with installedpos, the position that gave us problems last time */ 01472 for (i = installedpos, n = installed->start; n < installed->end; i++, n++) 01473 { 01474 Rule *rr; 01475 Id d; 01476 01477 if (i == installed->end) 01478 i = installed->start; 01479 s = pool->solvables + i; 01480 if (s->repo != installed) 01481 continue; 01482 01483 if (solv->decisionmap[i] > 0) 01484 continue; 01485 if (!pass && solv->updatemap.size && !MAPTST(&solv->updatemap, i - installed->start)) 01486 continue; /* updates first */ 01487 r = solv->rules + solv->updaterules + (i - installed->start); 01488 rr = r; 01489 if (!rr->p || rr->d < 0) /* disabled -> look at feature rule */ 01490 rr -= solv->installed->end - solv->installed->start; 01491 if (!rr->p) /* identical to update rule? */ 01492 rr = r; 01493 if (!rr->p) 01494 continue; /* orpaned package */ 01495 01496 /* XXX: noupdate check is probably no longer needed, as all jobs should 01497 * already be satisfied */ 01498 /* Actually we currently still need it because of erase jobs */ 01499 /* if noupdate is set we do not look at update candidates */ 01500 queue_empty(&dq); 01501 if (!MAPTST(&solv->noupdate, i - installed->start) && (solv->decisionmap[i] < 0 || solv->updatemap_all || (solv->updatemap.size && MAPTST(&solv->updatemap, i - installed->start)) || rr->p != i)) 01502 { 01503 if (solv->noobsoletes.size && solv->multiversionupdaters 01504 && (d = solv->multiversionupdaters[i - installed->start]) != 0) 01505 { 01506 /* special multiversion handling, make sure best version is chosen */ 01507 queue_push(&dq, i); 01508 while ((p = pool->whatprovidesdata[d++]) != 0) 01509 if (solv->decisionmap[p] >= 0) 01510 queue_push(&dq, p); 01511 policy_filter_unwanted(solv, &dq, POLICY_MODE_CHOOSE); 01512 p = dq.elements[0]; 01513 if (p != i && solv->decisionmap[p] == 0) 01514 { 01515 rr = solv->rules + solv->featurerules + (i - solv->installed->start); 01516 if (!rr->p) /* update rule == feature rule? */ 01517 rr = rr - solv->featurerules + solv->updaterules; 01518 dq.count = 1; 01519 } 01520 else 01521 dq.count = 0; 01522 } 01523 else 01524 { 01525 /* update to best package */ 01526 FOR_RULELITERALS(p, dp, rr) 01527 { 01528 if (solv->decisionmap[p] > 0) 01529 { 01530 dq.count = 0; /* already fulfilled */ 01531 break; 01532 } 01533 if (!solv->decisionmap[p]) 01534 queue_push(&dq, p); 01535 } 01536 } 01537 } 01538 /* install best version */ 01539 if (dq.count) 01540 { 01541 olevel = level; 01542 level = selectandinstall(solv, level, &dq, disablerules, rr - solv->rules); 01543 if (level == 0) 01544 { 01545 queue_free(&dq); 01546 queue_free(&dqs); 01547 return; 01548 } 01549 if (level <= olevel) 01550 { 01551 if (level == 1 || level < passlevel) 01552 break; /* trouble */ 01553 if (level < olevel) 01554 n = installed->start; /* redo all */ 01555 i--; 01556 n--; 01557 continue; 01558 } 01559 } 01560 /* if still undecided keep package */ 01561 if (solv->decisionmap[i] == 0) 01562 { 01563 olevel = level; 01564 if (solv->cleandepsmap.size && MAPTST(&solv->cleandepsmap, i - installed->start)) 01565 { 01566 POOL_DEBUG(SAT_DEBUG_POLICY, "cleandeps erasing %s\n", solvid2str(pool, i)); 01567 level = setpropagatelearn(solv, level, -i, disablerules, 0); 01568 } 01569 else 01570 { 01571 POOL_DEBUG(SAT_DEBUG_POLICY, "keeping %s\n", solvid2str(pool, i)); 01572 level = setpropagatelearn(solv, level, i, disablerules, r - solv->rules); 01573 } 01574 if (level == 0) 01575 { 01576 queue_free(&dq); 01577 queue_free(&dqs); 01578 return; 01579 } 01580 if (level <= olevel) 01581 { 01582 if (level == 1 || level < passlevel) 01583 break; /* trouble */ 01584 if (level < olevel) 01585 n = installed->start; /* redo all */ 01586 i--; 01587 n--; 01588 continue; /* retry with learnt rule */ 01589 } 01590 } 01591 } 01592 if (n < installed->end) 01593 { 01594 installedpos = i; /* retry problem solvable next time */ 01595 break; /* ran into trouble */ 01596 } 01597 installedpos = installed->start; /* reset installedpos */ 01598 } 01599 systemlevel = level + 1; 01600 if (pass < 2) 01601 continue; /* had trouble, retry */ 01602 } 01603 01604 if (level < systemlevel) 01605 systemlevel = level; 01606 01607 /* 01608 * decide 01609 */ 01610 POOL_DEBUG(SAT_DEBUG_POLICY, "deciding unresolved rules\n"); 01611 for (i = 1, n = 1; n < solv->nrules; i++, n++) 01612 { 01613 if (i == solv->nrules) 01614 i = 1; 01615 r = solv->rules + i; 01616 if (r->d < 0) /* ignore disabled rules */ 01617 continue; 01618 queue_empty(&dq); 01619 if (r->d == 0) 01620 { 01621 /* binary or unary rule */ 01622 /* need two positive undecided literals */ 01623 if (r->p < 0 || r->w2 <= 0) 01624 continue; 01625 if (solv->decisionmap[r->p] || solv->decisionmap[r->w2]) 01626 continue; 01627 queue_push(&dq, r->p); 01628 queue_push(&dq, r->w2); 01629 } 01630 else 01631 { 01632 /* make sure that 01633 * all negative literals are installed 01634 * no positive literal is installed 01635 * i.e. the rule is not fulfilled and we 01636 * just need to decide on the positive literals 01637 */ 01638 if (r->p < 0) 01639 { 01640 if (solv->decisionmap[-r->p] <= 0) 01641 continue; 01642 } 01643 else 01644 { 01645 if (solv->decisionmap[r->p] > 0) 01646 continue; 01647 if (solv->decisionmap[r->p] == 0) 01648 queue_push(&dq, r->p); 01649 } 01650 dp = pool->whatprovidesdata + r->d; 01651 while ((p = *dp++) != 0) 01652 { 01653 if (p < 0) 01654 { 01655 if (solv->decisionmap[-p] <= 0) 01656 break; 01657 } 01658 else 01659 { 01660 if (solv->decisionmap[p] > 0) 01661 break; 01662 if (solv->decisionmap[p] == 0) 01663 queue_push(&dq, p); 01664 } 01665 } 01666 if (p) 01667 continue; 01668 } 01669 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE) 01670 { 01671 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled "); 01672 solver_printruleclass(solv, SAT_DEBUG_PROPAGATE, r); 01673 } 01674 /* dq.count < 2 cannot happen as this means that 01675 * the rule is unit */ 01676 assert(dq.count > 1); 01677 01678 olevel = level; 01679 level = selectandinstall(solv, level, &dq, disablerules, r - solv->rules); 01680 if (level == 0) 01681 { 01682 queue_free(&dq); 01683 queue_free(&dqs); 01684 return; 01685 } 01686 if (level < systemlevel || level == 1) 01687 break; /* trouble */ 01688 /* something changed, so look at all rules again */ 01689 n = 0; 01690 } 01691 01692 if (n != solv->nrules) /* ran into trouble, restart */ 01693 continue; 01694 01695 /* at this point we have a consistent system. now do the extras... */ 01696 01697 if (doweak) 01698 { 01699 int qcount; 01700 01701 POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended packages\n"); 01702 queue_empty(&dq); /* recommended packages */ 01703 queue_empty(&dqs); /* supplemented packages */ 01704 for (i = 1; i < pool->nsolvables; i++) 01705 { 01706 if (solv->decisionmap[i] < 0) 01707 continue; 01708 if (solv->decisionmap[i] > 0) 01709 { 01710 /* installed, check for recommends */ 01711 Id *recp, rec, pp, p; 01712 s = pool->solvables + i; 01713 if (solv->ignorealreadyrecommended && s->repo == solv->installed) 01714 continue; 01715 /* XXX need to special case AND ? */ 01716 if (s->recommends) 01717 { 01718 recp = s->repo->idarraydata + s->recommends; 01719 while ((rec = *recp++) != 0) 01720 { 01721 qcount = dq.count; 01722 FOR_PROVIDES(p, pp, rec) 01723 { 01724 if (solv->decisionmap[p] > 0) 01725 { 01726 dq.count = qcount; 01727 break; 01728 } 01729 else if (solv->decisionmap[p] == 0) 01730 { 01731 if (solv->dupmap_all && solv->installed && pool->solvables[p].repo == solv->installed && (solv->droporphanedmap_all || (solv->droporphanedmap.size && MAPTST(&solv->droporphanedmap, p - solv->installed->start)))) 01732 continue; 01733 queue_pushunique(&dq, p); 01734 } 01735 } 01736 } 01737 } 01738 } 01739 else 01740 { 01741 s = pool->solvables + i; 01742 if (!s->supplements) 01743 continue; 01744 if (!pool_installable(pool, s)) 01745 continue; 01746 if (!solver_is_supplementing(solv, s)) 01747 continue; 01748 if (solv->dupmap_all && solv->installed && s->repo == solv->installed && (solv->droporphanedmap_all || (solv->droporphanedmap.size && MAPTST(&solv->droporphanedmap, i - solv->installed->start)))) 01749 continue; 01750 queue_push(&dqs, i); 01751 } 01752 } 01753 01754 /* filter out all packages obsoleted by installed packages */ 01755 /* this is no longer needed if we have reverse obsoletes */ 01756 if ((dqs.count || dq.count) && solv->installed) 01757 { 01758 Map obsmap; 01759 Id obs, *obsp, po, ppo; 01760 01761 map_init(&obsmap, pool->nsolvables); 01762 for (p = solv->installed->start; p < solv->installed->end; p++) 01763 { 01764 s = pool->solvables + p; 01765 if (s->repo != solv->installed || !s->obsoletes) 01766 continue; 01767 if (solv->decisionmap[p] <= 0) 01768 continue; 01769 if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, p)) 01770 continue; 01771 obsp = s->repo->idarraydata + s->obsoletes; 01772 /* foreach obsoletes */ 01773 while ((obs = *obsp++) != 0) 01774 FOR_PROVIDES(po, ppo, obs) 01775 MAPSET(&obsmap, po); 01776 } 01777 for (i = j = 0; i < dqs.count; i++) 01778 if (!MAPTST(&obsmap, dqs.elements[i])) 01779 dqs.elements[j++] = dqs.elements[i]; 01780 dqs.count = j; 01781 for (i = j = 0; i < dq.count; i++) 01782 if (!MAPTST(&obsmap, dq.elements[i])) 01783 dq.elements[j++] = dq.elements[i]; 01784 dq.count = j; 01785 map_free(&obsmap); 01786 } 01787 01788 /* filter out all already supplemented packages if requested */ 01789 if (solv->ignorealreadyrecommended && dqs.count) 01790 { 01791 /* turn off all new packages */ 01792 for (i = 0; i < solv->decisionq.count; i++) 01793 { 01794 p = solv->decisionq.elements[i]; 01795 if (p < 0) 01796 continue; 01797 s = pool->solvables + p; 01798 if (s->repo && s->repo != solv->installed) 01799 solv->decisionmap[p] = -solv->decisionmap[p]; 01800 } 01801 /* filter out old supplements */ 01802 for (i = j = 0; i < dqs.count; i++) 01803 { 01804 p = dqs.elements[i]; 01805 s = pool->solvables + p; 01806 if (!s->supplements) 01807 continue; 01808 if (!solver_is_supplementing(solv, s)) 01809 dqs.elements[j++] = p; 01810 } 01811 dqs.count = j; 01812 /* undo turning off */ 01813 for (i = 0; i < solv->decisionq.count; i++) 01814 { 01815 p = solv->decisionq.elements[i]; 01816 if (p < 0) 01817 continue; 01818 s = pool->solvables + p; 01819 if (s->repo && s->repo != solv->installed) 01820 solv->decisionmap[p] = -solv->decisionmap[p]; 01821 } 01822 } 01823 01824 /* multiversion doesn't mix well with supplements. 01825 * filter supplemented packages where we already decided 01826 * to install a different version (see bnc#501088) */ 01827 if (dqs.count && solv->noobsoletes.size) 01828 { 01829 for (i = j = 0; i < dqs.count; i++) 01830 { 01831 p = dqs.elements[i]; 01832 if (MAPTST(&solv->noobsoletes, p)) 01833 { 01834 Id p2, pp2; 01835 s = pool->solvables + p; 01836 FOR_PROVIDES(p2, pp2, s->name) 01837 if (solv->decisionmap[p2] > 0 && pool->solvables[p2].name == s->name) 01838 break; 01839 if (p2) 01840 continue; /* ignore this package */ 01841 } 01842 dqs.elements[j++] = p; 01843 } 01844 dqs.count = j; 01845 } 01846 01847 /* make dq contain both recommended and supplemented pkgs */ 01848 if (dqs.count) 01849 { 01850 for (i = 0; i < dqs.count; i++) 01851 queue_pushunique(&dq, dqs.elements[i]); 01852 } 01853 01854 if (dq.count) 01855 { 01856 Map dqmap; 01857 int decisioncount = solv->decisionq.count; 01858 01859 if (dq.count == 1) 01860 { 01861 /* simple case, just one package. no need to choose */ 01862 p = dq.elements[0]; 01863 if (dqs.count) 01864 POOL_DEBUG(SAT_DEBUG_POLICY, "installing supplemented %s\n", solvid2str(pool, p)); 01865 else 01866 POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvid2str(pool, p)); 01867 queue_push(&solv->recommendations, p); 01868 level = setpropagatelearn(solv, level, p, 0, 0); 01869 continue; /* back to main loop */ 01870 } 01871 01872 /* filter packages, this gives us the best versions */ 01873 policy_filter_unwanted(solv, &dq, POLICY_MODE_RECOMMEND); 01874 01875 /* create map of result */ 01876 map_init(&dqmap, pool->nsolvables); 01877 for (i = 0; i < dq.count; i++) 01878 MAPSET(&dqmap, dq.elements[i]); 01879 01880 /* install all supplemented packages */ 01881 for (i = 0; i < dqs.count; i++) 01882 { 01883 p = dqs.elements[i]; 01884 if (solv->decisionmap[p] || !MAPTST(&dqmap, p)) 01885 continue; 01886 POOL_DEBUG(SAT_DEBUG_POLICY, "installing supplemented %s\n", solvid2str(pool, p)); 01887 queue_push(&solv->recommendations, p); 01888 olevel = level; 01889 level = setpropagatelearn(solv, level, p, 0, 0); 01890 if (level <= olevel) 01891 break; 01892 } 01893 if (i < dqs.count || solv->decisionq.count < decisioncount) 01894 { 01895 map_free(&dqmap); 01896 continue; 01897 } 01898 01899 /* install all recommended packages */ 01900 /* more work as we want to created branches if multiple 01901 * choices are valid */ 01902 for (i = 0; i < decisioncount; i++) 01903 { 01904 Id rec, *recp, pp; 01905 p = solv->decisionq.elements[i]; 01906 if (p < 0) 01907 continue; 01908 s = pool->solvables + p; 01909 if (!s->repo || (solv->ignorealreadyrecommended && s->repo == solv->installed)) 01910 continue; 01911 if (!s->recommends) 01912 continue; 01913 recp = s->repo->idarraydata + s->recommends; 01914 while ((rec = *recp++) != 0) 01915 { 01916 queue_empty(&dq); 01917 FOR_PROVIDES(p, pp, rec) 01918 { 01919 if (solv->decisionmap[p] > 0) 01920 { 01921 dq.count = 0; 01922 break; 01923 } 01924 else if (solv->decisionmap[p] == 0 && MAPTST(&dqmap, p)) 01925 queue_pushunique(&dq, p); 01926 } 01927 if (!dq.count) 01928 continue; 01929 if (dq.count > 1) 01930 { 01931 /* multiple candidates, open a branch */ 01932 for (i = 1; i < dq.count; i++) 01933 queue_push(&solv->branches, dq.elements[i]); 01934 queue_push(&solv->branches, -level); 01935 } 01936 p = dq.elements[0]; 01937 POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvid2str(pool, p)); 01938 queue_push(&solv->recommendations, p); 01939 olevel = level; 01940 level = setpropagatelearn(solv, level, p, 0, 0); 01941 if (level <= olevel || solv->decisionq.count < decisioncount) 01942 break; /* we had to revert some decisions */ 01943 } 01944 if (rec) 01945 break; /* had a problem above, quit loop */ 01946 } 01947 map_free(&dqmap); 01948 01949 continue; /* back to main loop so that all deps are checked */ 01950 } 01951 } 01952 01953 if (solv->dupmap_all && solv->installed) 01954 { 01955 int installedone = 0; 01956 01957 /* let's see if we can install some unsupported package */ 01958 POOL_DEBUG(SAT_DEBUG_SOLVER, "deciding orphaned packages\n"); 01959 for (i = 0; i < solv->orphaned.count; i++) 01960 { 01961 p = solv->orphaned.elements[i]; 01962 if (solv->decisionmap[p]) 01963 continue; /* already decided */ 01964 olevel = level; 01965 if (solv->droporphanedmap_all) 01966 continue; 01967 if (solv->droporphanedmap.size && MAPTST(&solv->droporphanedmap, p - solv->installed->start)) 01968 continue; 01969 POOL_DEBUG(SAT_DEBUG_SOLVER, "keeping orphaned %s\n", solvid2str(pool, p)); 01970 level = setpropagatelearn(solv, level, p, 0, 0); 01971 installedone = 1; 01972 if (level < olevel) 01973 break; 01974 } 01975 if (installedone || i < solv->orphaned.count) 01976 continue; /* back to main loop */ 01977 for (i = 0; i < solv->orphaned.count; i++) 01978 { 01979 p = solv->orphaned.elements[i]; 01980 if (solv->decisionmap[p]) 01981 continue; /* already decided */ 01982 POOL_DEBUG(SAT_DEBUG_SOLVER, "removing orphaned %s\n", solvid2str(pool, p)); 01983 olevel = level; 01984 level = setpropagatelearn(solv, level, -p, 0, 0); 01985 if (level < olevel) 01986 break; 01987 } 01988 if (i < solv->orphaned.count) 01989 continue; /* back to main loop */ 01990 } 01991 01992 if (solv->solution_callback) 01993 { 01994 solv->solution_callback(solv, solv->solution_callback_data); 01995 if (solv->branches.count) 01996 { 01997 int i = solv->branches.count - 1; 01998 int l = -solv->branches.elements[i]; 01999 Id why; 02000 02001 for (; i > 0; i--) 02002 if (solv->branches.elements[i - 1] < 0) 02003 break; 02004 p = solv->branches.elements[i]; 02005 POOL_DEBUG(SAT_DEBUG_SOLVER, "branching with %s\n", solvid2str(pool, p)); 02006 queue_empty(&dq); 02007 for (j = i + 1; j < solv->branches.count; j++) 02008 queue_push(&dq, solv->branches.elements[j]); 02009 solv->branches.count = i; 02010 level = l; 02011 revert(solv, level); 02012 if (dq.count > 1) 02013 for (j = 0; j < dq.count; j++) 02014 queue_push(&solv->branches, dq.elements[j]); 02015 olevel = level; 02016 why = -solv->decisionq_why.elements[solv->decisionq_why.count]; 02017 assert(why >= 0); 02018 level = setpropagatelearn(solv, level, p, disablerules, why); 02019 if (level == 0) 02020 { 02021 queue_free(&dq); 02022 queue_free(&dqs); 02023 return; 02024 } 02025 continue; 02026 } 02027 /* all branches done, we're finally finished */ 02028 break; 02029 } 02030 02031 /* minimization step */ 02032 if (solv->branches.count) 02033 { 02034 int l = 0, lasti = -1, lastl = -1; 02035 Id why; 02036 02037 p = 0; 02038 for (i = solv->branches.count - 1; i >= 0; i--) 02039 { 02040 p = solv->branches.elements[i]; 02041 if (p < 0) 02042 l = -p; 02043 else if (p > 0 && solv->decisionmap[p] > l + 1) 02044 { 02045 lasti = i; 02046 lastl = l; 02047 } 02048 } 02049 if (lasti >= 0) 02050 { 02051 /* kill old solvable so that we do not loop */ 02052 p = solv->branches.elements[lasti]; 02053 solv->branches.elements[lasti] = 0; 02054 POOL_DEBUG(SAT_DEBUG_SOLVER, "minimizing %d -> %d with %s\n", solv->decisionmap[p], lastl, solvid2str(pool, p)); 02055 minimizationsteps++; 02056 02057 level = lastl; 02058 revert(solv, level); 02059 why = -solv->decisionq_why.elements[solv->decisionq_why.count]; 02060 assert(why >= 0); 02061 olevel = level; 02062 level = setpropagatelearn(solv, level, p, disablerules, why); 02063 if (level == 0) 02064 { 02065 queue_free(&dq); 02066 queue_free(&dqs); 02067 return; 02068 } 02069 continue; /* back to main loop */ 02070 } 02071 } 02072 /* no minimization found, we're finally finished! */ 02073 break; 02074 } 02075 02076 POOL_DEBUG(SAT_DEBUG_STATS, "solver statistics: %d learned rules, %d unsolvable, %d minimization steps\n", solv->stats_learned, solv->stats_unsolvable, minimizationsteps); 02077 02078 POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n"); 02079 queue_free(&dq); 02080 queue_free(&dqs); 02081 #if 0 02082 solver_printdecisionq(solv, SAT_DEBUG_RESULT); 02083 #endif 02084 } 02085 02086 02087 /*------------------------------------------------------------------- 02088 * 02089 * remove disabled conflicts 02090 * 02091 * purpose: update the decisionmap after some rules were disabled. 02092 * this is used to calculate the suggested/recommended package list. 02093 * Also returns a "removed" list to undo the discisionmap changes. 02094 */ 02095 02096 static void 02097 removedisabledconflicts(Solver *solv, Queue *removed) 02098 { 02099 Pool *pool = solv->pool; 02100 int i, n; 02101 Id p, why, *dp; 02102 Id new; 02103 Rule *r; 02104 Id *decisionmap = solv->decisionmap; 02105 02106 POOL_DEBUG(SAT_DEBUG_SCHUBI, "removedisabledconflicts\n"); 02107 queue_empty(removed); 02108 for (i = 0; i < solv->decisionq.count; i++) 02109 { 02110 p = solv->decisionq.elements[i]; 02111 if (p > 0) 02112 continue; /* conflicts only, please */ 02113 why = solv->decisionq_why.elements[i]; 02114 if (why == 0) 02115 { 02116 /* no rule involved, must be a orphan package drop */ 02117 continue; 02118 } 02119 /* we never do conflicts on free decisions, so there 02120 * must have been an unit rule */ 02121 assert(why > 0); 02122 r = solv->rules + why; 02123 if (r->d < 0 && decisionmap[-p]) 02124 { 02125 /* rule is now disabled, remove from decisionmap */ 02126 POOL_DEBUG(SAT_DEBUG_SCHUBI, "removing conflict for package %s[%d]\n", solvid2str(pool, -p), -p); 02127 queue_push(removed, -p); 02128 queue_push(removed, decisionmap[-p]); 02129 decisionmap[-p] = 0; 02130 } 02131 } 02132 if (!removed->count) 02133 return; 02134 /* we removed some confliced packages. some of them might still 02135 * be in conflict, so search for unit rules and re-conflict */ 02136 new = 0; 02137 for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++) 02138 { 02139 if (i == solv->nrules) 02140 { 02141 i = 1; 02142 r = solv->rules + i; 02143 } 02144 if (r->d < 0) 02145 continue; 02146 if (!r->w2) 02147 { 02148 if (r->p < 0 && !decisionmap[-r->p]) 02149 new = r->p; 02150 } 02151 else if (!r->d) 02152 { 02153 /* binary rule */ 02154 if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2)) 02155 new = r->p; 02156 else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p)) 02157 new = r->w2; 02158 } 02159 else 02160 { 02161 if (r->p < 0 && decisionmap[-r->p] == 0) 02162 new = r->p; 02163 if (new || DECISIONMAP_FALSE(r->p)) 02164 { 02165 dp = pool->whatprovidesdata + r->d; 02166 while ((p = *dp++) != 0) 02167 { 02168 if (new && p == new) 02169 continue; 02170 if (p < 0 && decisionmap[-p] == 0) 02171 { 02172 if (new) 02173 { 02174 new = 0; 02175 break; 02176 } 02177 new = p; 02178 } 02179 else if (!DECISIONMAP_FALSE(p)) 02180 { 02181 new = 0; 02182 break; 02183 } 02184 } 02185 } 02186 } 02187 if (new) 02188 { 02189 POOL_DEBUG(SAT_DEBUG_SCHUBI, "re-conflicting package %s[%d]\n", solvid2str(pool, -new), -new); 02190 decisionmap[-new] = -1; 02191 new = 0; 02192 n = 0; /* redo all rules */ 02193 } 02194 } 02195 } 02196 02197 static inline void 02198 undo_removedisabledconflicts(Solver *solv, Queue *removed) 02199 { 02200 int i; 02201 for (i = 0; i < removed->count; i += 2) 02202 solv->decisionmap[removed->elements[i]] = removed->elements[i + 1]; 02203 } 02204 02205 02206 /*------------------------------------------------------------------- 02207 * 02208 * weaken solvable dependencies 02209 */ 02210 02211 static void 02212 weaken_solvable_deps(Solver *solv, Id p) 02213 { 02214 int i; 02215 Rule *r; 02216 02217 for (i = 1, r = solv->rules + i; i < solv->rpmrules_end; i++, r++) 02218 { 02219 if (r->p != -p) 02220 continue; 02221 if ((r->d == 0 || r->d == -1) && r->w2 < 0) 02222 continue; /* conflict */ 02223 queue_push(&solv->weakruleq, i); 02224 } 02225 } 02226 02227 02228 /********************************************************************/ 02229 /* main() */ 02230 02231 02232 static void 02233 findrecommendedsuggested(Solver *solv) 02234 { 02235 Pool *pool = solv->pool; 02236 Queue redoq, disabledq; 02237 int goterase, i; 02238 Solvable *s; 02239 Rule *r; 02240 Map obsmap; 02241 02242 map_init(&obsmap, pool->nsolvables); 02243 if (solv->installed) 02244 { 02245 Id obs, *obsp, p, po, ppo; 02246 for (p = solv->installed->start; p < solv->installed->end; p++) 02247 { 02248 s = pool->solvables + p; 02249 if (s->repo != solv->installed || !s->obsoletes) 02250 continue; 02251 if (solv->decisionmap[p] <= 0) 02252 continue; 02253 if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, p)) 02254 continue; 02255 obsp = s->repo->idarraydata + s->obsoletes; 02256 /* foreach obsoletes */ 02257 while ((obs = *obsp++) != 0) 02258 FOR_PROVIDES(po, ppo, obs) 02259 MAPSET(&obsmap, po); 02260 } 02261 } 02262 02263 queue_init(&redoq); 02264 queue_init(&disabledq); 02265 goterase = 0; 02266 /* disable all erase jobs (including weak "keep uninstalled" rules) */ 02267 for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++) 02268 { 02269 if (r->d < 0) /* disabled ? */ 02270 continue; 02271 if (r->p >= 0) /* install job? */ 02272 continue; 02273 queue_push(&disabledq, i); 02274 solver_disablerule(solv, r); 02275 goterase++; 02276 } 02277 02278 if (goterase) 02279 { 02280 enabledisablelearntrules(solv); 02281 removedisabledconflicts(solv, &redoq); 02282 } 02283 02284 /* 02285 * find recommended packages 02286 */ 02287 02288 /* if redoq.count == 0 we already found all recommended in the 02289 * solver run */ 02290 if (redoq.count || solv->dontinstallrecommended || !solv->dontshowinstalledrecommended || solv->ignorealreadyrecommended) 02291 { 02292 Id rec, *recp, p, pp; 02293 02294 /* create map of all recommened packages */ 02295 solv->recommends_index = -1; 02296 MAPZERO(&solv->recommendsmap); 02297 for (i = 0; i < solv->decisionq.count; i++) 02298 { 02299 p = solv->decisionq.elements[i]; 02300 if (p < 0) 02301 continue; 02302 s = pool->solvables + p; 02303 if (s->recommends) 02304 { 02305 recp = s->repo->idarraydata + s->recommends; 02306 while ((rec = *recp++) != 0) 02307 { 02308 FOR_PROVIDES(p, pp, rec) 02309 if (solv->decisionmap[p] > 0) 02310 break; 02311 if (p) 02312 { 02313 if (!solv->dontshowinstalledrecommended) 02314 { 02315 FOR_PROVIDES(p, pp, rec) 02316 if (solv->decisionmap[p] > 0) 02317 MAPSET(&solv->recommendsmap, p); 02318 } 02319 continue; /* p != 0: already fulfilled */ 02320 } 02321 FOR_PROVIDES(p, pp, rec) 02322 MAPSET(&solv->recommendsmap, p); 02323 } 02324 } 02325 } 02326 for (i = 1; i < pool->nsolvables; i++) 02327 { 02328 if (solv->decisionmap[i] < 0) 02329 continue; 02330 if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended) 02331 continue; 02332 if (MAPTST(&obsmap, i)) 02333 continue; 02334 s = pool->solvables + i; 02335 if (!MAPTST(&solv->recommendsmap, i)) 02336 { 02337 if (!s->supplements) 02338 continue; 02339 if (!pool_installable(pool, s)) 02340 continue; 02341 if (!solver_is_supplementing(solv, s)) 02342 continue; 02343 } 02344 if (solv->dontinstallrecommended) 02345 queue_push(&solv->recommendations, i); 02346 else 02347 queue_pushunique(&solv->recommendations, i); 02348 } 02349 /* we use MODE_SUGGEST here so that repo prio is ignored */ 02350 policy_filter_unwanted(solv, &solv->recommendations, POLICY_MODE_SUGGEST); 02351 } 02352 02353 /* 02354 * find suggested packages 02355 */ 02356 02357 if (1) 02358 { 02359 Id sug, *sugp, p, pp; 02360 02361 /* create map of all suggests that are still open */ 02362 solv->recommends_index = -1; 02363 MAPZERO(&solv->suggestsmap); 02364 for (i = 0; i < solv->decisionq.count; i++) 02365 { 02366 p = solv->decisionq.elements[i]; 02367 if (p < 0) 02368 continue; 02369 s = pool->solvables + p; 02370 if (s->suggests) 02371 { 02372 sugp = s->repo->idarraydata + s->suggests; 02373 while ((sug = *sugp++) != 0) 02374 { 02375 FOR_PROVIDES(p, pp, sug) 02376 if (solv->decisionmap[p] > 0) 02377 break; 02378 if (p) 02379 { 02380 if (!solv->dontshowinstalledrecommended) 02381 { 02382 FOR_PROVIDES(p, pp, sug) 02383 if (solv->decisionmap[p] > 0) 02384 MAPSET(&solv->suggestsmap, p); 02385 } 02386 continue; /* already fulfilled */ 02387 } 02388 FOR_PROVIDES(p, pp, sug) 02389 MAPSET(&solv->suggestsmap, p); 02390 } 02391 } 02392 } 02393 for (i = 1; i < pool->nsolvables; i++) 02394 { 02395 if (solv->decisionmap[i] < 0) 02396 continue; 02397 if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended) 02398 continue; 02399 if (MAPTST(&obsmap, i)) 02400 continue; 02401 s = pool->solvables + i; 02402 if (!MAPTST(&solv->suggestsmap, i)) 02403 { 02404 if (!s->enhances) 02405 continue; 02406 if (!pool_installable(pool, s)) 02407 continue; 02408 if (!solver_is_enhancing(solv, s)) 02409 continue; 02410 } 02411 queue_push(&solv->suggestions, i); 02412 } 02413 policy_filter_unwanted(solv, &solv->suggestions, POLICY_MODE_SUGGEST); 02414 } 02415 02416 /* undo removedisabledconflicts */ 02417 if (redoq.count) 02418 undo_removedisabledconflicts(solv, &redoq); 02419 queue_free(&redoq); 02420 02421 /* undo job rule disabling */ 02422 for (i = 0; i < disabledq.count; i++) 02423 solver_enablerule(solv, solv->rules + disabledq.elements[i]); 02424 queue_free(&disabledq); 02425 map_free(&obsmap); 02426 } 02427 02428 void 02429 solver_calculate_noobsmap(Pool *pool, Queue *job, Map *noobsmap) 02430 { 02431 int i; 02432 Id how, what, select; 02433 Id p, pp; 02434 for (i = 0; i < job->count; i += 2) 02435 { 02436 how = job->elements[i]; 02437 if ((how & SOLVER_JOBMASK) != SOLVER_NOOBSOLETES) 02438 continue; 02439 what = job->elements[i + 1]; 02440 select = how & SOLVER_SELECTMASK; 02441 if (!noobsmap->size) 02442 map_grow(noobsmap, pool->nsolvables); 02443 FOR_JOB_SELECT(p, pp, select, what) 02444 MAPSET(noobsmap, p); 02445 } 02446 } 02447 02448 /* 02449 * add a rule created by a job, record job number and weak flag 02450 */ 02451 static inline void 02452 solver_addjobrule(Solver *solv, Id p, Id d, Id job, int weak) 02453 { 02454 solver_addrule(solv, p, d); 02455 queue_push(&solv->ruletojob, job); 02456 if (weak) 02457 queue_push(&solv->weakruleq, solv->nrules - 1); 02458 } 02459 02460 /* 02461 * 02462 * solve job queue 02463 * 02464 */ 02465 02466 void 02467 solver_solve(Solver *solv, Queue *job) 02468 { 02469 Pool *pool = solv->pool; 02470 Repo *installed = solv->installed; 02471 int i; 02472 int oldnrules; 02473 Map addedmap; /* '1' == have rpm-rules for solvable */ 02474 Map installcandidatemap; 02475 Id how, what, select, name, weak, p, pp, d; 02476 Queue q; 02477 Solvable *s; 02478 Rule *r; 02479 int now, solve_start; 02480 int hasdupjob = 0; 02481 02482 solve_start = sat_timems(0); 02483 02484 /* log solver options */ 02485 POOL_DEBUG(SAT_DEBUG_STATS, "solver started\n"); 02486 POOL_DEBUG(SAT_DEBUG_STATS, "fixsystem=%d updatesystem=%d dosplitprovides=%d, noupdateprovide=%d noinfarchcheck=%d\n", solv->fixsystem, solv->updatesystem, solv->dosplitprovides, solv->noupdateprovide, solv->noinfarchcheck); 02487 POOL_DEBUG(SAT_DEBUG_STATS, "distupgrade=%d distupgrade_removeunsupported=%d\n", solv->distupgrade, solv->distupgrade_removeunsupported); 02488 POOL_DEBUG(SAT_DEBUG_STATS, "allowuninstall=%d, allowdowngrade=%d, allowarchchange=%d, allowvendorchange=%d\n", solv->allowuninstall, solv->allowdowngrade, solv->allowarchchange, solv->allowvendorchange); 02489 POOL_DEBUG(SAT_DEBUG_STATS, "promoteepoch=%d, novirtualconflicts=%d, allowselfconflicts=%d\n", pool->promoteepoch, pool->novirtualconflicts, pool->allowselfconflicts); 02490 POOL_DEBUG(SAT_DEBUG_STATS, "obsoleteusesprovides=%d, implicitobsoleteusesprovides=%d, obsoleteusescolors=%d\n", pool->obsoleteusesprovides, pool->implicitobsoleteusesprovides, pool->obsoleteusescolors); 02491 POOL_DEBUG(SAT_DEBUG_STATS, "dontinstallrecommended=%d, ignorealreadyrecommended=%d, dontshowinstalledrecommended=%d\n", solv->dontinstallrecommended, solv->ignorealreadyrecommended, solv->dontshowinstalledrecommended); 02492 02493 /* create whatprovides if not already there */ 02494 if (!pool->whatprovides) 02495 pool_createwhatprovides(pool); 02496 02497 /* create obsolete index */ 02498 policy_create_obsolete_index(solv); 02499 02500 /* remember job */ 02501 queue_free(&solv->job); 02502 queue_init_clone(&solv->job, job); 02503 02504 /* initialize with legacy values */ 02505 solv->fixmap_all = solv->fixsystem; 02506 solv->updatemap_all = solv->updatesystem; 02507 solv->droporphanedmap_all = solv->distupgrade_removeunsupported; 02508 solv->dupmap_all = solv->distupgrade; 02509 02510 /* 02511 * create basic rule set of all involved packages 02512 * use addedmap bitmap to make sure we don't create rules twice 02513 */ 02514 02515 /* create noobsolete map if needed */ 02516 solver_calculate_noobsmap(pool, job, &solv->noobsoletes); 02517 02518 map_init(&addedmap, pool->nsolvables); 02519 MAPSET(&addedmap, SYSTEMSOLVABLE); 02520 02521 map_init(&installcandidatemap, pool->nsolvables); 02522 queue_init(&q); 02523 02524 now = sat_timems(0); 02525 /* 02526 * create rules for all package that could be involved with the solving 02527 * so called: rpm rules 02528 * 02529 */ 02530 if (installed) 02531 { 02532 /* check for update/verify jobs as they need to be known early */ 02533 for (i = 0; i < job->count; i += 2) 02534 { 02535 how = job->elements[i]; 02536 what = job->elements[i + 1]; 02537 select = how & SOLVER_SELECTMASK; 02538 switch (how & SOLVER_JOBMASK) 02539 { 02540 case SOLVER_VERIFY: 02541 if (select == SOLVER_SOLVABLE_ALL) 02542 solv->fixmap_all = 1; 02543 FOR_JOB_SELECT(p, pp, select, what) 02544 { 02545 s = pool->solvables + p; 02546 if (!solv->installed || s->repo != solv->installed) 02547 continue; 02548 if (!solv->fixmap.size) 02549 map_grow(&solv->fixmap, solv->installed->end - solv->installed->start); 02550 MAPSET(&solv->fixmap, p - solv->installed->start); 02551 } 02552 break; 02553 case SOLVER_UPDATE: 02554 if (select == SOLVER_SOLVABLE_ALL) 02555 solv->updatemap_all = 1; 02556 FOR_JOB_SELECT(p, pp, select, what) 02557 { 02558 s = pool->solvables + p; 02559 if (!solv->installed || s->repo != solv->installed) 02560 continue; 02561 if (!solv->updatemap.size) 02562 map_grow(&solv->updatemap, solv->installed->end - solv->installed->start); 02563 MAPSET(&solv->updatemap, p - solv->installed->start); 02564 } 02565 break; 02566 default: 02567 break; 02568 } 02569 } 02570 02571 oldnrules = solv->nrules; 02572 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n"); 02573 FOR_REPO_SOLVABLES(installed, p, s) 02574 solver_addrpmrulesforsolvable(solv, s, &addedmap); 02575 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules); 02576 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n"); 02577 oldnrules = solv->nrules; 02578 FOR_REPO_SOLVABLES(installed, p, s) 02579 solver_addrpmrulesforupdaters(solv, s, &addedmap, 1); 02580 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules); 02581 } 02582 02583 /* 02584 * create rules for all packages involved in the job 02585 * (to be installed or removed) 02586 */ 02587 02588 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n"); 02589 oldnrules = solv->nrules; 02590 for (i = 0; i < job->count; i += 2) 02591 { 02592 how = job->elements[i]; 02593 what = job->elements[i + 1]; 02594 select = how & SOLVER_SELECTMASK; 02595 02596 switch (how & SOLVER_JOBMASK) 02597 { 02598 case SOLVER_INSTALL: 02599 FOR_JOB_SELECT(p, pp, select, what) 02600 { 02601 MAPSET(&installcandidatemap, p); 02602 solver_addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap); 02603 } 02604 break; 02605 case SOLVER_DISTUPGRADE: 02606 if (select == SOLVER_SOLVABLE_ALL) 02607 { 02608 solv->dupmap_all = 1; 02609 solv->updatemap_all = 1; 02610 } 02611 if (!solv->dupmap_all) 02612 hasdupjob = 1; 02613 break; 02614 default: 02615 break; 02616 } 02617 } 02618 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules); 02619 02620 02621 /* 02622 * add rules for suggests, enhances 02623 */ 02624 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for suggested/enhanced packages ***\n"); 02625 oldnrules = solv->nrules; 02626 solver_addrpmrulesforweak(solv, &addedmap); 02627 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules); 02628 02629 /* 02630 * first pass done, we now have all the rpm rules we need. 02631 * unify existing rules before going over all job rules and 02632 * policy rules. 02633 * at this point the system is always solvable, 02634 * as an empty system (remove all packages) is a valid solution 02635 */ 02636 02637 IF_POOLDEBUG (SAT_DEBUG_STATS) 02638 { 02639 int possible = 0, installable = 0; 02640 for (i = 1; i < pool->nsolvables; i++) 02641 { 02642 if (pool_installable(pool, pool->solvables + i)) 02643 installable++; 02644 if (MAPTST(&addedmap, i)) 02645 possible++; 02646 } 02647 POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable); 02648 } 02649 02650 solver_unifyrules(solv); /* remove duplicate rpm rules */ 02651 solv->rpmrules_end = solv->nrules; /* mark end of rpm rules */ 02652 02653 POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule memory usage: %d K\n", solv->nrules * (int)sizeof(Rule) / 1024); 02654 POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule creation took %d ms\n", sat_timems(now)); 02655 02656 /* create dup maps if needed. We need the maps early to create our 02657 * update rules */ 02658 if (hasdupjob) 02659 solver_createdupmaps(solv); 02660 02661 /* 02662 * create feature rules 02663 * 02664 * foreach installed: 02665 * create assertion (keep installed, if no update available) 02666 * or 02667 * create update rule (A|update1(A)|update2(A)|...) 02668 * 02669 * those are used later on to keep a version of the installed packages in 02670 * best effort mode 02671 */ 02672 02673 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add feature rules ***\n"); 02674 solv->featurerules = solv->nrules; /* mark start of feature rules */ 02675 if (installed) 02676 { 02677 /* foreach possibly installed solvable */ 02678 for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++) 02679 { 02680 if (s->repo != installed) 02681 { 02682 solver_addrule(solv, 0, 0); /* create dummy rule */ 02683 continue; 02684 } 02685 solver_addupdaterule(solv, s, 1); /* allow s to be updated */ 02686 } 02687 /* make sure we accounted for all rules */ 02688 assert(solv->nrules - solv->featurerules == installed->end - installed->start); 02689 } 02690 solv->featurerules_end = solv->nrules; 02691 02692 /* 02693 * Add update rules for installed solvables 02694 * 02695 * almost identical to feature rules 02696 * except that downgrades/archchanges/vendorchanges are not allowed 02697 */ 02698 02699 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add update rules ***\n"); 02700 solv->updaterules = solv->nrules; 02701 02702 if (installed) 02703 { /* foreach installed solvables */ 02704 /* we create all update rules, but disable some later on depending on the job */ 02705 for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++) 02706 { 02707 Rule *sr; 02708 02709 if (s->repo != installed) 02710 { 02711 solver_addrule(solv, 0, 0); /* create dummy rule */ 02712 continue; 02713 } 02714 solver_addupdaterule(solv, s, 0); /* allowall = 0: downgrades not allowed */ 02715 /* 02716 * check for and remove duplicate 02717 */ 02718 r = solv->rules + solv->nrules - 1; /* r: update rule */ 02719 sr = r - (installed->end - installed->start); /* sr: feature rule */ 02720 /* it's orphaned if there is no feature rule or the feature rule 02721 * consists just of the installed package */ 02722 if (!sr->p || (sr->p == i && !sr->d && !sr->w2)) 02723 queue_push(&solv->orphaned, i); 02724 if (!r->p) 02725 { 02726 assert(solv->dupmap_all && !sr->p); 02727 continue; 02728 } 02729 if (!solver_samerule(solv, r, sr)) 02730 { 02731 /* identical rule, kill unneeded one */ 02732 if (solv->allowuninstall) 02733 { 02734 /* keep feature rule, make it weak */ 02735 memset(r, 0, sizeof(*r)); 02736 queue_push(&solv->weakruleq, sr - solv->rules); 02737 } 02738 else 02739 { 02740 /* keep update rule */ 02741 memset(sr, 0, sizeof(*sr)); 02742 } 02743 } 02744 else if (solv->allowuninstall) 02745 { 02746 /* make both feature and update rule weak */ 02747 queue_push(&solv->weakruleq, r - solv->rules); 02748 queue_push(&solv->weakruleq, sr - solv->rules); 02749 } 02750 else 02751 solver_disablerule(solv, sr); 02752 } 02753 /* consistency check: we added a rule for _every_ installed solvable */ 02754 assert(solv->nrules - solv->updaterules == installed->end - installed->start); 02755 } 02756 solv->updaterules_end = solv->nrules; 02757 02758 02759 /* 02760 * now add all job rules 02761 */ 02762 02763 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n"); 02764 02765 solv->jobrules = solv->nrules; 02766 for (i = 0; i < job->count; i += 2) 02767 { 02768 oldnrules = solv->nrules; 02769 02770 how = job->elements[i]; 02771 what = job->elements[i + 1]; 02772 weak = how & SOLVER_WEAK; 02773 select = how & SOLVER_SELECTMASK; 02774 switch (how & SOLVER_JOBMASK) 02775 { 02776 case SOLVER_INSTALL: 02777 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall %s\n", weak ? "weak " : "", solver_select2str(pool, select, what)); 02778 if (select == SOLVER_SOLVABLE) 02779 { 02780 p = what; 02781 d = 0; 02782 } 02783 else 02784 { 02785 queue_empty(&q); 02786 FOR_JOB_SELECT(p, pp, select, what) 02787 queue_push(&q, p); 02788 if (!q.count) 02789 { 02790 /* no candidate found, make this an impossible rule */ 02791 queue_push(&q, -SYSTEMSOLVABLE); 02792 } 02793 p = queue_shift(&q); /* get first candidate */ 02794 d = !q.count ? 0 : pool_queuetowhatprovides(pool, &q); /* internalize */ 02795 } 02796 solver_addjobrule(solv, p, d, i, weak); 02797 break; 02798 case SOLVER_ERASE: 02799 POOL_DEBUG(SAT_DEBUG_JOB, "job: %s%serase %s\n", weak ? "weak " : "", how & SOLVER_CLEANDEPS ? "clean deps " : "", solver_select2str(pool, select, what)); 02800 if ((how & SOLVER_CLEANDEPS) != 0 && !solv->cleandepsmap.size && solv->installed) 02801 map_grow(&solv->cleandepsmap, solv->installed->end - solv->installed->start); 02802 if (select == SOLVER_SOLVABLE && solv->installed && pool->solvables[what].repo == solv->installed) 02803 { 02804 /* special case for "erase a specific solvable": we also 02805 * erase all other solvables with that name, so that they 02806 * don't get picked up as replacement */ 02807 /* XXX: look also at packages that obsolete this package? */ 02808 name = pool->solvables[what].name; 02809 FOR_PROVIDES(p, pp, name) 02810 { 02811 if (p == what) 02812 continue; 02813 s = pool->solvables + p; 02814 if (s->name != name) 02815 continue; 02816 /* keep other versions installed */ 02817 if (s->repo == solv->installed) 02818 continue; 02819 /* keep installcandidates of other jobs */ 02820 if (MAPTST(&installcandidatemap, p)) 02821 continue; 02822 solver_addjobrule(solv, -p, 0, i, weak); /* remove by id */ 02823 } 02824 } 02825 FOR_JOB_SELECT(p, pp, select, what) 02826 solver_addjobrule(solv, -p, 0, i, weak); 02827 break; 02828 02829 case SOLVER_UPDATE: 02830 POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solver_select2str(pool, select, what)); 02831 break; 02832 case SOLVER_VERIFY: 02833 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sverify %s\n", weak ? "weak " : "", solver_select2str(pool, select, what)); 02834 break; 02835 case SOLVER_WEAKENDEPS: 02836 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sweaken deps %s\n", weak ? "weak " : "", solver_select2str(pool, select, what)); 02837 if (select != SOLVER_SOLVABLE) 02838 break; 02839 s = pool->solvables + what; 02840 weaken_solvable_deps(solv, what); 02841 break; 02842 case SOLVER_NOOBSOLETES: 02843 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sno obsolete %s\n", weak ? "weak " : "", solver_select2str(pool, select, what)); 02844 break; 02845 case SOLVER_LOCK: 02846 POOL_DEBUG(SAT_DEBUG_JOB, "job: %slock %s\n", weak ? "weak " : "", solver_select2str(pool, select, what)); 02847 FOR_JOB_SELECT(p, pp, select, what) 02848 { 02849 s = pool->solvables + p; 02850 solver_addjobrule(solv, installed && s->repo == installed ? p : -p, 0, i, weak); 02851 } 02852 break; 02853 case SOLVER_DISTUPGRADE: 02854 POOL_DEBUG(SAT_DEBUG_JOB, "job: distupgrade %s\n", solver_select2str(pool, select, what)); 02855 break; 02856 case SOLVER_DROP_ORPHANED: 02857 POOL_DEBUG(SAT_DEBUG_JOB, "job: drop orphaned %s\n", solver_select2str(pool, select, what)); 02858 if (select == SOLVER_SOLVABLE_ALL) 02859 solv->droporphanedmap_all = 1; 02860 FOR_JOB_SELECT(p, pp, select, what) 02861 { 02862 s = pool->solvables + p; 02863 if (!installed || s->repo != installed) 02864 continue; 02865 if (!solv->droporphanedmap.size) 02866 map_grow(&solv->droporphanedmap, installed->end - installed->start); 02867 MAPSET(&solv->droporphanedmap, p - installed->start); 02868 } 02869 break; 02870 case SOLVER_USERINSTALLED: 02871 POOL_DEBUG(SAT_DEBUG_JOB, "job: user installed %s\n", solver_select2str(pool, select, what)); 02872 break; 02873 default: 02874 POOL_DEBUG(SAT_DEBUG_JOB, "job: unknown job\n"); 02875 break; 02876 } 02877 02878 /* 02879 * debug 02880 */ 02881 02882 IF_POOLDEBUG (SAT_DEBUG_JOB) 02883 { 02884 int j; 02885 if (solv->nrules == oldnrules) 02886 POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n"); 02887 for (j = oldnrules; j < solv->nrules; j++) 02888 { 02889 POOL_DEBUG(SAT_DEBUG_JOB, " - job "); 02890 solver_printrule(solv, SAT_DEBUG_JOB, solv->rules + j); 02891 } 02892 } 02893 } 02894 assert(solv->ruletojob.count == solv->nrules - solv->jobrules); 02895 solv->jobrules_end = solv->nrules; 02896 02897 /* now create infarch and dup rules */ 02898 if (!solv->noinfarchcheck) 02899 { 02900 solver_addinfarchrules(solv, &addedmap); 02901 if (pool->obsoleteusescolors) 02902 { 02903 /* currently doesn't work well with infarch rules, so make 02904 * them weak */ 02905 for (i = solv->infarchrules; i < solv->infarchrules_end; i++) 02906 queue_push(&solv->weakruleq, i); 02907 } 02908 } 02909 else 02910 solv->infarchrules = solv->infarchrules_end = solv->nrules; 02911 02912 if (hasdupjob) 02913 { 02914 solver_addduprules(solv, &addedmap); 02915 solver_freedupmaps(solv); /* no longer needed */ 02916 } 02917 else 02918 solv->duprules = solv->duprules_end = solv->nrules; 02919 02920 if (1) 02921 solver_addchoicerules(solv); 02922 else 02923 solv->choicerules = solv->choicerules_end = solv->nrules; 02924 02925 /* all rules created 02926 * -------------------------------------------------------------- 02927 * prepare for solving 02928 */ 02929 02930 /* free unneeded memory */ 02931 map_free(&addedmap); 02932 map_free(&installcandidatemap); 02933 queue_free(&q); 02934 02935 POOL_DEBUG(SAT_DEBUG_STATS, "%d rpm rules, %d job rules, %d infarch rules, %d dup rules, %d choice rules\n", solv->rpmrules_end - 1, solv->jobrules_end - solv->jobrules, solv->infarchrules_end - solv->infarchrules, solv->duprules_end - solv->duprules, solv->choicerules_end - solv->choicerules); 02936 02937 /* create weak map */ 02938 map_init(&solv->weakrulemap, solv->nrules); 02939 for (i = 0; i < solv->weakruleq.count; i++) 02940 { 02941 p = solv->weakruleq.elements[i]; 02942 MAPSET(&solv->weakrulemap, p); 02943 } 02944 02945 /* all new rules are learnt after this point */ 02946 solv->learntrules = solv->nrules; 02947 02948 /* create watches chains */ 02949 makewatches(solv); 02950 02951 /* create assertion index. it is only used to speed up 02952 * makeruledecsions() a bit */ 02953 for (i = 1, r = solv->rules + i; i < solv->nrules; i++, r++) 02954 if (r->p && !r->w2 && (r->d == 0 || r->d == -1)) 02955 queue_push(&solv->ruleassertions, i); 02956 02957 /* disable update rules that conflict with our job */ 02958 solver_disablepolicyrules(solv); 02959 02960 /* make initial decisions based on assertion rules */ 02961 makeruledecisions(solv); 02962 POOL_DEBUG(SAT_DEBUG_SOLVER, "problems so far: %d\n", solv->problems.count); 02963 02964 /* 02965 * ******************************************** 02966 * solve! 02967 * ******************************************** 02968 */ 02969 02970 now = sat_timems(0); 02971 solver_run_sat(solv, 1, solv->dontinstallrecommended ? 0 : 1); 02972 POOL_DEBUG(SAT_DEBUG_STATS, "solver took %d ms\n", sat_timems(now)); 02973 02974 /* 02975 * calculate recommended/suggested packages 02976 */ 02977 findrecommendedsuggested(solv); 02978 02979 /* 02980 * prepare solution queue if there were problems 02981 */ 02982 solver_prepare_solutions(solv); 02983 02984 /* 02985 * finally prepare transaction info 02986 */ 02987 transaction_calculate(&solv->trans, &solv->decisionq, &solv->noobsoletes); 02988 02989 POOL_DEBUG(SAT_DEBUG_STATS, "final solver statistics: %d problems, %d learned rules, %d unsolvable\n", solv->problems.count / 2, solv->stats_learned, solv->stats_unsolvable); 02990 POOL_DEBUG(SAT_DEBUG_STATS, "solver_solve took %d ms\n", sat_timems(solve_start)); 02991 } 02992 02993 /***********************************************************************/ 02994 /* disk usage computations */ 02995 02996 /*------------------------------------------------------------------- 02997 * 02998 * calculate DU changes 02999 */ 03000 03001 void 03002 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps) 03003 { 03004 Map installedmap; 03005 03006 solver_create_state_maps(solv, &installedmap, 0); 03007 pool_calc_duchanges(solv->pool, &installedmap, mps, nmps); 03008 map_free(&installedmap); 03009 } 03010 03011 03012 /*------------------------------------------------------------------- 03013 * 03014 * calculate changes in install size 03015 */ 03016 03017 int 03018 solver_calc_installsizechange(Solver *solv) 03019 { 03020 Map installedmap; 03021 int change; 03022 03023 solver_create_state_maps(solv, &installedmap, 0); 03024 change = pool_calc_installsizechange(solv->pool, &installedmap); 03025 map_free(&installedmap); 03026 return change; 03027 } 03028 03029 void 03030 solver_trivial_installable(Solver *solv, Queue *pkgs, Queue *res) 03031 { 03032 Map installedmap; 03033 solver_create_state_maps(solv, &installedmap, 0); 03034 pool_trivial_installable_noobsoletesmap(solv->pool, &installedmap, pkgs, res, solv->noobsoletes.size ? &solv->noobsoletes : 0); 03035 map_free(&installedmap); 03036 } 03037