From dabfd4fe6dacc6bb2abeeca1decc26050af03129 Mon Sep 17 00:00:00 2001
From: Michael Schroeder <mls@suse.de>
Date: Fri, 16 Nov 2007 22:06:57 +0000
Subject: [PATCH] - log complete proof

---
 src/solver.c | 43 +++++++++++++++++++++++++++++++++++--------
 1 file changed, 35 insertions(+), 8 deletions(-)

diff --git a/src/solver.c b/src/solver.c
index 0087923..1e64c51 100644
--- a/src/solver.c
+++ b/src/solver.c
@@ -607,11 +607,6 @@ makeruledecisions(Solver *solv)
 	  continue;
 	}
 
-      /* record proof */
-      queue_push(&solv->problems, solv->learnt_pool.count);
-      queue_push(&solv->learnt_pool, ri);
-      queue_push(&solv->learnt_pool, 0);
-
       /* only job and system rules left */
       for (i = 0; i < solv->decisionq.count; i++)
 	if (solv->decisionq.elements[i] == -v)
@@ -621,6 +616,13 @@ makeruledecisions(Solver *solv)
       if (solv->decisionq_why.elements[i] == 0)
 	{
 	  /* conflict with rpm rule, need only disable our rule */
+	  if (v < 0 && v != -SYSTEMSOLVABLE)
+	    abort();
+	  /* record proof */
+	  queue_push(&solv->problems, solv->learnt_pool.count);
+	  queue_push(&solv->learnt_pool, ri);
+	  queue_push(&solv->learnt_pool, v != -SYSTEMSOLVABLE ? -v : v);
+	  queue_push(&solv->learnt_pool, 0);
 	  printf("conflict with rpm rule, disabling rule #%d\n", ri);
 	  if (ri < solv->systemrules)
 	    v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
@@ -629,6 +631,12 @@ makeruledecisions(Solver *solv)
 	  queue_push(&solv->problems, 0);
 	  continue;
 	}
+      /* 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);
+
       /* conflict with another job or system rule */
       printf("conflicting system/job rules over literal %d\n", vv);
       /* push all of our rules asserting this literal on the problem stack */
@@ -1612,11 +1620,13 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
   int l, i, idx;
   Id *decisionmap = solv->decisionmap;
   int oldproblemcount;
+  int oldlearntpoolcount;
   int lastweak;
 
   if (pool->verbose > 1)
     printf("ANALYZE UNSOLVABLE ----------------------\n");
   oldproblemcount = solv->problems.count;
+  oldlearntpoolcount = solv->learnt_pool.count;
 
   /* make room for proof index */
   /* must update it later, as analyze_unsolvable_rule would confuse
@@ -1625,6 +1635,7 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
 
   r = cr;
   map_init(&seen, pool->nsolvables);
+  queue_push(&solv->learnt_pool, r - solv->rules);
   analyze_unsolvable_rule(solv, r);
   dp = r->d ? pool->whatprovidesdata + r->d : 0;
   for (i = -1; ; i++)
@@ -1655,14 +1666,22 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
       why = solv->decisionq_why.elements[idx];
       if (!why)
 	{
+	  /* level 1 and no why, must be an rpm assertion */
 	  if (pool->verbose > 3)
 	    {
 	      printf("RPM ");
 	      printruleelement(solv, 0, v);
 	    }
+	  /* this is the only positive rpm assertion */
+	  if (v == SYSTEMSOLVABLE)
+	    v = -v;
+	  if (v >= 0)
+	    abort();
+	  queue_push(&solv->learnt_pool, v);
 	  continue;
 	}
       r = solv->rules + why;
+      queue_push(&solv->learnt_pool, why);
       analyze_unsolvable_rule(solv, r);
       dp = r->d ? pool->whatprovidesdata + r->d : 0;
       for (i = -1; ; i++)
@@ -1703,6 +1722,7 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
     {
       /* disable last weak rule */
       solv->problems.count = oldproblemcount;
+      solv->learnt_pool.count = oldlearntpoolcount;
       r = solv->rules + lastweak;
       printf("disabling weak ");
       printrule(solv, r);
@@ -1711,10 +1731,9 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
       return 1;
     }
 
-  /* record proof */
-  solv->problems.elements[oldproblemcount] = solv->learnt_pool.count;
-  queue_push(&solv->learnt_pool, cr - solv->rules);
+  /* finish proof */
   queue_push(&solv->learnt_pool, 0);
+  solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
 
   if (disablerules)
     {
@@ -2782,8 +2801,16 @@ printprobleminfo(Solver *solv, Queue *job, Id idx)
 	    }
 	  return;
 	}
+      if (p > 0 && solv->learnt_pool.elements[idx + 1] == -p)
+	{
+	  /* we conflicted with a direct rpm assertion */
+	  /* print other rule */
+	  p = -p;
+	  rn = 0;
+	}
       if (rn >= solv->jobrules)
 	{
+	  printf("some job/system/learnt rule\n");
 	  printrule(solv, r);
 	  return;
 	}
-- 
2.34.1