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.

diff --git a/ext/testcase.c b/ext/testcase.c
index c529057a8f02a61e1534d995fb615863f5188cc4..838248b96a904e223c55c424ed3a60bf9dc507a5 100644 (file)
--- 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 d57f116c7cb401ad70c9223f5a42210071339212..fae63798f35cc1bca3bc14d7709f9b7e247f80e9 100644 (file)
--- 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 c77f8d372d5839afae35d22fad3c04d767417235..1966161c6661a61ac3c5d9ce5d153eda47a0709e 100644 (file)
--- 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 0bd48d4db6010b5cbdc5106322cb7d15baa2ebff..a228e4551acb6ce884702213b0d76ca897f23d94 100644 (file)
--- 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 f9b1efc3cfebcf6d66f02679d8874c5dbd106952..9dd39a9d6dbc164f6a84dc4cb29f3acbfde32669 100644 (file)
--- 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 e3779e23252c66005d7b1ee9a2c928dd64e782c7..42498fa226085d66b7df9323d3fa1756aa81d974 100644 (file)
--- 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);
        }