-/* a problem is an item on the solver's problem list. It can either be >0, in that
- * case it is a update rule, or it can be <0, which makes it refer to a job
- * consisting of multiple job rules.
- */
-
-static void
-disableproblem(Solver *solv, Id v)
-{
- Rule *r;
- int i;
- Id *jp;
-
- if (v > 0)
- {
- disablerule(solv, solv->rules + v);
- return;
- }
- v = -(v + 1);
- jp = solv->ruletojob.elements;
- for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++, jp++)
- if (*jp == v)
- disablerule(solv, r);
-}
-
-/*-------------------------------------------------------------------
- * enableproblem
- */
-
-static void
-enableproblem(Solver *solv, Id v)
-{
- Rule *r;
- int i;
- Id *jp;
-
- if (v > 0)
- {
- if (v >= solv->featurerules && v < solv->featurerules_end)
- {
- /* do not enable feature rule if update rule is enabled */
- r = solv->rules + (v - solv->featurerules + solv->updaterules);
- if (r->d >= 0)
- return;
- }
- enablerule(solv, solv->rules + v);
- if (v >= solv->updaterules && v < solv->updaterules_end)
- {
- /* disable feature rule when enabling update rule */
- r = solv->rules + (v - solv->updaterules + solv->featurerules);
- if (r->p)
- disablerule(solv, r);
- }
- return;
- }
- v = -(v + 1);
- jp = solv->ruletojob.elements;
- for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++, jp++)
- if (*jp == v)
- enablerule(solv, r);
-}
-
-
-/************************************************************************/
-
-/*
- * make assertion rules into decisions
- *
- * go through update and job rules and add direct assertions
- * to the decisionqueue. If we find a conflict, disable rules and
- * add them to problem queue.
- */
-
-static void
-makeruledecisions(Solver *solv)
-{
- Pool *pool = solv->pool;
- int i, ri, ii;
- Rule *r, *rr;
- Id v, vv;
- int decisionstart;
-
- POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions ; size decisionq: %d -----\n",solv->decisionq.count);
-
- decisionstart = solv->decisionq.count;
- for (ii = 0; ii < solv->ruleassertions.count; ii++)
- {
- ri = solv->ruleassertions.elements[ii];
- r = solv->rules + ri;
-
- if (r->d < 0 || !r->p || r->w2) /* disabled, dummy or no assertion */
- continue;
- /* do weak rules in phase 2 */
- if (ri < solv->learntrules && MAPTST(&solv->weakrulemap, ri))
- continue;
-
- v = r->p;
- vv = v > 0 ? v : -v;
-
- if (!solv->decisionmap[vv]) /* if not yet decided */
- {
- /*
- * decide !
- */
- queue_push(&solv->decisionq, v);
- queue_push(&solv->decisionq_why, r - solv->rules);
- solv->decisionmap[vv] = v > 0 ? 1 : -1;
- IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
- {
- Solvable *s = solv->pool->solvables + vv;
- if (v < 0)
- POOL_DEBUG(SAT_DEBUG_PROPAGATE, "conflicting %s (assertion)\n", solvable2str(solv->pool, s));
- else
- POOL_DEBUG(SAT_DEBUG_PROPAGATE, "installing %s (assertion)\n", solvable2str(solv->pool, s));
- }
- continue;
- }
- /*
- * check previous decision: is it sane ?
- */
-
- if (v > 0 && solv->decisionmap[vv] > 0) /* ok to install */
- continue;
- if (v < 0 && solv->decisionmap[vv] < 0) /* ok to remove */
- continue;
-
- /*
- * found a conflict!
- *
- * The rule (r) we're currently processing says something
- * different (v = r->p) than a previous decision (decisionmap[abs(v)])
- * on this literal
- */
-
- if (ri >= solv->learntrules)
- {
- /* conflict with a learnt rule */
- /* can happen when packages cannot be installed for
- * multiple reasons. */
- /* we disable the learnt rule in this case */
- disablerule(solv, r);
- continue;
- }
-
- /*
- * find the decision which is the "opposite" of the rule
- */
-
- for (i = 0; i < solv->decisionq.count; i++)
- if (solv->decisionq.elements[i] == -v)
- break;
- assert(i < solv->decisionq.count); /* assert that we found it */
-
- /*
- * conflict with system solvable ?
- */
-
- if (v == -SYSTEMSOLVABLE) {
- /* conflict with system solvable */
- queue_push(&solv->problems, solv->learnt_pool.count);
- queue_push(&solv->learnt_pool, ri);
- queue_push(&solv->learnt_pool, 0);
- POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with system solvable, disabling rule #%d\n", ri);
- if (ri >= solv->jobrules && ri < solv->jobrules_end)
- v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
- else
- v = ri;
- queue_push(&solv->problems, v);
- queue_push(&solv->problems, 0);
- disableproblem(solv, v);
- continue;
- }
-
- assert(solv->decisionq_why.elements[i]);
-
- /*
- * conflict with an rpm rule ?
- */
-
- if (solv->decisionq_why.elements[i] < solv->rpmrules_end)
- {
- /* conflict with rpm rule assertion */
- queue_push(&solv->problems, solv->learnt_pool.count);
- queue_push(&solv->learnt_pool, ri);
- queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]);
- queue_push(&solv->learnt_pool, 0);
- assert(v > 0 || v == -SYSTEMSOLVABLE);
- POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with rpm rule, disabling rule #%d\n", ri);
- if (ri >= solv->jobrules && ri < solv->jobrules_end)
- v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
- else
- v = ri;
- queue_push(&solv->problems, v);
- queue_push(&solv->problems, 0);
- disableproblem(solv, v);
- continue;
- }
-
- /*
- * conflict with another job or update/feature rule
- */
-
- /* record proof */
- queue_push(&solv->problems, solv->learnt_pool.count);
- queue_push(&solv->learnt_pool, ri);
- queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]);
- queue_push(&solv->learnt_pool, 0);
-
- POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflicting update/job assertions over literal %d\n", vv);
-
- /*
- * push all of our rules (can only be feature or job rules)
- * asserting this literal on the problem stack
- */
-
- for (i = solv->featurerules, rr = solv->rules + i; i < solv->learntrules; i++, rr++)
- {
- if (rr->d < 0 /* disabled */
- || rr->w2) /* or no assertion */
- continue;
- if (rr->p != vv /* not affecting the literal */
- && rr->p != -vv)
- continue;
- if (MAPTST(&solv->weakrulemap, i)) /* weak: silently ignore */
- continue;
-
- POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, " - disabling rule #%d\n", i);
-
- solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, solv->rules + i);
-
- v = i;
- /* is is a job rule ? */
- if (i >= solv->jobrules && i < solv->jobrules_end)
- v = -(solv->ruletojob.elements[i - solv->jobrules] + 1);
-
- queue_push(&solv->problems, v);
- disableproblem(solv, v);
- }
- queue_push(&solv->problems, 0);
-
- /*
- * start over
- * (back up from decisions)
- */
- while (solv->decisionq.count > decisionstart)
- {
- v = solv->decisionq.elements[--solv->decisionq.count];
- --solv->decisionq_why.count;
- vv = v > 0 ? v : -v;
- solv->decisionmap[vv] = 0;
- }
- ii = -1; /* restarts loop at 0 */
- }
-
- /*
- * phase 2: now do the weak assertions
- */
- for (ii = 0; ii < solv->ruleassertions.count; ii++)
- {
- ri = solv->ruleassertions.elements[ii];
- r = solv->rules + ri;
- if (r->d < 0 || r->w2) /* disabled or no assertion */
- continue;
- if (!MAPTST(&solv->weakrulemap, ri)) /* skip non-weak */
- continue;
- v = r->p;
- vv = v > 0 ? v : -v;
- /*
- * decide !
- * (if not yet decided)
- */
- if (!solv->decisionmap[vv])
- {
- queue_push(&solv->decisionq, v);
- queue_push(&solv->decisionq_why, r - solv->rules);
- solv->decisionmap[vv] = v > 0 ? 1 : -1;
- IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
- {
- Solvable *s = solv->pool->solvables + vv;
- if (v < 0)
- POOL_DEBUG(SAT_DEBUG_PROPAGATE, "conflicting %s (weak assertion)\n", solvable2str(solv->pool, s));
- else
- POOL_DEBUG(SAT_DEBUG_PROPAGATE, "installing %s (weak assertion)\n", solvable2str(solv->pool, s));
- }
- continue;
- }
- /*
- * previously decided, sane ?
- */
- if (v > 0 && solv->decisionmap[vv] > 0)
- continue;
- if (v < 0 && solv->decisionmap[vv] < 0)
- continue;
-
- POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "assertion conflict, but I am weak, disabling ");
- solver_printrule(solv, SAT_DEBUG_UNSOLVABLE, r);
- disablerule(solv, r);
- }
-
- POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions end; size decisionq: %d -----\n",solv->decisionq.count);
-}
-
-
-/*-------------------------------------------------------------------
- * enable/disable learnt rules
- *
- * we have enabled or disabled some of our rules. We now reenable all
- * of our learnt rules but the ones that were learnt from rules that
- * are now disabled.
- */
-static void
-enabledisablelearntrules(Solver *solv)
-{
- Pool *pool = solv->pool;
- Rule *r;
- Id why, *whyp;
- int i;
-
- POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "enabledisablelearntrules called\n");
- for (i = solv->learntrules, r = solv->rules + i; i < solv->nrules; i++, r++)
- {
- whyp = solv->learnt_pool.elements + solv->learnt_why.elements[i - solv->learntrules];
- while ((why = *whyp++) != 0)
- {
- assert(why > 0 && why < i);
- if (solv->rules[why].d < 0)
- break;
- }
- /* why != 0: we found a disabled rule, disable the learnt rule */
- if (why && r->d >= 0)
- {
- IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
- {
- POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "disabling ");
- solver_printruleclass(solv, SAT_DEBUG_SOLUTIONS, r);
- }
- disablerule(solv, r);
- }
- else if (!why && r->d < 0)
- {
- IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
- {
- POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "re-enabling ");
- solver_printruleclass(solv, SAT_DEBUG_SOLUTIONS, r);
- }
- enablerule(solv, r);
- }
- }
-}
-
-
-/*-------------------------------------------------------------------
- * enable weak rules
- *
- * Enable all rules, except learnt rules, which are
- * - disabled and weak (set in weakrulemap)
- *
- */
-
-static void
-enableweakrules(Solver *solv)
-{
- int i;
- Rule *r;
-
- for (i = 1, r = solv->rules + i; i < solv->learntrules; i++, r++)
- {
- if (r->d >= 0) /* skip non-direct literals */
- continue;
- if (!MAPTST(&solv->weakrulemap, i))
- continue;
- enablerule(solv, r);
- }
-}
-
-
-/* FIXME: bad code ahead, replace as soon as possible */
-/* FIXME: should probably look at SOLVER_INSTALL|SOLVABLE_ONE_OF */
-
-/*-------------------------------------------------------------------
- * disable update rules
- */
-
-static void
-disableupdaterules(Solver *solv, Queue *job, int jobidx)
-{
- Pool *pool = solv->pool;
- int i, j;
- Id how, select, what, p, pp;
- Solvable *s;
- Repo *installed;
- Rule *r;
- Id lastjob = -1;
-
- installed = solv->installed;
- if (!installed)
- return;
-
- if (jobidx != -1)
- {
- how = job->elements[jobidx];
- select = how & SOLVER_SELECTMASK;
- switch (how & SOLVER_JOBMASK)
- {
- case SOLVER_ERASE:
- break;
- case SOLVER_INSTALL:
- if (select != SOLVER_SOLVABLE)
- return;
- break;
- default:
- return;
- }
- }
- /* go through all enabled job rules */
- MAPZERO(&solv->noupdate);
- for (i = solv->jobrules; i < solv->jobrules_end; i++)
- {
- r = solv->rules + i;
- if (r->d < 0) /* disabled? */
- continue;
- j = solv->ruletojob.elements[i - solv->jobrules];
- if (j == lastjob)
- continue;
- lastjob = j;
- how = job->elements[j];
- what = job->elements[j + 1];
- select = how & SOLVER_SELECTMASK;
- switch (how & SOLVER_JOBMASK)
- {
- case SOLVER_INSTALL:
- if (select != SOLVER_SOLVABLE)
- break;
- s = pool->solvables + what;
- if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, what))
- break;
- if (s->repo == installed)
- {
- MAPSET(&solv->noupdate, what - installed->start);
- break;
- }
- if (s->obsoletes)
- {
- Id obs, *obsp;
- obsp = s->repo->idarraydata + s->obsoletes;
- while ((obs = *obsp++) != 0)
- FOR_PROVIDES(p, pp, obs)
- {
- if (pool->solvables[p].repo != installed)
- continue;
- if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
- continue;
- MAPSET(&solv->noupdate, p - installed->start);
- }
- }
- FOR_PROVIDES(p, pp, s->name)
- {
- if (!solv->implicitobsoleteusesprovides && pool->solvables[p].name != s->name)
- continue;
- if (pool->solvables[p].repo == installed)
- MAPSET(&solv->noupdate, p - installed->start);
- }
- break;
- case SOLVER_ERASE:
- FOR_JOB_SELECT(p, pp, select, what)
- if (pool->solvables[p].repo == installed)
- MAPSET(&solv->noupdate, p - installed->start);
- break;
- default:
- break;
- }
- }
-
- /* fixup update rule status */
- if (jobidx != -1)
- {
- /* we just disabled job #jobidx. enable all update rules
- * that aren't disabled by the remaining job rules */
- how = job->elements[jobidx];
- what = job->elements[jobidx + 1];
- select = how & SOLVER_SELECTMASK;
- switch (how & SOLVER_JOBMASK)
- {
- case SOLVER_INSTALL:
- if (select != SOLVER_SOLVABLE)
- break;
- s = pool->solvables + what;
- if (s->repo == installed)
- {
- r = solv->rules + solv->updaterules + (what - installed->start);
- if (r->d >= 0)
- break;
- enablerule(solv, r);
- IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
- {
- POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "@@@ re-enabling ");
- solver_printrule(solv, SAT_DEBUG_SOLUTIONS, r);
- }
- break;
- }
- if (s->obsoletes)
- {
- Id obs, *obsp;
- obsp = s->repo->idarraydata + s->obsoletes;
- while ((obs = *obsp++) != 0)
- FOR_PROVIDES(p, pp, obs)
- {
- if (pool->solvables[p].repo != installed)
- continue;
- if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
- continue;
- if (MAPTST(&solv->noupdate, p - installed->start))
- continue;
- r = solv->rules + solv->updaterules + (p - installed->start);
- if (r->d >= 0)
- continue;
- enablerule(solv, r);
- IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
- {
- POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "@@@ re-enabling ");
- solver_printrule(solv, SAT_DEBUG_SOLUTIONS, r);
- }
- }
- }
- FOR_PROVIDES(p, pp, s->name)
- {
- if (!solv->implicitobsoleteusesprovides && pool->solvables[p].name != s->name)
- continue;
- if (pool->solvables[p].repo != installed)
- continue;
- if (MAPTST(&solv->noupdate, p - installed->start))
- continue;
- r = solv->rules + solv->updaterules + (p - installed->start);
- if (r->d >= 0)
- continue;
- enablerule(solv, r);
- IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
- {
- POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "@@@ re-enabling ");
- solver_printrule(solv, SAT_DEBUG_SOLUTIONS, r);
- }
- }
- break;
- case SOLVER_ERASE:
- FOR_JOB_SELECT(p, pp, select, what)