From d4f96a9e7d39c2142ee0f1d7d7971cad98df6584 Mon Sep 17 00:00:00 2001
From: Michael Schroeder <mls@suse.de>
Date: Thu, 15 Nov 2007 19:24:03 +0000
Subject: [PATCH] - speed solving up a bit by not removing learnt rules if
 rules get   disabled

---
 src/solver.c | 97 ++++++++++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 82 insertions(+), 15 deletions(-)

diff --git a/src/solver.c b/src/solver.c
index b2bcaca..7bb44c6 100644
--- a/src/solver.c
+++ b/src/solver.c
@@ -550,15 +550,12 @@ makeruledecisions(Solver *solv)
   Id v, vv;
   int decisionstart;
 
-  /* no learnt rules for now */
-  if (solv->learntrules && solv->learntrules != solv->nrules)
-    abort();
-
   decisionstart = solv->decisionq.count;
-  /* the loop is over jobrules, system rules and weak rules */
+  /* 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++)
     {
-      if (!r->w1 || r->w2)
+      if (!r->w1 || r->w2)	/* disabled or no assertion */
 	continue;
       v = r->p;
       vv = v > 0 ? v : -v;
@@ -574,12 +571,19 @@ makeruledecisions(Solver *solv)
       if (v < 0 && solv->decisionmap[vv] < 0)
 	continue;
       /* found a conflict! */
+      if (solv->learntrules && ri >= solv->learntrules)
+        {
+	  /* cannot happen, as this would mean that the problem
+           * was not solvable, so we wouldn't have created the
+           * learnt rule at all */
+	  abort();
+        }
       /* if we are weak, just disable ourself */
       if (ri >= solv->weakrules)
 	{
 	  printf("conflict, but I am weak, disabling ");
 	  printrule(solv, r);
-	  r->w1 = 0;
+	  disablerule(solv, r);
 	  continue;
 	}
       /* only job and system rules left */
@@ -641,6 +645,53 @@ makeruledecisions(Solver *solv)
     }
 }
 
+/*
+ * 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;
+
+  if (pool->verbose)
+    printf("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)
+	{
+	  if (why < 0 || why >= i)
+	    abort();		/* cannot reference newer learnt rules */
+	  if (!solv->rules[why].w1)
+	    break;
+	}
+      /* why != 0: we found a disabled rule, disable the learnt rule */
+      if (why && r->w1)
+	{
+	  if (pool->verbose)
+	    {
+	      printf("disabling learnt ");
+	      printrule(solv, r);
+	    }
+          disablerule(solv, r);
+	}
+      else if (!why && !r->w1)
+	{
+	  if (pool->verbose)
+	    {
+	      printf("re-enabling learnt ");
+	      printrule(solv, r);
+	    }
+          enablerule(solv, r);
+	}
+    }
+}
+
 
 /* FIXME: bad code ahead, replace as soon as possible */
 static void
@@ -797,7 +848,7 @@ disableupdaterules(Solver *solv, Queue *job, int jobidx)
     {
       r = solv->rules + solv->systemrules + i;
       if (r->w1 && MAPTST(&solv->noupdate, i))
-	r->w1 = 0;		/* was enabled, need to disable */
+        disablerule(solv, r);	/* was enabled, need to disable */
     }
 }
 
@@ -1307,7 +1358,18 @@ analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *why)
   idx = solv->decisionq.count;
   for (;;)
     {
-      if (pool->verbose > 1) printrule(solv, c);
+      if (pool->verbose > 1)
+	{
+	  if (c - solv->rules >= solv->learntrules)
+	    printf("LEARNT ");
+	  else if (c - solv->rules >= solv->weakrules)
+	    printf("WEAK ");
+	  else if (c - solv->rules >= solv->systemrules)
+	    printf("SYSTEM ");
+	  else if (c - solv->rules >= solv->jobrules)
+	    printf("JOB ");
+	  printrule(solv, c);
+	}
       queue_push(&solv->learnt_pool, c - solv->rules);
       dp = c->d ? pool->whatprovidesdata + c->d : 0;
       for (i = -1; ; i++)
@@ -1417,10 +1479,14 @@ reset_solver(Solver *solv)
   int i;
   Id v;
 
+#if 0
   /* delete all learnt rules */
   solv->nrules = solv->learntrules;
   queue_empty(&solv->learnt_why);
   queue_empty(&solv->learnt_pool);
+#else
+  enabledisablelearntrules(solv);
+#endif
 
   /* redo all direct rpm rule decisions */
   /* we break at the first decision with a why attached, this is
@@ -1450,8 +1516,8 @@ reset_solver(Solver *solv)
   /* redo all job/system decisions */
   makeruledecisions(solv);
   if (solv->pool->verbose > 1)
-    printf("decisions after adding job and system rules: %d\n", solv->decisionq.count);
-  /* recreate watches */
+    printf("decisions so far: %d\n", solv->decisionq.count);
+  /* recreate watch chains */
   makewatches(solv);
 }
 
@@ -1612,7 +1678,7 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
       r = solv->rules + lastweak;
       printf("disabling weak ");
       printrule(solv, r);
-      r->w1 = 0;
+      disablerule(solv, r);
       reset_solver(solv);
       return 1;
     }
@@ -1919,9 +1985,7 @@ run_solver(Solver *solv, int disablerules, int doweak)
 	printrule(solv, solv->rules + i);
     }
 
-  /* all new rules are learnt after this point */
-  solv->learntrules = solv->nrules;
-  /* crate watches lists */
+  /* create watches chains */
   makewatches(solv);
 
   if (pool->verbose) printf("initial decisions: %d\n", solv->decisionq.count);
@@ -3326,6 +3390,9 @@ solve(Solver *solv, Queue *job)
 	  }
     }
 
+  /* all new rules are learnt after this point */
+  solv->learntrules = solv->nrules;
+
   /*
    * solve !
    * 
-- 
2.7.4