module SAT.Mios.Util.DIMACS.MinisatReader
(
fromMinisatOutput
, clauseListFromMinisatOutput
)
where
import Data.Char
import Text.ParserCombinators.ReadP
pint = do
n <- munch isDigit
return (read n :: Int)
mint = do
char '-'
n <- munch isDigit
return ( (read n::Int))
int = mint <++ pint
seqNums = do
skipSpaces
x <- int
skipSpaces
if (x == 0) then return [] else (x :) <$> seqNums
parseMinisatOutput :: ReadP ((Int, Int), [Int])
parseMinisatOutput = do
string "SAT"
skipSpaces
l <- seqNums
return ((length l,0), l)
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 []