diff --git a/Add-functions-to-make-proof-reporting-easier.patch b/Add-functions-to-make-proof-reporting-easier.patch new file mode 100644 index 0000000000000000000000000000000000000000..8f406b9db2be42b9cfe9877cc31bbba2526bc46e --- /dev/null +++ b/Add-functions-to-make-proof-reporting-easier.patch @@ -0,0 +1,290 @@ +From ba58eebc3cb907aaad2488425df245cb9ceb532a Mon Sep 17 00:00:00 2001 +From: Michael Schroeder +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 + diff --git a/libsolv.spec b/libsolv.spec index 29d82dddeca4b6fb65707bdda752640f11e4cae7..ed31507397c811621a3efd53917879d130ff76f9 100644 --- a/libsolv.spec +++ b/libsolv.spec @@ -15,7 +15,7 @@ Name: libsolv Version: 0.7.20 -Release: 3 +Release: 4 Summary: Package dependency solver License: BSD URL: https://github.com/openSUSE/libsolv @@ -24,6 +24,7 @@ Source: https://github.com/openSUSE/libsolv/archive/refs/tags/%{v Patch0: Fix-segfault-on-conflict-resolution-when-using-bindi.patch Patch1: Fix-memory-leak-when-using-testsolv-to-execute-cases.patch Patch2: ensure-duplinvolvedmap_all-is-reset.patch +Patch3: Add-functions-to-make-proof-reporting-easier.patch BuildRequires: cmake gcc-c++ ninja-build pkgconfig(rpm) zlib-devel BuildRequires: libxml2-devel xz-devel bzip2-devel @@ -217,6 +218,12 @@ Python 3 version. %{_mandir}/man3/%{name}*.3* %changelog +* Wed Nov 3 2022 zhangjun - 0.7.20-4 +- Type:enhancement +- ID:NA +- SUG:NA +- DESC:Add functions to make proof reporting easier + * Fri Oct 21 2022 hanhuihui - 0.7.20-3 - Type:bugfix - ID:NA