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.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
get' m = get' (_numActives m)
set' m = set' (_numActives m)
instance StackFamily ClauseSimpleManager C.Clause where
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
newManager initialSize = do
i <- new' 0
v <- C.newClauseVector initialSize
ClauseSimpleManager i <$> IORef.newIORef v
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
get' m = get' (_nActives m)
set' m = set' (_nActives m)
instance StackFamily ClauseExtManager C.Clause where
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 $ MV.length v
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
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
getClauseVector !m = IORef.readIORef (_clauseVector m)
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
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
getKeyVector :: ClauseExtManager -> IO (Vec [Int])
getKeyVector ClauseExtManager{..} = IORef.readIORef _keyVector
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 $ MV.length v
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"
reset m = set' (_nActives m) 0
type WatcherList = V.Vector ClauseExtManager
newWatcherList :: Int -> Int -> IO WatcherList
newWatcherList n m = V.replicateM (int2lit (negate n) + 2) (newManager m)
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"
reset = V.mapM_ purifyManager