Author: mlschroe Date: Mon Jan 7 19:51:06 2008 New Revision: 8220 URL: http://svn.opensuse.org/viewcvs/zypp?rev=8220&view=rev Log: - also push level 1 rules on leanrt stack - this also fixes a nasty bug where a learnt rule was not disabled by enabledisablelearntrules() Modified: trunk/sat-solver/src/solver.c Modified: trunk/sat-solver/src/solver.c URL: http://svn.opensuse.org/viewcvs/zypp/trunk/sat-solver/src/solver.c?rev=8220&r1=8219&r2=8220&view=diff ============================================================================== --- trunk/sat-solver/src/solver.c (original) +++ trunk/sat-solver/src/solver.c Mon Jan 7 19:51:06 2008 @@ -1417,7 +1417,7 @@ Map seen; /* global? */ Id v, vv, *dp; int l, i, idx; - int num = 0; + int num = 0, l1num = 0; int learnt_why = solv->learnt_pool.count; Id *decisionmap = solv->decisionmap; @@ -1432,6 +1432,7 @@ printruleclass(solv, SAT_DEBUG_ANALYZE, c); queue_push(&solv->learnt_pool, c - solv->rules); dp = c->d ? pool->whatprovidesdata + c->d : 0; + /* go through all literals of the rule */ for (i = -1; ; i++) { if (i == -1) @@ -1442,8 +1443,9 @@ v = *dp++; if (v == 0) break; + if (DECISIONMAP_TRUE(v)) /* the one true literal */ - continue; + continue; vv = v > 0 ? v : -v; if (MAPTST(&seen, vv)) continue; @@ -1452,6 +1454,7 @@ l = -l; if (l == 1) { + /* a level 1 literal, mark it for later */ #if 0 int j; for (j = 0; j < solv->decisionq.count; j++) @@ -1461,7 +1464,9 @@ abort(); queue_push(&rulq, -(j + 1)); #endif - continue; /* initial setting */ + MAPSET(&seen, vv); /* mark for scanning in level 1 phase */ + l1num++; + continue; } MAPSET(&seen, vv); if (l == level) @@ -1487,7 +1492,46 @@ if (--num == 0) break; } - *pr = -v; + *pr = -v; /* so that v doesn't get lost */ + + /* add involved level 1 rules */ + if (l1num) + { + POOL_DEBUG(SAT_DEBUG_ANALYZE, "got %d involved level 1 decisions\n", l1num); + idx++; + while (idx) + { + v = solv->decisionq.elements[--idx]; + vv = v > 0 ? v : -v; + if (!MAPTST(&seen, vv)) + continue; + if (!solv->decisionq_why.elements[idx]) + continue; + c = solv->rules + solv->decisionq_why.elements[idx]; + IF_POOLDEBUG (SAT_DEBUG_ANALYZE) + printruleclass(solv, SAT_DEBUG_ANALYZE, c); + queue_push(&solv->learnt_pool, c - solv->rules); + for (i = -1; ; i++) + { + if (i == -1) + v = c->p; + else if (c->d == 0) + v = i ? 0 : c->w2; + else + v = *dp++; + if (v == 0) + break; + if (DECISIONMAP_TRUE(v)) /* the one true literal */ + continue; + vv = v > 0 ? v : -v; + l = solv->decisionmap[vv]; + if (l != 1 && l != -1) + continue; + MAPSET(&seen, vv); + } + } + } + if (r.count == 0) *dr = 0; else if (r.count == 1 && r.elements[0] < 0) @@ -1497,7 +1541,7 @@ IF_POOLDEBUG (SAT_DEBUG_ANALYZE) { POOL_DEBUG(SAT_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level); - printruleelement(solv, SAT_DEBUG_ANALYZE, 0, -v); + printruleelement(solv, SAT_DEBUG_ANALYZE, 0, *pr); for (i = 0; i < r.count; i++) printruleelement(solv, SAT_DEBUG_ANALYZE, 0, r.elements[i]); } -- To unsubscribe, e-mail: zypp-commit+unsubscribe@opensuse.org For additional commands, e-mail: zypp-commit+help@opensuse.org