- make installed packages pass much faster

- disable classes of choice rules
- add solver_printdecisionq() debug function

diff --git a/src/rules.c b/src/rules.c
index 5a186da..0069e75 100644 (file)
--- a/src/rules.c
+++ b/src/rules.c
@@ -1788,6 +1788,7 @@ addchoicerules(Solver *solv)
       solv->choicerules_end = solv->nrules;
       return;
     }
+  solv->choicerules_ref = sat_calloc(solv->rpmrules_end, sizeof(Id));
   queue_init(&q);
   for (rid = 1; rid < solv->rpmrules_end ; rid++)
     {
@@ -1871,10 +1872,46 @@ addchoicerules(Solver *solv)
       d = q.count ? pool_queuetowhatprovides(pool, &q) : 0;
       solver_addrule(solv, r->p, d);
       queue_push(&solv->weakruleq, solv->nrules - 1);
-      /* solver_printrule(solv, SAT_DEBUG_RESULT, solv->rules + solv->nrules - 1); */
+      solv->choicerules_ref[solv->nrules - 1 - solv->choicerules] = rid;
+#if 0
+      printf("OLD ");
+      solver_printrule(solv, SAT_DEBUG_RESULT, solv->rules + rid);
+      printf("WEAK CHOICE ");
+      solver_printrule(solv, SAT_DEBUG_RESULT, solv->rules + solv->nrules - 1);
+#endif
     }
   queue_free(&q);
   solv->choicerules_end = solv->nrules;
 }
 
+void
+disablechoicerules(Solver *solv, Rule *r)
+{
+  Id rid, p, *pp;
+  Pool *pool = solv->pool;
+  Map m;
+  Rule *or;
+
+  or = solv->rules + solv->choicerules_ref[(r - solv->rules) - solv->choicerules];
+  map_init(&m, pool->nsolvables);
+  FOR_RULELITERALS(p, pp, or)
+    if (p > 0)
+      MAPSET(&m, p);
+  FOR_RULELITERALS(p, pp, r)
+    if (p > 0)
+      MAPCLR(&m, p);
+  for (rid = solv->choicerules; rid < solv->choicerules_end; rid++)
+    {
+      r = solv->rules + rid;
+      if (r->d < 0)
+       continue;
+      or = solv->rules + solv->choicerules_ref[(r - solv->rules) - solv->choicerules];
+      FOR_RULELITERALS(p, pp, or)
+        if (p > 0 && MAPTST(&m, p))
+         break;
+      if (p)
+       solver_disablerule(solv, r);
+    }
+}
+
 /* EOF */

diff --git a/src/solver.c b/src/solver.c
index 206be13..98f8dd0 100644 (file)
--- a/src/solver.c
+++ b/src/solver.c
@@ -975,6 +975,7 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
   if (lastweak)
     {
       Id v;
+      extern void disablechoicerules(Solver *solv, Rule *r);
       /* disable last weak rule */
       solv->problems.count = oldproblemcount;
       solv->learnt_pool.count = oldlearntpoolcount;
@@ -984,6 +985,8 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
         v = lastweak;
       POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling ");
       solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, solv->rules + lastweak);
+      if (lastweak >= solv->choicerules && lastweak < solv->choicerules_end)
+       disablechoicerules(solv, solv->rules + lastweak);
       solver_disableproblem(solv, v);
       if (v < 0)
        solver_reenablepolicyrules(solv, -(v + 1));
@@ -1299,6 +1302,7 @@ solver_free(Solver *solv)
   sat_free(solv->obsoletes);
   sat_free(solv->obsoletes_data);
   sat_free(solv->multiversionupdaters);
+  sat_free(solv->choicerules_ref);
   sat_free(solv);
 }
 
@@ -1324,6 +1328,7 @@ solver_run_sat(Solver *solv, int disablerules, int doweak)
   Pool *pool = solv->pool;
   Id p, *dp;
   int minimizationsteps;
+  int installedpos = solv->installed ? solv->installed->start : 0;
 
   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
     {
@@ -1340,7 +1345,7 @@ solver_run_sat(Solver *solv, int disablerules, int doweak)
   /* start SAT algorithm */
   level = 1;
   systemlevel = level + 1;
-  POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n");
+  POOL_DEBUG(SAT_DEBUG_SOLVER, "solving...\n");
 
   queue_init(&dq);
   queue_init(&dqs);
@@ -1362,7 +1367,6 @@ solver_run_sat(Solver *solv, int disablerules, int doweak)
       /*
        * propagate
        */
-
       if (level == 1)
        {
          POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
@@ -1441,21 +1445,30 @@ solver_run_sat(Solver *solv, int disablerules, int doweak)
          Repo *installed = solv->installed;
          int pass;
 
+         POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving installed packages\n");
          /* we use two passes if we need to update packages 
            * to create a better user experience */
          for (pass = solv->updatemap.size ? 0 : 1; pass < 2; pass++)
            {
-             FOR_REPO_SOLVABLES(installed, i, s)
+             int passlevel = level;
+             /* start with installedpos, the position that gave us problems last time */
+             for (i = installedpos, n = installed->start; n < installed->end; i++, n++)
                {
                  Rule *rr;
                  Id d;
 
+                 if (i == installed->end)
+                   i = installed->start;
+                 s = pool->solvables + i;
+                 if (s->repo != installed)
+                   continue;
+
+                 if (solv->decisionmap[i] > 0)
+                   continue;
                  /* XXX: noupdate check is probably no longer needed, as all jobs should
                    * already be satisfied */
                  if (MAPTST(&solv->noupdate, i - installed->start))
                    continue;
-                 if (solv->decisionmap[i] > 0)
-                   continue;
                  if (!pass && solv->updatemap.size && !MAPTST(&solv->updatemap, i - installed->start))
                    continue;           /* updates first */
                  r = solv->rules + solv->updaterules + (i - installed->start);
@@ -1517,7 +1530,15 @@ solver_run_sat(Solver *solv, int disablerules, int doweak)
                          return;
                        }
                      if (level <= olevel)
-                       break;
+                       {
+                         if (level < passlevel)
+                           break;      /* trouble */
+                         if (level < olevel)
+                           n = installed->start;       /* redo all */
+                         i--;
+                         n--;
+                         continue;
+                       }
                    }
                  /* if still undecided keep package */
                  if (solv->decisionmap[i] == 0)
@@ -1532,11 +1553,23 @@ solver_run_sat(Solver *solv, int disablerules, int doweak)
                          return;
                        }
                      if (level <= olevel)
-                       break;
+                       {
+                         if (level < passlevel)
+                           break;      /* trouble */
+                         if (level < olevel)
+                           n = installed->start;       /* redo all */
+                         i--;
+                         n--;
+                         continue; /* retry with learnt rule */
+                       }
                    }
                }
