{-# LANGUAGE Safe #-}
module SAT.Mios.Util.DIMACS.MinisatReader
(
fromMinisatOutput
, clauseListFromMinisatOutput
)
where
import Data.Char
import Text.ParserCombinators.ReadP
{-# INLINE pint #-}
pint :: ReadP Int
pint = do
n <- munch isDigit
return (read n :: Int)
{-# INLINE mint #-}
mint :: ReadP Int
mint = do
char '-'
n <- munch isDigit
return (- (read n::Int))
{-# INLINE int #-}
int :: ReadP Int
int = mint <++ pint
{-# INLINE seqNums #-}
seqNums :: ReadP [Int]
seqNums = do
skipSpaces
x <- int
skipSpaces
if x == 0 then return [] else (x :) <$> seqNums
{-# INLINE parseMinisatOutput #-}
parseMinisatOutput :: ReadP ((Int, Int), [Int])
parseMinisatOutput = do
string "SAT"
skipSpaces
l <- seqNums
return ((length l,0), l)
{-# INLINE fromMinisatOutput #-}
fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int]))
fromMinisatOutput f = do
c <- readFile f
case readP_to_S parseMinisatOutput c of
[(a, _)] -> return $ Just a
_ -> return Nothing
clauseListFromMinisatOutput :: FilePath -> IO [Int]
clauseListFromMinisatOutput l = do
res <- fromMinisatOutput l
case res of
Just p -> return (snd p)
_ -> return []