{-# language PatternSignatures #-}

module Satchmo.Solver.Minisat 

( solve
, using
)

where

import Satchmo.Data
import qualified Satchmo.Solve
import Satchmo.Solver.Internal
import Satchmo.SAT.Seq

import qualified Data.ByteString.Char8 as BS
-- import qualified Data.ByteString.Lazy.Char8 as BS

import Data.Monoid
import System.IO 
import System.Process
import Control.Monad ( when )
import Control.Concurrent
import Control.Exception

import System.TimeIt
import Text.Printf

-- import qualified Data.Map as M
import qualified Data.Array as A

solve = using "minisat2"

using fp = Satchmo.Solve.solve $ minisat fp

minisat :: FilePath -> Satchmo.Solve.Implementation
minisat fp cs Header{numVars=numVars, numClauses=numClauses} = do
    let header = BS.pack $ mkDimacsHeader numVars numClauses
    
    let debug = False
    when debug $ do
        BS.hPutStrLn stderr header
        BS.hPutStrLn stderr cs

    ( hin, hout, herr, proc ) <- runInteractiveCommand
           ( unwords [ fp, "/dev/stdin", "/dev/stdout" ] )
    
    container <- newEmptyMVar

    streamer <- forkIO $ do
        BS.hPutStr hin ( mappend header cs )
        -- waitForProcess proc
        ds <- hGetContents hout
        hPutStrLn stderr $ unwords [ "output", "length", show (length ds) ]
        hPutStrLn stderr $ take 80 ds
        putMVar container ds

    out <- takeMVar container `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do 
        -- hPutStrLn stderr "got exception in waitForProcess"
        killThread streamer
        terminateProcess proc
        -- hPutStrLn stderr "terminateProcess done"
        return ""
    -- hPutStrLn stderr "end waitForProcess"

    case lines out of
        "SAT" : xs : _ -> do
           let dict = Just $ A.listArray (1,numVars) $ do
                            (v,l) <- zip [1..] $ map read $ takeWhile ( /= "0" ) $ words xs
                            return $ if variable l == v then  positive l else error "huh"
           seq (length out) $ return dict
        _ -> return $ Nothing


timeItMsg msg action = do 
    (time, res) <- timeItT action
    hPrintf stderr "CPU time: %6.2fs for %s\n" time msg    
    hFlush stderr 
    return res