From 5f9c97811b4c5607b4ebe187fd6aae65dbd143e0 Mon Sep 17 00:00:00 2001 From: Michael Schroeder Date: Fri, 15 Apr 2011 11:28:41 +0200 Subject: [PATCH] analyze_unsolvable: save memory be only using the rseen map for learnt rules --- src/solver.c | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/solver.c b/src/solver.c index 068e2dc..6f5b98a 100644 --- a/src/solver.c +++ b/src/solver.c @@ -862,11 +862,13 @@ analyze_unsolvable_rule(Solver *solv, Rule *r, Id *lastweakp, Map *rseen) IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE) solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r); - MAPSET(rseen, why); if (solv->learntrules && why >= solv->learntrules) { + if (MAPTST(rseen, why - solv->learntrules)) + return; + MAPSET(rseen, why - solv->learntrules); for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++) - if (solv->learnt_pool.elements[i] > 0 && !MAPTST(rseen, solv->learnt_pool.elements[i])) + if (solv->learnt_pool.elements[i] > 0) analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], lastweakp, rseen); return; } @@ -941,7 +943,7 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules) r = cr; map_init(&seen, pool->nsolvables); - map_init(&rseen, solv->nrules); + map_init(&rseen, solv->learntrules ? solv->nrules - solv->learntrules : 0); if (record_proof) queue_push(&solv->learnt_pool, r - solv->rules); lastweak = 0; @@ -978,8 +980,7 @@ analyze_unsolvable(Solver *solv, Rule *cr, int disablerules) if (record_proof) queue_push(&solv->learnt_pool, why); r = solv->rules + why; - if (!MAPTST(&rseen, why)) - analyze_unsolvable_rule(solv, r, &lastweak, &rseen); + analyze_unsolvable_rule(solv, r, &lastweak, &rseen); d = r->d < 0 ? -r->d - 1 : r->d; dp = d ? pool->whatprovidesdata + d : 0; for (i = -1; ; i++) @@ -2989,7 +2990,7 @@ solver_solve(Solver *solv, Queue *job) /* disable update rules that conflict with our job */ solver_disablepolicyrules(solv); - /* make decisions based on job/update assertions */ + /* make initial decisions based on assertion rules */ makeruledecisions(solv); POOL_DEBUG(SAT_DEBUG_SOLVER, "problems so far: %d\n", solv->problems.count); -- 2.7.4