From: Michael Schroeder Date: Fri, 9 Sep 2022 12:10:16 +0000 (+0200) Subject: Add functions to make proof reporting easier X-Git-Tag: 0.7.23~52 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=ba58eebc3cb907aaad2488425df245cb9ceb532a;p=thirdparty%2Flibsolv.git 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 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); }