{-# LANGUAGE Safe #-}
module SAT.Mios.Util.DIMACS.Reader
(
fromFile
, clauseListFromFile
)
where
import Control.Applicative ((<$>), (<*>), (<*), (*>))
import Data.Char
import Text.ParserCombinators.ReadP
{-# INLINE newline #-}
newline :: ReadP Char
newline = char '\n'
{-# INLINE digit #-}
digit :: ReadP Char
digit = satisfy isDigit
{-# INLINE spaces #-}
spaces :: ReadP String
spaces = munch (`elem` " \t")
{-# INLINE noneOf #-}
noneOf :: Foldable t => t Char -> ReadP Char
noneOf s = satisfy (`notElem` s)
{-# 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 problemLine #-}
problemLine :: ReadP (Int, Int)
problemLine = do
char 'p'
skipSpaces
(string "cnf" <++ string "CNF")
skipSpaces
vars <- pint
skipSpaces
clas <- pint
spaces
newline
return (vars, clas)
{-# INLINE commentLines #-}
commentLines :: ReadP ()
commentLines = do
l <- look
if (head l) == 'c'
then do
munch ('\n' /=)
newline
commentLines
else return ()
_commentLines :: ReadP ()
_commentLines = do
char 'c'
munch ('\n' /=)
newline
l <- look
if (head l) == 'c' then commentLines else return ()
{-# INLINE preambleCNF #-}
preambleCNF :: ReadP (Int, Int)
preambleCNF = do
commentLines
problemLine
{-# INLINE seqNums #-}
seqNums :: ReadP [Int]
seqNums = do
skipSpaces
x <- int
skipSpaces
if (x == 0) then return [] else (x :) <$> seqNums
{-# INLINE parseClauses #-}
parseClauses :: Int -> ReadP [[Int]]
parseClauses n = count n seqNums
{-# INLINE parseCNF #-}
parseCNF :: ReadP ((Int, Int), [[Int]])
parseCNF = do
a <- preambleCNF
b <- parseClauses (snd a)
return (a, b)
driver :: String -> [([[Int]], String)]
driver input = readP_to_S (parseClauses 1) input
{-# INLINE fromFile #-}
fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]]))
fromFile f = do
c <- readFile f
case readP_to_S parseCNF c of
[(a, _)] -> return $ Just a
_ -> return Nothing
clauseListFromFile :: FilePath -> IO [[Int]]
clauseListFromFile l = do
res <- fromFile l
case res of
Just (_, l) -> return l
_ -> return []