From: Michael Matz <matz@suse.de>
Date: Wed, 6 Feb 2008 01:46:44 +0000 (+0000)
Subject: I understand the solver a bit now , enough to hack around the problem causing
X-Git-Tag: BASE-SuSE-Code-12_1-Branch~308^2~669
X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=b545920b07bfb52a72eeca35988e93a103c48696;p=thirdparty%2Flibsolv.git

I understand the solver a bit now , enough to hack around the problem causing
#354404 .  See the elaborate comment.  No additional test suite errors
(i.e. only those from the disabling of locale/language support).
---

diff --git a/src/solver.c b/src/solver.c
index b407c46e..c5c35570 100644
--- a/src/solver.c
+++ b/src/solver.c
@@ -604,6 +604,56 @@ makeruledecisions(Solver *solv)
   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions ; size decisionq: %d -----\n",solv->decisionq.count);
 
   decisionstart = solv->decisionq.count;
+#if 1
+  /* FIXME: For the time being we first need to assert what we can get
+     from learned rules.  Currently it can happen that we learn a unit
+     rule (i.e. assertion) in direct conflict with e.g. a job unit rule.  The 
+     input problem was unsolvable, but we can't deal with this situation
+     of two conflicting assertions (see also FIXME at refine_suggestion).
+
+     What normally would happen (without this loop), we would first see the
+     job rule (and let's say decide to install A), and later see the learned
+     rule (which says don't install A), have a conflict, and assert, because
+     we don't ever expect to see conflicts with learned rules.
+
+     So we gather assertions from learned rules first.  This then leads
+     to a conflict with a job rule, which is dealt with (mostly).  We note
+     that job rule as a problem (and don't remember the learned rule as a
+     problem like we would normally do, as even other code doesn't expect to
+     see learned rules in problem descriptions.
+
+     We need to deal with this situation in a better way, preferably by
+     never learning unit rules in conflicts with any other unit rule.  */
+
+  for (ri = solv->learntrules, r = solv->rules + ri; ri < solv->nrules; ri++, r++)
+    {
+      if (!r->w1 || r->w2)	/* disabled or no assertion */
+	continue;
+      v = r->p;
+      vv = v > 0 ? v : -v;
+      if (solv->decisionmap[vv] == 0)
+	{
+	  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;
+	}
+      if (v > 0 && solv->decisionmap[vv] > 0)
+	continue;
+      if (v < 0 && solv->decisionmap[vv] < 0)
+	continue;
+      /* found a conflict, which can't happen with learned rules.  */
+      assert(0);
+    }
+#endif
   /* rpm rules don't have assertions, so we can start with the job
    * rules */
   for (ri = solv->jobrules, r = solv->rules + ri; ri < solv->nrules; ri++, r++)
@@ -686,6 +736,10 @@ makeruledecisions(Solver *solv)
 	    continue;
 	  if (rr->p != vv && rr->p != -vv)
 	    continue;
+	  /* See the large comment in front of the very first loop in this
+	     function at FIXME.  */
+	  if (i >= solv->learntrules)
+	    continue;
 	  POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, " - disabling rule #%d\n", i);
 	  v = i;
 	  if (i < solv->systemrules)