-             if (i < installed->end)
-               break;
+             if (n < installed->end)
+               {
+                 installedpos = i;     /* retry problem solvable next time */
+                 break;                /* ran into trouble */
+               }
+             installedpos = installed->start;  /* reset installedpos */
            }
          systemlevel = level + 1;
          if (pass < 2)
@@ -1551,10 +1584,8 @@ solver_run_sat(Solver *solv, int disablerules, int doweak)
        */
 
       POOL_DEBUG(SAT_DEBUG_POLICY, "deciding unresolved rules\n");
-      for (i = 1, n = 1; ; i++, n++)
+      for (i = 1, n = 1; n < solv->nrules; i++, n++)
        {
-         if (n == solv->nrules)
-           break;
          if (i == solv->nrules)
            i = 1;
          r = solv->rules + i;
@@ -2005,6 +2036,9 @@ solver_run_sat(Solver *solv, int disablerules, int doweak)
   POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
   queue_free(&dq);
   queue_free(&dqs);
+#if 0
+  solver_printdecisionq(solv, SAT_DEBUG_RESULT);
+#endif
 }
 
 

diff --git a/src/solver.h b/src/solver.h
index 91a7664..5b3884e 100644 (file)
--- a/src/solver.h
+++ b/src/solver.h
@@ -76,6 +76,7 @@ typedef struct _Solver {
     
   Id choicerules;                      /* choice rules (always weak) */
   Id choicerules_end;
+  Id *choicerules_ref;
 
   Id learntrules;                      /* learnt rules, (end == nrules) */
 

diff --git a/src/solverdebug.c b/src/solverdebug.c
index ee43212..48cfaba 100644 (file)
--- a/src/solverdebug.c
+++ b/src/solverdebug.c
@@ -203,7 +203,7 @@ solver_printruleclass(Solver *solv, int type, Rule *r)
   if (p < solv->learntrules)
     if (MAPTST(&solv->weakrulemap, p))
       POOL_DEBUG(type, "WEAK ");
-  if (p >= solv->learntrules)
+  if (solv->learntrules && p >= solv->learntrules)
     POOL_DEBUG(type, "LEARNT ");
   else if (p >= solv->choicerules && p < solv->choicerules_end)
     POOL_DEBUG(type, "CHOICE ");
@@ -256,6 +256,37 @@ solver_printwatches(Solver *solv, int type)
     POOL_DEBUG(type, "    solvable [%d] -- rule [%d]\n", counter, solv->watches[counter + pool->nsolvables]);
 }
 
+void
+solver_printdecisionq(Solver *solv, int type)
+{
+  Pool *pool = solv->pool;
+  int i;
+  Id p, why;
+
+  POOL_DEBUG(type, "Decisions:\n");
+  for (i = 0; i < solv->decisionq.count; i++)
+    {
+      p = solv->decisionq.elements[i];
+      if (p > 0)
+        POOL_DEBUG(type, "%d %d install  %s, ", i, solv->decisionmap[p], solvid2str(pool, p));
+      else
+        POOL_DEBUG(type, "%d %d conflict %s, ", i, -solv->decisionmap[-p], solvid2str(pool, -p));
+      why = solv->decisionq_why.elements[i];
+      if (why > 0)
+       {
+         POOL_DEBUG(type, "forced by ");
+         solver_printruleclass(solv, type, solv->rules + why);
+       }
+      else if (why < 0)
+       {
+         POOL_DEBUG(type, "chosen from ");
+         solver_printruleclass(solv, type, solv->rules - why);
+       }
+      else
+        POOL_DEBUG(type, "picked for some unknown reason.\n");
+    }
+}
+
 /*
  * printdecisions
  */

diff --git a/src/solverdebug.h b/src/solverdebug.h
index 8b2feec..50fff6b 100644 (file)
--- a/src/solverdebug.h
+++ b/src/solverdebug.h
@@ -23,6 +23,7 @@ extern void solver_printrule(Solver *solv, int type, Rule *r);
 extern void solver_printruleclass(Solver *solv, int type, Rule *r);
 extern void solver_printproblem(Solver *solv, Id v);
 extern void solver_printwatches(Solver *solv, int type);
+extern void solver_printdecisionq(Solver *solv, int type);
 extern void solver_printdecisions(Solver *solv);
 extern void solver_printtransaction(Solver *solv);
 extern void solver_printprobleminfo(Solver *solv, Id problem);