mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-12-24 05:55:18 +03:00
Improve memory usage of pbBacktrack
This commit is contained in:
parent
7aa7f5cc80
commit
37d25048d3
@ -67,13 +67,13 @@ pbBv pb ds = preEmpCount ds <= pb
|
|||||||
-- the same state being reached multiple times, but is needed because
|
-- the same state being reached multiple times, but is needed because
|
||||||
-- of the artificial dependency imposed by the bound.
|
-- of the artificial dependency imposed by the bound.
|
||||||
pbBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]
|
pbBacktrack :: [BacktrackStep] -> Int -> ThreadId -> [BacktrackStep]
|
||||||
pbBacktrack bs i tid = backtrack True (backtrack False bs i tid) (maximum js) tid where
|
pbBacktrack bs i tid = maybe id (\j b -> backtrack True b j tid) j $ backtrack False bs i tid where
|
||||||
-- Index of the conservative point
|
-- Index of the conservative point
|
||||||
js = 0 : [ j
|
j = goJ . reverse . pairs $ zip [0..i-1] bs where
|
||||||
| ((_,b1), (j,b2)) <- pairs $ zip [0..] bs
|
goJ (((_,b1), (j,b2)):rest)
|
||||||
, _threadid b1 /= _threadid b2
|
| _threadid b1 /= _threadid b2 = Just j
|
||||||
, j < i
|
| otherwise = goJ rest
|
||||||
]
|
goJ [] = Nothing
|
||||||
|
|
||||||
{-# INLINE pairs #-}
|
{-# INLINE pairs #-}
|
||||||
pairs = zip <*> tail
|
pairs = zip <*> tail
|
||||||
|
Loading…
Reference in New Issue
Block a user