module Text.MaxSAT
(
WCNF (..)
, WeightedClause
, Weight
, parseWCNFString
, parseWCNFFile
) where
import qualified SAT.Types as SAT
import Text.Util
data WCNF
= WCNF
{ numVars :: !Int
, numClauses :: !Int
, topCost :: !Weight
, clauses :: [WeightedClause]
}
type WeightedClause = (Weight, SAT.Clause)
type Weight = Integer
parseWCNFString :: String -> Either String WCNF
parseWCNFString s =
case words l of
(["p","wcnf", nvar, nclause, top]) ->
Right $
WCNF
{ numVars = read nvar
, numClauses = read nclause
, topCost = read top
, clauses = map parseWCNFLine ls
}
(["p","wcnf", nvar, nclause]) ->
Right $
WCNF
{ numVars = read nvar
, numClauses = read nclause
, topCost = 2^(63::Int)
, clauses = map parseWCNFLine ls
}
(["p","cnf", nvar, nclause]) ->
Right $
WCNF
{ numVars = read nvar
, numClauses = read nclause
, topCost = 2
, clauses = map parseCNFLine ls
}
_ ->
Left "cannot find wcnf/cnf header"
where
(l:ls) = filter (not . isComment) (lines s)
parseWCNFFile :: FilePath -> IO (Either String WCNF)
parseWCNFFile filename = do
s <- readFile filename
return $ parseWCNFString s
isComment :: String -> Bool
isComment ('c':_) = True
isComment _ = False
parseWCNFLine :: String -> WeightedClause
parseWCNFLine s =
case words s of
(w:xs) ->
let w' = readUnsignedInteger w
ys = map readInt $ init xs
in seq w' $ seqList ys $ (w', ys)
_ -> error "parse error"
parseCNFLine :: String -> WeightedClause
parseCNFLine s = seq xs $ seqList xs $ (1, xs)
where
xs = init (map readInt (words s))
seqList :: [a] -> b -> b
seqList [] b = b
seqList (x:xs) b = seq x $ seqList xs b