module ToySolver.Text.GCNF
(
GCNF (..)
, GroupIndex
, GClause
, parseByteString
, parseFile
, writeFile
, hPutGCNF
, gcnfBuilder
) where
import Prelude hiding (writeFile)
import qualified Data.ByteString.Lazy.Char8 as BS
import Data.ByteString.Builder
import Data.Char
import Data.Monoid
import qualified ToySolver.SAT.Types as SAT
import System.IO hiding (writeFile)
import ToySolver.Internal.TextUtil
data GCNF
= GCNF
{ numVars :: !Int
, numClauses :: !Int
, lastGroupIndex :: !GroupIndex
, clauses :: [GClause]
}
type GroupIndex = Int
type GClause = (GroupIndex, SAT.Clause)
parseFile :: FilePath -> IO (Either String GCNF)
parseFile filename = do
s <- BS.readFile filename
return $ parseByteString s
parseByteString :: BS.ByteString -> Either String GCNF
parseByteString s =
case BS.words l of
(["p","gcnf", nbvar', nbclauses', lastGroupIndex']) ->
Right $
GCNF
{ numVars = read $ BS.unpack nbvar'
, numClauses = read $ BS.unpack nbclauses'
, lastGroupIndex = read $ BS.unpack lastGroupIndex'
, clauses = map parseLineBS ls
}
(["p","cnf", nbvar', nbclause']) ->
Right $
GCNF
{ numVars = read $ BS.unpack nbvar'
, numClauses = read $ BS.unpack nbclause'
, lastGroupIndex = read $ BS.unpack nbclause'
, clauses = zip [1..] $ map parseCNFLineBS ls
}
_ ->
Left "cannot find gcnf header"
where
l :: BS.ByteString
ls :: [BS.ByteString]
(l:ls) = filter (not . isCommentBS) (BS.lines s)
parseLineBS :: BS.ByteString -> GClause
parseLineBS s =
case BS.uncons (BS.dropWhile isSpace s) of
Just ('{', s1) ->
case BS.readInt s1 of
Just (idx,s2) | Just ('}', s3) <- BS.uncons s2 ->
let ys = parseClauseBS s3
in seq idx $ seqList ys $ (idx, ys)
_ -> error "ToySolver.Text.GCNF: parse error"
_ -> error "ToySolver.Text.GCNF: parse error"
parseCNFLineBS :: BS.ByteString -> SAT.Clause
parseCNFLineBS s = seq xs $ seqList xs $ xs
where
xs = parseClauseBS 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.GCNF: 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 -> GCNF -> IO ()
writeFile filepath gcnf = do
withBinaryFile filepath WriteMode $ \h -> do
hSetBuffering h (BlockBuffering Nothing)
hPutGCNF h gcnf
gcnfBuilder :: GCNF -> Builder
gcnfBuilder gcnf = header <> mconcat (map f (clauses gcnf))
where
header = mconcat
[ byteString "p gcnf "
, intDec (numVars gcnf), char7 ' '
, intDec (numClauses gcnf), char7 ' '
, intDec (lastGroupIndex gcnf), char7 '\n'
]
f (idx,c) = char7 '{' <> intDec idx <> char7 '}' <>
mconcat [char7 ' ' <> intDec lit | lit <- c] <>
byteString " 0\n"
hPutGCNF :: Handle -> GCNF -> IO ()
hPutGCNF h gcnf = hPutBuilder h (gcnfBuilder gcnf)