Imported Upstream version 0.7.27

[platform/upstream/libsolv.git] / ext / testcase.c

diff --git a/ext/testcase.c b/ext/testcase.c
index 035cfdb..f46f738 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,82 @@ 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_decisionlist(solv, problem, SOLVER_DECISIONLIST_PROBLEM, &q);
+           }
+         else
+           {
+             s = testcase_ruleid(solv, lq.elements[problem - pcnt - 1]);
+             solver_get_decisionlist(solv, lq.elements[problem - pcnt - 1], SOLVER_DECISIONLIST_LEARNTRULE, &q);
+           }
+         probprefix = solv_dupjoin("proof ", s, 0);
+         for (i = 0; i < q.count; i += 3)
+           {
+             SolverRuleinfo rclass;
+             Queue rq;
+             Id truelit = q.elements[i];
+             Id rid = q.elements[i + 2];
+             char *rprefix;
+             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 / 3);
+             rprefix = solv_dupjoin(probprefix, " ", nbuf);
+             if (q.elements[i + 1] == SOLVER_REASON_PREMISE)
+               {
+                 rprefix = solv_dupappend(rprefix, " premise", 0);
+                 queue_empty(&rq);
+                 queue_push(&rq, truelit);
+               }
+             else
+               {
+                 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;
@@ -1481,59 +1558,20 @@ testcase_solverresult(Solver *solv, int resultflags)
     }
   if ((resultflags & TESTCASE_RESULT_ALTERNATIVES) != 0)
     {
-      char *altprefix;
-      Queue q, rq;
+      Queue q;
       int cnt;
       Id alternative;
       queue_init(&q);
-      queue_init(&rq);
       cnt = solver_alternatives_count(solv);
       for (alternative = 1; alternative <= cnt; alternative++)
        {
          Id id, from, chosen;
-         char num[20];
+         char num[20], *s;
          int type = solver_get_alternative(solv, alternative, &id, &from, &chosen, &q, 0);
-         altprefix = solv_dupjoin("alternative ", testcase_alternativeid(solv, type, id, from), " ");
+         char *altprefix = solv_dupjoin("alternative ", testcase_alternativeid(solv, type, id, from), " ");
          strcpy(num, " 0 ");
-         if (type == SOLVER_ALTERNATIVE_TYPE_RECOMMENDS)
-           {
-             char *s = pool_tmpjoin(pool, altprefix, num, testcase_solvid2str(pool, from));
-             s = pool_tmpappend(pool, s, " recommends ", testcase_dep2str(pool, id));
-             strqueue_push(&sq, s);
-           }
-         else if (type == SOLVER_ALTERNATIVE_TYPE_RULE)
-           {
-             /* map choice rules back to pkg rules */
-             if (solver_ruleclass(solv, id) == SOLVER_RULE_CHOICE)
-               id = solver_rule2pkgrule(solv, id);
-             if (solver_ruleclass(solv, id) == SOLVER_RULE_RECOMMENDS)
-               id = solver_rule2pkgrule(solv, id);
-             solver_allruleinfos(solv, id, &rq);
-             for (i = 0; i < rq.count; i += 4)
-               {
-                 int rtype = rq.elements[i];
-                 if ((rtype & SOLVER_RULE_TYPEMASK) == SOLVER_RULE_JOB)
-                   {
-                     const char *js = testcase_job2str(pool, rq.elements[i + 2], rq.elements[i + 3]);
-                     char *s = pool_tmpjoin(pool, altprefix, num, "job ");
-                     s = pool_tmpappend(pool, s, js, 0);
-                     strqueue_push(&sq, s);
-                   }
-                 else if (rtype == SOLVER_RULE_PKG_REQUIRES)
-                   {
-                     char *s = pool_tmpjoin(pool, altprefix, num, testcase_solvid2str(pool, rq.elements[i + 1]));
-                     s = pool_tmpappend(pool, s, " requires ", testcase_dep2str(pool, rq.elements[i + 3]));
-                     strqueue_push(&sq, s);
-                   }
-                 else if (rtype == SOLVER_RULE_UPDATE || rtype == SOLVER_RULE_FEATURE)
-                   {
-                     const char *js = testcase_solvid2str(pool, rq.elements[i + 1]);
-                     char *s = pool_tmpjoin(pool, altprefix, num, "update ");
-                     s = pool_tmpappend(pool, s, js, 0);
-                     strqueue_push(&sq, s);
-                   }
-               }
-           }
+          s = pool_tmpjoin(pool, altprefix, num, solver_alternative2str(solv, type, id, from));
+         strqueue_push(&sq, s);
          for (i = 0; i < q.count; i++)
            {
              Id p = q.elements[i];
@@ -1552,7 +1590,6 @@ testcase_solverresult(Solver *solv, int resultflags)
          solv_free(altprefix);
        }
       queue_free(&q);
-      queue_free(&rq);
     }
   if ((resultflags & TESTCASE_RESULT_RULES) != 0)
     {
@@ -2448,7 +2485,10 @@ testcase_read(Pool *pool, FILE *fp, const char *testcase, Queue *job, char **res
                }
            }
          if (resultp)
+         {
+           solv_free(*resultp);
            *resultp = result;
+         }
          else
            solv_free(result);
          if (resultflagsp)