summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMichael Schroeder <mls@suse.de>2014-02-17 13:23:54 +0100
committerMichael Schroeder <mls@suse.de>2014-02-17 13:23:54 +0100
commit82149483e908492b349ac6a43b9414936f9a4295 (patch)
tree403fdffa3fe2b29f5fefbb10f0689bb285b00079
parent1bc0138ea114a264fd33c8321e0777a2ca5c638e (diff)
downloadlibsolv-82149483e908492b349ac6a43b9414936f9a4295.tar.gz
libsolv-82149483e908492b349ac6a43b9414936f9a4295.tar.bz2
libsolv-82149483e908492b349ac6a43b9414936f9a4295.zip
optimize unfulfilled rule handling a bit
-rw-r--r--src/solver.c20
1 files changed, 11 insertions, 9 deletions
diff --git a/src/solver.c b/src/solver.c
index 177dd0d..4ffdec4 100644
--- a/src/solver.c
+++ b/src/solver.c
@@ -2063,12 +2063,18 @@ solver_run_sat(Solver *solv, int disablerules, int doweak)
r = solv->rules + i;
if (r->d < 0) /* ignore disabled rules */
continue;
- queue_empty(&dq);
+ if (r->p < 0) /* most common cases first */
+ {
+ if (r->d == 0 || solv->decisionmap[-r->p] <= 0)
+ continue;
+ }
+ if (dq.count)
+ queue_empty(&dq);
if (r->d == 0)
{
/* binary or unary rule */
- /* need two positive undecided literals */
- if (r->p < 0 || r->w2 <= 0)
+ /* need two positive undecided literals, r->p already checked above */
+ if (r->w2 <= 0)
continue;
if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
continue;
@@ -2082,13 +2088,9 @@ solver_run_sat(Solver *solv, int disablerules, int doweak)
* no positive literal is installed
* i.e. the rule is not fulfilled and we
* just need to decide on the positive literals
+ * (decisionmap[-r->p] for the r->p < 0 case is already checked above)
*/
- if (r->p < 0)
- {
- if (solv->decisionmap[-r->p] <= 0)
- continue;
- }
- else
+ if (r->p >= 0)
{
if (solv->decisionmap[r->p] > 0)
continue;