{-# LANGUAGE
ViewPatterns
#-}
{-# LANGUAGE Trustworthy #-}
module SAT.Mios.ClausePool
(
ClausePool
, newClausePool
, makeClauseFromStack
, putBackToPool
)
where
import Control.Monad (when)
import qualified Data.Vector as V
import SAT.Mios.Vec
import SAT.Mios.Clause
import qualified SAT.Mios.ClauseManager as CM
type ClausePool = V.Vector CM.ClauseSimpleManager
storeLimit :: Int
storeLimit = 62
newClausePool ::Int -> IO ClausePool
newClausePool n = V.fromList <$> mapM (\_ -> CM.newManager n) [0 .. storeLimit]
{-# INLINE getManager #-}
getManager :: ClausePool -> Int -> CM.ClauseSimpleManager
getManager p n = V.unsafeIndex p n
{-# INLINABLE makeClauseFromStack #-}
makeClauseFromStack :: ClausePool -> Stack -> IO Clause
makeClauseFromStack pool v = do
let pickup :: Int -> IO Clause
pickup ((<= storeLimit) -> False) = return NullClause
pickup i = do
let mgr = getManager pool i
nn <- get' mgr
if 0 < nn
then do c <- lastOf mgr; popFrom mgr; return c
else pickup $ i + 1
n <- get' v
c <- pickup (n - 2)
if c == NullClause
then newClauseFromStack True v
else do let lstack = lits c
loop :: Int -> IO ()
loop ((<= n) -> False) = set' (activity c) 0.0
loop i = (setNth lstack i =<< getNth v i) >> loop (i + 1)
loop 0
return c
{-# INLINE putBackToPool #-}
putBackToPool :: ClausePool -> Clause -> IO ()
putBackToPool pool c = do
n <- subtract 2 <$> get' c
l <- getRank c
when (0 /= l && n <= storeLimit) $ pushTo (getManager pool n) c