module SAT.Mios.Util.DIMACS.Reader
(
fromFile
, clauseListFromFile
)
where
import Control.Applicative ((<$>), (<*>), (<*), (*>))
import Data.Char
import Text.ParserCombinators.ReadP
newline :: ReadP Char
newline = char '\n'
digit :: ReadP Char
digit = satisfy isDigit
spaces :: ReadP String
spaces = munch (`elem` " \t")
noneOf :: Foldable t => t Char -> ReadP Char
noneOf s = satisfy (`notElem` s)
pint :: ReadP Int
pint = do
n <- munch isDigit
return (read n :: Int)
mint :: ReadP Int
mint = do
char '-'
n <- munch isDigit
return ( (read n::Int))
int :: ReadP Int
int = mint <++ pint
problemLine :: ReadP (Int, Int)
problemLine = do
char 'p'
skipSpaces
(string "cnf" <++ string "CNF")
skipSpaces
vars <- pint
skipSpaces
clas <- pint
spaces
newline
return (vars, clas)
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 ()
preambleCNF :: ReadP (Int, Int)
preambleCNF = do
commentLines
problemLine
seqNums :: ReadP [Int]
seqNums = do
skipSpaces
x <- int
skipSpaces
if (x == 0) then return [] else (x :) <$> seqNums
parseClauses :: Int -> ReadP [[Int]]
parseClauses n = count n seqNums
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
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 []