{-# LANGUAGE
RecordWildCards
, ViewPatterns
#-}
{-# LANGUAGE Safe #-}
module SAT.Mios.Validator
(
validate
)
where
import Control.Monad (when)
import Data.Foldable (toList)
import Data.List (sort)
import SAT.Mios.Types
import SAT.Mios.Clause
import SAT.Mios.ClauseManager
import SAT.Mios.Solver
validate :: Traversable t => Solver -> t Int -> IO Bool
validate s t = do
assignment <- newVec (1 + nVars s) (0 :: Int) :: IO (Vec Int)
vec <- getClauseVector (clauses s)
nc <- get' (clauses s)
let
lst = map int2lit $ toList t
inject :: Lit -> IO ()
inject l = setNth assignment (lit2var l) $ lit2lbool l
satisfied :: Lit -> IO Bool
satisfied l
| positiveLit l = (LiftedT ==) <$> getNth assignment (lit2var l)
| otherwise = (LiftedF ==) <$> getNth assignment (lit2var l)
satAny :: [Lit] -> IO Bool
satAny [] = return False
satAny (l:ls) = do
sat' <- satisfied l
if sat' then return True else satAny ls
loopOnVector :: Int -> IO Bool
loopOnVector ((< nc) -> False) = return True
loopOnVector i = do
sat' <- satAny =<< asList =<< getNth vec i
if sat' then loopOnVector (i + 1) else return False
if null lst
then error "validator got an empty assignment."
else mapM_ inject lst >> loopOnVector 0
checkUniqueness :: Solver -> Clause -> IO ()
checkUniqueness Solver{..} c = do
n <- get' learnts
cvec <- getClauseVector learnts
cls <- sort <$> asList c
let
loop :: Int -> IO ()
loop ((< n) -> False) = return ()
loop i = do
c' <- getNth cvec i
cls' <- sort <$> asList c'
when (cls' == cls) $ errorWithoutStackTrace "reinsert a same clause"
loop (i + 1)
loop 0