{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
module ToySolver.FileFormat.CNF
(
module ToySolver.FileFormat.Base
, CNF (..)
, WCNF (..)
, WeightedClause
, Weight
, GCNF (..)
, GroupIndex
, GClause
, QDimacs (..)
, Quantifier (..)
, QuantSet
, Atom
, Lit
, Clause
, PackedClause
, packClause
, unpackClause
) where
import Prelude hiding (readFile, writeFile)
import Control.DeepSeq
import qualified Data.ByteString.Lazy.Char8 as BS
import Data.ByteString.Builder
import Data.Char
#if !MIN_VERSION_base(4,11,0)
import Data.Monoid
#endif
import ToySolver.FileFormat.Base
import qualified ToySolver.SAT.Types as SAT
import ToySolver.SAT.Types (Lit, Clause, PackedClause, packClause, unpackClause)
data CNF
= CNF
{ cnfNumVars :: !Int
, cnfNumClauses :: !Int
, cnfClauses :: [SAT.PackedClause]
}
deriving (Eq, Ord, Show, Read)
instance FileFormat CNF where
parse s =
case BS.words l of
(["p","cnf", nvar, nclause]) ->
Right $
CNF
{ cnfNumVars = read $ BS.unpack nvar
, cnfNumClauses = read $ BS.unpack nclause
, cnfClauses = map parseClauseBS ls
}
_ ->
Left "cannot find cnf header"
where
l :: BS.ByteString
ls :: [BS.ByteString]
(l:ls) = filter (not . isCommentBS) (BS.lines s)
render cnf = header <> mconcat (map f (cnfClauses cnf))
where
header = mconcat
[ byteString "p cnf "
, intDec (cnfNumVars cnf), char7 ' '
, intDec (cnfNumClauses cnf), char7 '\n'
]
f c = mconcat [intDec lit <> char7 ' '| lit <- SAT.unpackClause c] <> byteString "0\n"
readInts :: BS.ByteString -> [Int]
readInts s =
case BS.readInt (BS.dropWhile isSpace s) of
Just (0,_) -> []
Just (z,s') -> z : readInts s'
Nothing -> error "ToySolver.FileFormat.CNF.readInts: 0 is missing"
parseClauseBS :: BS.ByteString -> SAT.PackedClause
parseClauseBS = SAT.packClause . readInts
isCommentBS :: BS.ByteString -> Bool
isCommentBS s =
case BS.uncons s of
Just ('c',_) -> True
_ -> False
data WCNF
= WCNF
{ wcnfNumVars :: !Int
, wcnfNumClauses :: !Int
, wcnfTopCost :: !Weight
, wcnfClauses :: [WeightedClause]
}
deriving (Eq, Ord, Show, Read)
type WeightedClause = (Weight, SAT.PackedClause)
type Weight = Integer
instance FileFormat WCNF where
parse s =
case BS.words l of
(["p","wcnf", nvar, nclause, top]) ->
Right $
WCNF
{ wcnfNumVars = read $ BS.unpack nvar
, wcnfNumClauses = read $ BS.unpack nclause
, wcnfTopCost = read $ BS.unpack top
, wcnfClauses = map parseWCNFLineBS ls
}
(["p","wcnf", nvar, nclause]) ->
Right $
WCNF
{ wcnfNumVars = read $ BS.unpack nvar
, wcnfNumClauses = read $ BS.unpack nclause
, wcnfTopCost = fromInteger $ 2^(63::Int) - 1
, wcnfClauses = map parseWCNFLineBS ls
}
(["p","cnf", nvar, nclause]) ->
Right $
WCNF
{ wcnfNumVars = read $ BS.unpack nvar
, wcnfNumClauses = read $ BS.unpack nclause
, wcnfTopCost = fromInteger $ 2^(63::Int) - 1
, wcnfClauses = map ((\c -> seq c (1,c)) . parseClauseBS) ls
}
_ ->
Left "cannot find wcnf/cnf header"
where
l :: BS.ByteString
ls :: [BS.ByteString]
(l:ls) = filter (not . isCommentBS) (BS.lines s)
render wcnf = header <> mconcat (map f (wcnfClauses wcnf))
where
header = mconcat
[ byteString "p wcnf "
, intDec (wcnfNumVars wcnf), char7 ' '
, intDec (wcnfNumClauses wcnf), char7 ' '
, integerDec (wcnfTopCost wcnf), char7 '\n'
]
f (w,c) = integerDec w <> mconcat [char7 ' ' <> intDec lit | lit <- SAT.unpackClause c] <> byteString " 0\n"
parseWCNFLineBS :: BS.ByteString -> WeightedClause
parseWCNFLineBS s =
case BS.readInteger (BS.dropWhile isSpace s) of
Nothing -> error "ToySolver.FileFormat.CNF: no weight"
Just (w, s') -> seq w $ seq xs $ (w, xs)
where
xs = parseClauseBS s'
data GCNF
= GCNF
{ gcnfNumVars :: !Int
, gcnfNumClauses :: !Int
, gcnfLastGroupIndex :: !GroupIndex
, gcnfClauses :: [GClause]
}
deriving (Eq, Ord, Show, Read)
type GroupIndex = Int
type GClause = (GroupIndex, SAT.PackedClause)
instance FileFormat GCNF where
parse s =
case BS.words l of
(["p","gcnf", nbvar', nbclauses', lastGroupIndex']) ->
Right $
GCNF
{ gcnfNumVars = read $ BS.unpack nbvar'
, gcnfNumClauses = read $ BS.unpack nbclauses'
, gcnfLastGroupIndex = read $ BS.unpack lastGroupIndex'
, gcnfClauses = map parseGCNFLineBS ls
}
(["p","cnf", nbvar', nbclause']) ->
Right $
GCNF
{ gcnfNumVars = read $ BS.unpack nbvar'
, gcnfNumClauses = read $ BS.unpack nbclause'
, gcnfLastGroupIndex = read $ BS.unpack nbclause'
, gcnfClauses = zip [1..] $ map parseClauseBS ls
}
_ ->
Left "cannot find gcnf header"
where
l :: BS.ByteString
ls :: [BS.ByteString]
(l:ls) = filter (not . isCommentBS) (BS.lines s)
render gcnf = header <> mconcat (map f (gcnfClauses gcnf))
where
header = mconcat
[ byteString "p gcnf "
, intDec (gcnfNumVars gcnf), char7 ' '
, intDec (gcnfNumClauses gcnf), char7 ' '
, intDec (gcnfLastGroupIndex gcnf), char7 '\n'
]
f (idx,c) = char7 '{' <> intDec idx <> char7 '}' <>
mconcat [char7 ' ' <> intDec lit | lit <- SAT.unpackClause c] <>
byteString " 0\n"
parseGCNFLineBS :: BS.ByteString -> GClause
parseGCNFLineBS s
| Just ('{', s1) <- BS.uncons (BS.dropWhile isSpace s)
, Just (!idx,s2) <- BS.readInt s1
, Just ('}', s3) <- BS.uncons s2 =
let ys = parseClauseBS s3
in seq ys $ (idx, ys)
| otherwise = error "ToySolver.FileFormat.CNF: parse error"
data QDimacs
= QDimacs
{ qdimacsNumVars :: !Int
, qdimacsNumClauses :: !Int
, qdimacsPrefix :: [QuantSet]
, qdimacsMatrix :: [SAT.PackedClause]
}
deriving (Eq, Ord, Show, Read)
data Quantifier
= E
| A
deriving (Eq, Ord, Show, Read, Enum, Bounded)
type QuantSet = (Quantifier, [Atom])
type Atom = SAT.Var
instance FileFormat QDimacs where
parse = f . BS.lines
where
f [] = Left "ToySolver.FileFormat.CNF.parse: premature end of file"
f (l : ls) =
case BS.uncons l of
Nothing -> Left "ToySolver.FileFormat.CNF.parse: no problem line"
Just ('c', _) -> f ls
Just ('p', s) ->
case BS.words s of
["cnf", numVars', numClauses'] ->
case parsePrefix ls of
(prefix', ls') -> Right $
QDimacs
{ qdimacsNumVars = read $ BS.unpack numVars'
, qdimacsNumClauses = read $ BS.unpack numClauses'
, qdimacsPrefix = prefix'
, qdimacsMatrix = map parseClauseBS ls'
}
_ -> Left "ToySolver.FileFormat.CNF.parse: invalid problem line"
Just (c, _) -> Left ("ToySolver.FileFormat.CNF.parse: invalid prefix " ++ show c)
render qdimacs = problem_line <> prefix' <> mconcat (map f (qdimacsMatrix qdimacs))
where
problem_line = mconcat
[ byteString "p cnf "
, intDec (qdimacsNumVars qdimacs), char7 ' '
, intDec (qdimacsNumClauses qdimacs), char7 '\n'
]
prefix' = mconcat
[ char7 (if q == E then 'e' else 'a') <> mconcat [char7 ' ' <> intDec atom | atom <- atoms] <> byteString " 0\n"
| (q, atoms) <- qdimacsPrefix qdimacs
]
f c = mconcat [intDec lit <> char7 ' '| lit <- SAT.unpackClause c] <> byteString "0\n"
parsePrefix :: [BS.ByteString] -> ([QuantSet], [BS.ByteString])
parsePrefix = go []
where
go result [] = (reverse result, [])
go result lls@(l : ls) =
case BS.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 "ToySolver.FileFormat.CNF.parseProblem: invalid line"