{-# LANGUAGE
BangPatterns
, FlexibleInstances
, MultiParamTypeClasses
, RecordWildCards
, ViewPatterns
#-}
{-# LANGUAGE Trustworthy #-}
module SAT.Mios.ClauseManager
(
ClauseManager (..)
, ClauseSimpleManager
, ClauseExtManager
, pushClauseWithKey
, getKeyVector
, markClause
, WatcherList
, newWatcherList
, getNthWatcher
)
where
import Control.Monad (unless, when)
import qualified Data.IORef as IORef
import qualified Data.Primitive.ByteArray as BA
import qualified Data.Vector as V
import qualified Data.Vector.Mutable as MV
import SAT.Mios.Types
import qualified SAT.Mios.Clause as C
class ClauseManager a where
newManager :: Int -> IO a
getClauseVector :: a -> IO C.ClauseVector
data ClauseSimpleManager = ClauseSimpleManager
{
_numActives :: !Int'
, _clsVector :: IORef.IORef C.ClauseVector
}
instance SingleStorage ClauseSimpleManager Int where
{-# SPECIALIZE INLINE get' :: ClauseSimpleManager -> IO Int #-}
get' m = get' (_numActives m)
{-# SPECIALIZE INLINE set' :: ClauseSimpleManager -> Int -> IO () #-}
set' m = set' (_numActives m)
instance StackFamily ClauseSimpleManager C.Clause where
{-# SPECIALIZE INLINE shrinkBy :: ClauseSimpleManager -> Int -> IO () #-}
shrinkBy m k = modify' (_numActives m) (subtract k)
pushTo ClauseSimpleManager{..} c = do
!n <- get' _numActives
!v <- IORef.readIORef _clsVector
if MV.length v - 1 <= n
then do
let len = max 8 $ MV.length v
v' <- MV.unsafeGrow v len
MV.unsafeWrite v' n c
IORef.writeIORef _clsVector v'
else MV.unsafeWrite v n c
modify' _numActives (1 +)
popFrom m = modify' (_numActives m) (subtract 1)
lastOf ClauseSimpleManager{..} = do
n <- get' _numActives
v <- IORef.readIORef _clsVector
MV.unsafeRead v (n - 1)
instance ClauseManager ClauseSimpleManager where
{-# SPECIALIZE INLINE newManager :: Int -> IO ClauseSimpleManager #-}
newManager initialSize = do
i <- new' 0
v <- C.newClauseVector initialSize
ClauseSimpleManager i <$> IORef.newIORef v
{-# SPECIALIZE INLINE getClauseVector :: ClauseSimpleManager -> IO C.ClauseVector #-}
getClauseVector !m = IORef.readIORef (_clsVector m)
data ClauseExtManager = ClauseExtManager
{
_nActives :: !Int'
, _purged :: !Bool'
, _clauseVector :: IORef.IORef C.ClauseVector
, _keyVector :: IORef.IORef (Vec Int)
}
instance SingleStorage ClauseExtManager Int where
{-# SPECIALIZE INLINE get' :: ClauseExtManager -> IO Int #-}
get' m = get' (_nActives m)
{-# SPECIALIZE INLINE set' :: ClauseExtManager -> Int -> IO () #-}
set' m = set' (_nActives m)
instance StackFamily ClauseExtManager C.Clause where
{-# SPECIALIZE INLINE shrinkBy :: ClauseExtManager -> Int -> IO () #-}
shrinkBy m k = modify' (_nActives m) (subtract k)
pushTo ClauseExtManager{..} c = do
!n <- get' _nActives
!v <- IORef.readIORef _clauseVector
!b <- IORef.readIORef _keyVector
if MV.length v - 1 <= n
then do
let len = max 8 $ div (MV.length v) 2
v' <- MV.unsafeGrow v len
b' <- growBy b len
MV.unsafeWrite v' n c
setNth b' n 0
IORef.writeIORef _clauseVector v'
IORef.writeIORef _keyVector b'
else MV.unsafeWrite v n c >> setNth b n 0
modify' _nActives (1 +)
popFrom m = modify' (_nActives m) (subtract 1)
lastOf ClauseExtManager{..} = do
n <- get' _nActives
v <- IORef.readIORef _clauseVector
MV.unsafeRead v (n - 1)
instance ClauseManager ClauseExtManager where
{-# SPECIALIZE INLINE newManager :: Int -> IO ClauseExtManager #-}
newManager initialSize = do
i <- new' 0
v <- C.newClauseVector initialSize
b <- newVec (MV.length v) 0
ClauseExtManager i <$> new' False <*> IORef.newIORef v <*> IORef.newIORef b
{-# SPECIALIZE INLINE getClauseVector :: ClauseExtManager -> IO C.ClauseVector #-}
getClauseVector !m = IORef.readIORef (_clauseVector m)
{-# INLINABLE markClause #-}
markClause :: ClauseExtManager -> C.Clause -> IO ()
markClause ClauseExtManager{..} c = do
!n <- get' _nActives
!v <- IORef.readIORef _clauseVector
let
seekIndex :: Int -> IO ()
seekIndex k = do
c' <- MV.unsafeRead v k
if c' == c then MV.unsafeWrite v k C.NullClause else seekIndex $ k + 1
unless (n == 0) $ do
seekIndex 0
set' _purged True
{-# INLINABLE purifyManager #-}
purifyManager :: ClauseExtManager -> IO ()
purifyManager ClauseExtManager{..} = do
diry <- get' _purged
when diry $ do
n <- get' _nActives
vec <- IORef.readIORef _clauseVector
keys <- IORef.readIORef _keyVector
let
loop :: Int -> Int -> IO Int
loop ((< n) -> False) n' = return n'
loop i j = do
c <- getNth vec i
if c /= C.NullClause
then do
unless (i == j) $ do
setNth vec j c
setNth keys j =<< getNth keys i
loop (i + 1) (j + 1)
else loop (i + 1) j
set' _nActives =<< loop 0 0
set' _purged False
{-# INLINE getKeyVector #-}
getKeyVector :: ClauseExtManager -> IO (Vec Int)
getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector
{-# INLINABLE pushClauseWithKey #-}
pushClauseWithKey :: ClauseExtManager -> C.Clause -> Lit -> IO ()
pushClauseWithKey ClauseExtManager{..} !c k = do
!n <- get' _nActives
!v <- IORef.readIORef _clauseVector
!b <- IORef.readIORef _keyVector
if MV.length v - 1 <= n
then do
let len = max 8 $ div (MV.length v) 2
v' <- MV.unsafeGrow v len
b' <- growBy b len
MV.unsafeWrite v' n c
setNth b' n k
IORef.writeIORef _clauseVector v'
IORef.writeIORef _keyVector b'
else MV.unsafeWrite v n c >> setNth b n k
modify' _nActives (1 +)
instance VecFamily ClauseExtManager C.Clause where
getNth = error "no getNth method for ClauseExtManager"
setNth = error "no setNth method for ClauseExtManager"
{-# SPECIALIZE INLINE reset :: ClauseExtManager -> IO () #-}
reset m = set' (_nActives m) 0
type WatcherList = V.Vector ClauseExtManager
newWatcherList :: Int -> Int -> IO WatcherList
newWatcherList n m = do let n' = int2lit (negate n) + 2
v <- MV.unsafeNew n'
mapM_ (\i -> MV.unsafeWrite v i =<< newManager m) [0 .. n' - 1]
V.unsafeFreeze v
{-# INLINE getNthWatcher #-}
getNthWatcher :: WatcherList -> Lit -> ClauseExtManager
getNthWatcher = V.unsafeIndex
instance VecFamily WatcherList C.Clause where
getNth = error "no getNth method for WatcherList"
setNth = error "no setNth method for WatcherList"
{-# SPECIALIZE INLINE reset :: WatcherList -> IO () #-}
reset = V.mapM_ purifyManager
{-# INLINE setKeyVector #-}
setKeyVector :: ClauseExtManager -> Vec Int -> IO ()
setKeyVector ClauseExtManager{..} v = IORef.writeIORef _keyVector v
{-# INLINABLE allocateKeyVectorSize #-}
allocateKeyVectorSize :: ClauseExtManager -> Int -> IO (Vec Int)
allocateKeyVectorSize ClauseExtManager{..} n' = do
v <- IORef.readIORef _keyVector
if realLength v < n'
then do v' <- newVec n' 0
IORef.writeIORef _keyVector v'
return v'
else return v