From ba58eebc3cb907aaad2488425df245cb9ceb532a Mon Sep 17 00:00:00 2001
From: Michael Schroeder <mls@suse.de>
Date: Fri, 9 Sep 2022 14:10:16 +0200
Subject: [PATCH] Add functions to make proof reporting easier

solver_get_learnt: return all rearnt rules used in the proof
of a problem or another learnt rule.

solver_get_proof: return the decisions that led to the
problem or learnt rule.

Note that this is experimental and subject to change. We will
need to add some sorting code to solver_get_proof() to group
similar steps, but this means that we need to get the
ruleinfo for the involved rules. But in that case we can
as well also return the ruleinfo data with the call.
---
 ext/testcase.c  |  68 ++++++++++++++++++++++++++++++++
 ext/testcase.h  |   1 +
 src/libsolv.ver |   2 +
 src/problems.c  | 102 ++++++++++++++++++++++++++++++++++++++++++++++++
 src/problems.h  |   2 +
 src/solver.c    |   8 +++-
 6 files changed, 181 insertions(+), 2 deletions(-)

diff --git a/ext/testcase.c b/ext/testcase.c
index c529057a..838248b9 100644
--- a/ext/testcase.c
+++ b/ext/testcase.c
@@ -102,6 +102,7 @@ static struct resultflags2str {
   { TESTCASE_RESULT_USERINSTALLED,	"userinstalled" },
   { TESTCASE_RESULT_ORDER,		"order" },
   { TESTCASE_RESULT_ORDEREDGES,		"orderedges" },
+  { TESTCASE_RESULT_PROOF,		"proof" },
   { 0, 0 }
 };
 
@@ -1359,6 +1360,73 @@ testcase_solverresult(Solver *solv, int resultflags)
 	}
     }
 
