{-
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU Lesser General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public License
along with this program. If not, see .
Copyright 2008 Denis Bueno
-}
-- | A simple Parsec module for parsing CNF files in DIMACS format.
module Language.CNF.Parse.ParseDIMACS
( parseCNF, CNF(..) ) where
import Text.ParserCombinators.Parsec
data CNF = CNF {numVars :: Int
,numClauses :: Int
,clauses :: [[Int]]}
deriving Show
parseCNF :: String -- ^ The filename. Used to report errors.
-> String -- ^ The contents of the CNF file.
-> CNF
parseCNF title input =
case parse cnf title input of
Left parseError -> error $ "Parse error: " ++ show parseError
Right cs -> cs
-- A DIMACS CNF file contains a header of the form "p cnf
-- " and then a bunch of 0-terminated clauses.
cnf :: Parser CNF
cnf =
do many comment
char 'p' ; spaces
string "cnf" ; spaces
numVars <- many1 digit ; spaces
numClauses <- many1 digit
space `manyTill` newline
actualClauses <- many1 clause
return $ CNF (read numVars) (read numClauses) actualClauses
comment :: Parser String
comment = do char 'c' ; manyTill anyChar (try newline)
clause :: Parser [Int]
clause = do many (space <|> newline)
lits <- between (string "") (char '0') (many1 intSpaces)
many (space <|> newline)
return lits
-- Consume all whitespace after the int so the `between' in `clause' matches
-- on "0" at the end.
intSpaces = do i <- int
many1 (space <|> newline)
return i
int :: Parser Int
int = do parity <- option '+' $ choice $ map char "+-"
first <- posDigit
rest <- many digit
return . read $
case parity of
'+' -> first : rest
'-' -> '-' : first : rest
_ -> error $ "unknown parity syntax: " ++ [parity]
posDigit :: Parser Char
posDigit = oneOf ['1'..'9']