+ /* phase 2: now do the weak assertions */
+ for (ri = 1, r = solv->rules + ri; ri < solv->learntrules; ri++, r++)
+ {
+ if (!r->w1 || r->w2) /* disabled or no assertion */
+ continue;
+ if (!MAPTST(&solv->weakrulemap, ri))
+ continue;
+ v = r->p;
+ vv = v > 0 ? v : -v;
+ 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;
+ }
+ 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 ");
+ printrule(solv, SAT_DEBUG_UNSOLVABLE, r);
+ disablerule(solv, r);
+ }
+
+ POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions end; size decisionq: %d -----\n",solv->decisionq.count);