Commit 6c00067c authored by Franz Thoma's avatar Franz Thoma
Browse files

Fix conflict counting bug

We used to miss a lot of conflicts during counting in `logBackjump`.
Counting initial conflicts here drastically reduces search time in some
cases.
Not sure whether counting the current conflicts (`cs`) may be even
better than counting the initial conflicts (`initial`).
parent be9992db
......@@ -60,7 +60,10 @@ backjump (EnableBackjumping enableBj) var initial xs =
| otherwise = f (csAcc `CS.union` cs) cm'
logBackjump :: ConflictSet QPN -> ConflictMap -> ConflictSetLog a
logBackjump cs cm = failWith (Failure cs Backjump) (cs, cm)
logBackjump cs cm = failWith (Failure cs Backjump) (cs, updateCM initial cm)
-- 'intial' instead of 'cs' here ---^
-- since we do not want to double-count the
-- additionally accumulated conflicts.
type ConflictSetLog = RetryLog Message (ConflictSet QPN, ConflictMap)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment