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]
getManager :: ClausePool -> Int -> CM.ClauseSimpleManager
getManager p n = V.unsafeIndex p n
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) = return ()
loop i = (setNth lstack i =<< getNth v i) >> loop (i + 1)
loop 0
set' (activity c) 0.0
return c
putBackToPool :: ClausePool -> Clause -> IO ()
putBackToPool pool c = do
l <- get' (rank c)
when (0 /= l) $ do let n = realLengthOfStack (lits c) 3
when (n <= storeLimit) $ pushTo (getManager pool n) c