+  if ((resultflags & TESTCASE_RESULT_PROOF) != 0)
+    {
+      char *probprefix;
+      int pcnt, problem;
+      Queue q, lq;
+
+      queue_init(&q);
+      queue_init(&lq);
+      pcnt = solver_problem_count(solv);
+      for (problem = 1; problem <= pcnt + lq.count; problem++)
+	{
+	  if (problem <= pcnt)
+	    {
+	      s = testcase_problemid(solv, problem);
+	      solver_get_proof(solv, problem, 0, &q);
+	    }
+	  else
+	    {
+	      s = testcase_ruleid(solv, lq.elements[problem - pcnt - 1]);
+	      solver_get_proof(solv, lq.elements[problem - pcnt - 1], 1, &q);
+	    }
+	  probprefix = solv_dupjoin("proof ", s, 0);
+	  for (i = 0; i < q.count; i += 2)
+	    {
+	      SolverRuleinfo rclass;
+	      Queue rq;
+	      Id rid = q.elements[i];
+	      char *rprefix;
+	      Id truelit = i + 1 < q.count ? q.elements[i + 1] : 0;
+	      char nbuf[16];
+
+	      rclass = solver_ruleclass(solv, rid);
+	      if (rclass == SOLVER_RULE_LEARNT)
+		queue_pushunique(&lq, rid);
+	      queue_init(&rq);
+	      solver_ruleliterals(solv, rid, &rq);
+	      sprintf(nbuf, "%3d", i / 2);
+	      rprefix = solv_dupjoin(probprefix, " ", nbuf);
+	      rprefix = solv_dupappend(rprefix, " ", testcase_rclass2str(rclass));
+	      rprefix = solv_dupappend(rprefix, " ", testcase_ruleid(solv, rid));
+	      strqueue_push(&sq, rprefix);
+	      solv_free(rprefix);
+	      rprefix = solv_dupjoin(probprefix, " ", nbuf);
+	      rprefix = solv_dupappend(rprefix, ": ", 0);
+	      for (j = 0; j < rq.count; j++)
+		{
+		  const char *s;
+		  Id p = rq.elements[j];
+		  if (p == truelit)
+		    s = pool_tmpjoin(pool, rprefix, "-->", 0);
+		  else
+		    s = pool_tmpjoin(pool, rprefix, "   ", 0);
+		  if (p < 0)
+		    s = pool_tmpappend(pool, s, " -", testcase_solvid2str(pool, -p));
+		  else
+		    s = pool_tmpappend(pool, s, "  ", testcase_solvid2str(pool, p));
+		  strqueue_push(&sq, s);
+		}
+	      solv_free(rprefix);
+	      queue_free(&rq);
+	    }
+	  solv_free(probprefix);
+	}
+      queue_free(&q);
+      queue_free(&lq);
+    }
+
   if ((resultflags & TESTCASE_RESULT_ORPHANED) != 0)
     {
       Queue q;
diff --git a/ext/testcase.h b/ext/testcase.h
index d57f116c..fae63798 100644
--- a/ext/testcase.h
+++ b/ext/testcase.h
@@ -23,6 +23,7 @@
 #define TESTCASE_RESULT_USERINSTALLED	(1 << 11)
 #define TESTCASE_RESULT_ORDER		(1 << 12)
 #define TESTCASE_RESULT_ORDEREDGES	(1 << 13)
+#define TESTCASE_RESULT_PROOF		(1 << 14)
 
 /* reuse solver hack, testsolv use only */
 #define TESTCASE_RESULT_REUSE_SOLVER	(1 << 31)
diff --git a/src/libsolv.ver b/src/libsolv.ver
index c77f8d37..1966161c 100644
--- a/src/libsolv.ver
+++ b/src/libsolv.ver
@@ -363,7 +363,9 @@ SOLV_1.0 {
 		solver_get_decisionqueue;
 		solver_get_flag;
 		solver_get_lastdecisionblocklevel;
+		solver_get_learnt;
 		solver_get_orphaned;
+		solver_get_proof;
 		solver_get_recommendations;
 		solver_get_unneeded;
 		solver_get_userinstalled;
diff --git a/src/problems.c b/src/problems.c
index 0bd48d4d..a228e455 100644
--- a/src/problems.c
+++ b/src/problems.c
@@ -1447,3 +1447,105 @@ solver_solutionelement2str(Solver *solv, Id p, Id rp)
     return "bad solution element";
 }
 
+void
+solver_get_proof(Solver *solv, Id id, int islearnt, Queue *q)
+{
+  Pool *pool = solv->pool;
+  Map seen, seent;	/* seent: was the literal true or false */
+  Id rid, truelit;
+  int first = 1;
+  int why, i, j;
+
+  queue_empty(q);
+  if (!islearnt)
+    why = solv->problems.elements[2 * id - 2];
+  else if (id >= solv->learntrules && id < solv->nrules)
+    why = solv->learnt_why.elements[id - solv->learntrules];
+  else
+    return;
+  map_init(&seen, pool->nsolvables);
+  map_init(&seent, pool->nsolvables);
+  while ((rid = solv->learnt_pool.elements[why++]) != 0)
+    {
+      Rule *r = solv->rules + rid;
+      Id p, pp;
+      truelit = 0;
+      FOR_RULELITERALS(p, pp, r)
+	{
+	  Id vv = p > 0 ? p : -p;
+	  if (MAPTST(&seen, vv))
+	    {
+	      if ((p > 0 ? 1 : 0) == (MAPTST(&seent, vv) ? 1 : 0))
+		{
+		  if (truelit)
+		    abort();
+		  truelit = p;		/* the one true literal! */
+		}
+	    }
+	  else
+	    {
+	      /* a new literal. it must be false as the rule is unit */
+	      MAPSET(&seen, vv);
+	      if (p < 0)
+		MAPSET(&seent, vv);
+	    }
+	}
+      if (truelit)
+        queue_push(q, truelit);
+      else if (!first)
+	abort();
+      queue_push(q, rid);
+      first = 0;
+    }
+  /* reverse proof queue */
+  for (i = 0, j = q->count - 1; i < j; i++, j--)
+    {
+      Id e = q->elements[i];
+      q->elements[i] = q->elements[j];
+      q->elements[j] = e;
+    }
+  map_free(&seen);
+  map_free(&seent);
+}
+
+void
+solver_get_learnt(Solver *solv, Id id, int islearnt, Queue *q)
+{
+  int why;
+  Queue todo;
+
+  queue_empty(q);
+  if (!islearnt)
+    why = solv->problems.elements[2 * id - 2];
+  else if (id >= solv->learntrules && id < solv->nrules)
+    why = solv->learnt_why.elements[id - solv->learntrules];
+  else
+    return;
+  queue_init(&todo);
+  queue_push(&todo, why);
+  while (todo.count)
+    {
+      int i, rid;
+      why = queue_pop(&todo);
+      while ((rid = solv->learnt_pool.elements[why++]) != 0)
+	{
+	  if (rid < solv->learntrules || rid >= solv->nrules)
+	    continue;
+	  /* insert sorted and unified */
+	  for (i = 0; i < q->count; i++)
+	    {
+	      if (q->elements[i] < rid)
+		continue;
+	      if (q->elements[i] == rid)
+		rid = 0;
+	      break;
+	    }
+	  if (!rid)
+	    continue;	/* already in list */
+	  queue_insert(q, i, rid);
+	  queue_push(&todo, solv->learnt_why.elements[rid - solv->learntrules]);
+	}
+    }
+  queue_free(&todo);
+}
+
diff --git a/src/problems.h b/src/problems.h
index f9b1efc3..9dd39a9d 100644
--- a/src/problems.h
+++ b/src/problems.h
@@ -51,6 +51,8 @@ void solver_take_solution(struct s_Solver *solv, Id problem, Id solution, Queue
 
 Id solver_findproblemrule(struct s_Solver *solv, Id problem);
 void solver_findallproblemrules(struct s_Solver *solv, Id problem, Queue *rules);
+void solver_get_proof(struct s_Solver *solv, Id id, int islearnt, Queue *q);
+void solver_get_learnt(struct s_Solver *solv, Id id, int islearnt, Queue *q);
 
 extern const char *solver_problemruleinfo2str(struct s_Solver *solv, SolverRuleinfo type, Id source, Id target, Id dep);
 extern const char *solver_problem2str(struct s_Solver *solv, Id problem);
diff --git a/src/solver.c b/src/solver.c
index e3779e23..42498fa2 100644
--- a/src/solver.c
+++ b/src/solver.c
@@ -986,7 +986,7 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
   FOR_RULELITERALS(v, pp, r)
     {
       if (DECISIONMAP_TRUE(v))	/* the one true literal */
-	  continue;
+	  abort();
       vv = v > 0 ? v : -v;
       MAPSET(&involved, vv);
     }
@@ -1005,8 +1005,12 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
       analyze_unsolvable_rule(solv, r, &weakq, &rseen);
       FOR_RULELITERALS(v, pp, r)
 	{
-	  if (DECISIONMAP_TRUE(v))	/* the one true literal */
+	  if (DECISIONMAP_TRUE(v))	/* the one true literal, i.e. our decision */
+	    {
+	      if (v != solv->decisionq.elements[idx])
+		abort();
 	      continue;
+	    }
 	  vv = v > 0 ? v : -v;
 	  MAPSET(&involved, vv);
 	}
-- 
2.25.1