{-# LANGUAGE Safe #-}
module SAT.Mios.Util.DIMACS.Writer
(
toFile
, toDIMACSString
, toString
, toLatexString
)
where
import Data.List (intercalate, nub, sort)
import System.IO
toFile :: FilePath -> [[Int]] -> IO ()
toFile f l = writeFile f $ toDIMACSString l
toDIMACSString :: [[Int]] -> String
toDIMACSString l = hdr ++ str
where
hdr = "p cnf " ++ show numV ++ " " ++ show numC ++ "\n"
numC = length l
numV = last $ nub $ sort $ map abs $ concat l
str = concat [intercalate " " (map show c) ++ " 0\n" | c <- l]
toString :: [[Int]] -> String -> String -> String
toString l and' or' = intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l]
where
lit x
| 0 <= x = "X" ++ show x
| otherwise = "-X" ++ show (abs x)
a = pad and'
o = pad or'
pad s = " " ++ s ++ " "
toLatexString :: [[Int]] -> String
toLatexString l = "\\begin{eqnarray*}\n" ++ intercalate a ["(" ++ intercalate o [ lit x | x <- c] ++ ")" | c <- l] ++ "\n\\end{eqnarray*}"
where
lit x
| 0 <= x = "X_{" ++ show x ++ "}"
| otherwise = "\\overline{X_{" ++ show (abs x) ++ "}}"
a = " \n\\wedge "
o = " \\vee "