module Satchmo.Solve
( solve
, Decoder
)
where
import Satchmo.Data
import Satchmo.Code
import Satchmo.Internal
import Data.Map ( Map )
import qualified Data.Map as M
import Control.Monad.State
import Control.Monad.Reader
import System.Process
solve :: SAT ( Decoder a )
-> IO ( Maybe a )
solve build = do
let (s, a) = sat build
mfm <- run s
case mfm of
Nothing -> do
putStrLn "not satisfiable"
return Nothing
Just fm -> do
putStrLn "satisfiable"
return $ Just $ runReader a fm
run :: String -> IO ( Maybe ( Map Literal Bool ) )
run cs = do
let debug = False
if debug
then putStrLn cs
else putStrLn $ head $ lines cs
( code, stdout, stderr ) <-
readProcessWithExitCode "minisat" [ "/dev/stdin", "/dev/stdout" ] cs
when debug $ putStrLn stdout
case lines stdout of
"SAT" : xs : _ -> return $ Just $ M.fromList $ do
x <- takeWhile ( /= 0 ) $ map read $ words xs
let l = literal $ abs x
return ( l, x > 0 )
_ -> return $ Nothing