module ToySolver.Text.CNF
(
CNF (..)
, parseFile
, parseByteString
, writeFile
, hPutCNF
, cnfBuilder
) where
import Prelude hiding (writeFile)
import qualified Data.ByteString.Lazy.Char8 as BS
import Data.ByteString.Builder
import Data.Char
import Data.Monoid
import System.IO hiding (writeFile)
import qualified ToySolver.SAT.Types as SAT
data CNF
= CNF
{ numVars :: !Int
, numClauses :: !Int
, clauses :: [SAT.Clause]
}
deriving (Show, Eq, Ord)
parseFile :: FilePath -> IO (Either String CNF)
parseFile filename = do
s <- BS.readFile filename
return $ parseByteString s
parseByteString :: BS.ByteString -> Either String CNF
parseByteString s =
case BS.words l of
(["p","cnf", nvar, nclause]) ->
Right $
CNF
{ numVars = read $ BS.unpack nvar
, numClauses = read $ BS.unpack nclause
, clauses = map parseClauseBS ls
}
_ ->
Left "cannot find cnf header"
where
l :: BS.ByteString
ls :: [BS.ByteString]
(l:ls) = filter (not . isCommentBS) (BS.lines s)
parseClauseBS :: BS.ByteString -> SAT.Clause
parseClauseBS s = seqList xs $ xs
where
xs = go s
go s =
case BS.readInt (BS.dropWhile isSpace s) of
Nothing -> error "ToySolver.Text.MaxSAT: parse error"
Just (0,_) -> []
Just (i,s') -> i : go s'
isCommentBS :: BS.ByteString -> Bool
isCommentBS s =
case BS.uncons s of
Just ('c',_) -> True
_ -> False
seqList :: [a] -> b -> b
seqList [] b = b
seqList (x:xs) b = seq x $ seqList xs b
writeFile :: FilePath -> CNF -> IO ()
writeFile filepath cnf = do
withBinaryFile filepath WriteMode $ \h -> do
hSetBuffering h (BlockBuffering Nothing)
hPutBuilder h (cnfBuilder cnf)
cnfBuilder :: CNF -> Builder
cnfBuilder cnf = header <> mconcat (map f (clauses cnf))
where
header = mconcat
[ byteString "p cnf "
, intDec (numVars cnf), char7 ' '
, intDec (numClauses cnf), char7 '\n'
]
f c = mconcat [intDec lit <> char7 ' '| lit <- c] <> byteString "0\n"
hPutCNF :: Handle -> CNF -> IO ()
hPutCNF h cnf = hPutBuilder h (cnfBuilder cnf)