ParseDIMACS.hs

{-
    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 <http://www.gnu.org/licenses/>.

    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 :: [[Integer]]}

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

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