From: Michael Schroeder Date: Thu, 14 Apr 2011 12:57:14 +0000 (+0200) Subject: - add some comments, prepare to make proof recording optional X-Git-Tag: BASE-SuSE-Code-12_1-Branch~73 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=3f38d2c9a022cedeea84bc34052879439dd7456d;p=thirdparty%2Flibsolv.git - add some comments, prepare to make proof recording optional --- diff --git a/src/solver.c b/src/solver.c index 3ab12be1..068e2dc7 100644 --- a/src/solver.c +++ b/src/solver.c @@ -112,6 +112,7 @@ makeruledecisions(Solver *solv) Rule *r, *rr; Id v, vv; int decisionstart; + int record_proof = 1; POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions ; size decisionq: %d -----\n",solv->decisionq.count); @@ -194,35 +195,46 @@ makeruledecisions(Solver *solv) * conflict with system solvable ? */ - if (v == -SYSTEMSOLVABLE) { - /* conflict with system solvable */ - queue_push(&solv->problems, solv->learnt_pool.count); - queue_push(&solv->learnt_pool, ri); - queue_push(&solv->learnt_pool, 0); - POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with system solvable, disabling rule #%d\n", ri); - if (ri >= solv->jobrules && ri < solv->jobrules_end) - v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1); - else - v = ri; - queue_push(&solv->problems, v); - queue_push(&solv->problems, 0); - solver_disableproblem(solv, v); - continue; - } + if (v == -SYSTEMSOLVABLE) + { + /* conflict with system solvable */ + if (record_proof) + { + queue_push(&solv->problems, solv->learnt_pool.count); + queue_push(&solv->learnt_pool, ri); + queue_push(&solv->learnt_pool, 0); + } + else + queue_push(&solv->problems, 0); + POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with system solvable, disabling rule #%d\n", ri); + if (ri >= solv->jobrules && ri < solv->jobrules_end) + v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1); + else + v = ri; + queue_push(&solv->problems, v); + queue_push(&solv->problems, 0); + solver_disableproblem(solv, v); + continue; + } assert(solv->decisionq_why.elements[i] > 0); - + /* * conflict with an rpm rule ? */ - + if (solv->decisionq_why.elements[i] < solv->rpmrules_end) { /* conflict with rpm rule assertion */ - queue_push(&solv->problems, solv->learnt_pool.count); - queue_push(&solv->learnt_pool, ri); - queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]); - queue_push(&solv->learnt_pool, 0); + if (record_proof) + { + queue_push(&solv->problems, solv->learnt_pool.count); + queue_push(&solv->learnt_pool, ri); + queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]); + queue_push(&solv->learnt_pool, 0); + } + else + queue_push(&solv->problems, 0); assert(v > 0 || v == -SYSTEMSOLVABLE); POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with rpm rule, disabling rule #%d\n", ri); if (ri >= solv->jobrules && ri < solv->jobrules_end) @@ -240,10 +252,15 @@ makeruledecisions(Solver *solv) */ /* record proof */ - queue_push(&solv->problems, solv->learnt_pool.count); - queue_push(&solv->learnt_pool, ri); - queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]); - queue_push(&solv->learnt_pool, 0); + if (record_proof) + { + queue_push(&solv->problems, solv->learnt_pool.count); + queue_push(&solv->learnt_pool, ri); + queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]); + queue_push(&solv->learnt_pool, 0); + } + else + queue_push(&solv->problems, 0); POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflicting update/job assertions over literal %d\n", vv); @@ -678,6 +695,7 @@ analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp) { Pool *pool = solv->pool; Queue r; + Id r_buf[4]; int rlevel = 1; Map seen; /* global? */ Id d, v, vv, *dp, why; @@ -686,7 +704,7 @@ analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp) int learnt_why = solv->learnt_pool.count; Id *decisionmap = solv->decisionmap; - queue_init(&r); + queue_init_buffer(&r, r_buf, sizeof(r_buf)/sizeof(*r_buf)); POOL_DEBUG(SAT_DEBUG_ANALYZE, "ANALYZE at %d ----------------------\n", level); map_init(&seen, pool->nsolvables); @@ -718,7 +736,7 @@ analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp) l = solv->decisionmap[vv]; if (l < 0) l = -l; - MAPSET(&seen, vv); + MAPSET(&seen, vv); /* mark that we also need to look at this literal */ if (l == 1) l1num++; /* need to do this one in level1 pass */ else if (l == level) @@ -733,6 +751,9 @@ analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp) l1retry: if (!num && !--l1num) break; /* all level 1 literals done */ + + /* find the next literal to investigate */ + /* (as num + l1num > 0, we know that we'll always find one) */ for (;;) { assert(idx > 0); @@ -742,21 +763,24 @@ l1retry: break; } MAPCLR(&seen, vv); + if (num && --num == 0) { *pr = -v; /* so that v doesn't get lost */ if (!l1num) break; POOL_DEBUG(SAT_DEBUG_ANALYZE, "got %d involved level 1 decisions\n", l1num); + /* clear non-l1 bits from seen map */ for (i = 0; i < r.count; i++) { v = r.elements[i]; MAPCLR(&seen, v > 0 ? v : -v); } - /* only level 1 marks left */ - l1num++; + /* only level 1 marks left in seen map */ + l1num++; /* as l1retry decrements it */ goto l1retry; } + why = solv->decisionq_why.elements[idx]; if (why <= 0) /* just in case, maybe for SYSTEMSOLVABLE */ goto l1retry; @@ -781,6 +805,7 @@ l1retry: queue_push(&solv->learnt_pool, 0); if (whyp) *whyp = learnt_why; + queue_free(&r); solv->stats_learned++; return rlevel; } @@ -817,7 +842,7 @@ solver_reset(Solver *solv) /* adapt learnt rule status to new set of enabled/disabled rules */ enabledisablelearntrules(solv); - /* redo all job/update decisions */ + /* redo all assertion rule decisions */ makeruledecisions(solv); POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count); } @@ -895,13 +920,14 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules) Pool *pool = solv->pool; Rule *r; Map seen; /* global to speed things up? */ + Map rseen; Id d, v, vv, *dp, why; int l, i, idx; Id *decisionmap = solv->decisionmap; int oldproblemcount; int oldlearntpoolcount; Id lastweak; - Map rseen; + int record_proof = 1; POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n"); solv->stats_unsolvable++; @@ -916,7 +942,8 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules) r = cr; map_init(&seen, pool->nsolvables); map_init(&rseen, solv->nrules); - queue_push(&solv->learnt_pool, r - solv->rules); + if (record_proof) + queue_push(&solv->learnt_pool, r - solv->rules); lastweak = 0; analyze_unsolvable_rule(solv, r, &lastweak, &rseen); d = r->d < 0 ? -r->d - 1 : r->d; @@ -948,7 +975,8 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules) continue; why = solv->decisionq_why.elements[idx]; assert(why > 0); - queue_push(&solv->learnt_pool, why); + if (record_proof) + queue_push(&solv->learnt_pool, why); r = solv->rules + why; if (!MAPTST(&rseen, why)) analyze_unsolvable_rule(solv, r, &lastweak, &rseen); @@ -999,8 +1027,11 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules) } /* finish proof */ - queue_push(&solv->learnt_pool, 0); - solv->problems.elements[oldproblemcount] = oldlearntpoolcount; + if (record_proof) + { + queue_push(&solv->learnt_pool, 0); + solv->problems.elements[oldproblemcount] = oldlearntpoolcount; + } if (disablerules) { @@ -1021,7 +1052,7 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules) /*------------------------------------------------------------------- * * revert - * revert decision at level + * revert decisionq to a level */ static void @@ -1250,6 +1281,8 @@ solver_create(Pool *pool) queue_init(&solv->weakruleq); queue_init(&solv->ruleassertions); + queue_push(&solv->learnt_pool, 0); /* so that 0 does not describe a proof */ + map_init(&solv->recommendsmap, pool->nsolvables); map_init(&solv->suggestsmap, pool->nsolvables); map_init(&solv->noupdate, solv->installed ? solv->installed->end - solv->installed->start : 0);