module Language.CNF.Parse.ParseDIMACS
(parseCNF, CNF(..)) where
import Text.ParserCombinators.Parsec
data CNF = CNF {numVars :: Int
,numClauses :: Int
,clauses :: [[Integer]]}
parseCNF :: String
-> String
-> CNF
parseCNF title input =
case parse cnf title input of
Left parseError -> error $ "Parse error: " ++ show parseError
Right cs -> cs
cnf :: Parser CNF
cnf =
do skipComments
char 'p'
spaces
string "cnf"
spaces
numVars <- many1 digit
spaces
numClauses <- many1 digit
manyTill space (try newline)
actualClauses <- manyClause
return $ CNF (read numVars) (read numClauses) (actualClauses)
skipComments :: Parser ()
skipComments =
do try (do char 'c'
_ <- manyTill anyChar (try (char '\n'))
skipComments)
<|> return ()
int :: Parser Integer
int = do parity <- option '+' $ choice $ map char "+-"
first <- nonZeroDigit
rest <- many digit
return . read $
case parity of
'+' -> first : rest
'-' -> '-' : first : rest
_ -> error $ "unknown parity syntax: " ++ [parity]
nonZeroDigit :: Parser Char
nonZeroDigit = oneOf ['1'..'9']
intSpaces = do i <- int
spaces
return i
clause :: Parser [Integer]
clause =
do spaces
lits <- between (string "") (char '0') (many1 intSpaces)
newline
return $ lits
manyClause :: Parser [[Integer]]
manyClause = many1 clause