module ToySolver.Text.QDimacs
( QDimacs (..)
, Quantifier (..)
, QuantSet
, Atom
, Lit
, Clause
, parseFile
, parseByteString
) where
import Control.DeepSeq
import qualified Data.ByteString.Lazy.Char8 as BL
import Data.Char
data QDimacs
= QDimacs
{ numVars :: !Int
, numClauses :: !Int
, prefix :: [QuantSet]
, matrix :: [Clause]
}
deriving (Eq, Ord, Show, Read)
data Quantifier
= E
| A
deriving (Eq, Ord, Show, Read, Enum, Bounded)
type QuantSet = (Quantifier, [Atom])
type Atom = Int
type Lit = Int
type Clause = [Lit]
parseFile :: FilePath -> IO (Either String QDimacs)
parseFile filename = do
s <- BL.readFile filename
return $ parseByteString s
parseByteString :: BL.ByteString -> (Either String QDimacs)
parseByteString = f . BL.lines
where
f [] = Left "QDimacs.parseByteString: premature end of file"
f (l : ls) =
case BL.uncons l of
Nothing -> Left "QDimacs.parseByteString: no problem line"
Just ('c', _) -> f ls
Just ('p', s) ->
case BL.words s of
["cnf", numVars', numClauses'] ->
case parsePrefix ls of
(prefix', ls') -> Right $
QDimacs
{ numVars = read $ BL.unpack numVars'
, numClauses = read $ BL.unpack numClauses'
, prefix = prefix'
, matrix = parseClauses ls'
}
_ -> Left "QDimacs.parseByteString: invalid problem line"
Just (c, _) -> Left ("QDimacs.parseByteString: invalid prefix " ++ show c)
parsePrefix :: [BL.ByteString] -> ([QuantSet], [BL.ByteString])
parsePrefix = go []
where
go result [] = (reverse result, [])
go result lls@(l : ls) =
case BL.uncons l of
Just (c,s)
| c=='a' || c=='e' ->
let atoms = readInts s
q = if c=='a' then A else E
in seq q $ deepseq atoms $ go ((q, atoms) : result) ls
| otherwise ->
(reverse result, lls)
_ -> error "QDimacs.parseProblem: invalid line"
parseClauses :: [BL.ByteString] -> [Clause]
parseClauses = map readInts
readInts :: BL.ByteString -> [Int]
readInts s =
case BL.readInt (BL.dropWhile isSpace s) of
Just (z, s') -> if z == 0 then [] else z : readInts s'
Nothing -> []