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"
            -- print fm
            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