module SAT.Solver.Mios.Glucose
(
computeLBD
, lbdOf
, setLBD
, updateLBD
, nextReduction
)
where
import Control.Monad (when)
import SAT.Solver.Mios.Types
import SAT.Solver.Mios.Clause
import SAT.Solver.Mios.Solver
computeLBD :: Solver -> Vec -> IO Int
computeLBD Solver{..} vec = do
key <- (1 +) <$> getInt lbd'key
setInt lbd'key key
nv <- getNth vec 0
let
loop :: Int -> Int -> IO Int
loop ((<= nv) -> False) n = return n
loop !i !n = do
l <- getNth level . lit2var =<< getNth vec i
seen <- if l == 0 then return True else (key ==) <$> getNth lbd'seen l
if seen
then loop (i + 1) n
else setNth lbd'seen l key >> loop (i + 1) (n + 1)
loop 1 0
lbdOf :: Solver -> Clause -> IO Int
lbdOf s (lits -> v) = computeLBD s v
setLBD :: Solver -> Clause -> IO ()
setLBD s c = setInt (lbd c) =<< lbdOf s c
updateLBD :: Solver -> Clause -> IO ()
updateLBD _ NullClause = error "LBD71"
updateLBD _ (learnt -> False) = return ()
updateLBD s c@Clause{..} = setInt lbd =<< lbdOf s c
nextReduction :: Int -> Int -> Int
nextReduction b n = b + 300 * n