Minisat.hs

{-# language PatternSignatures #-}

module Satchmo.Solver.Minisat 

( solve
, using
)

where

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

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

import Data.Monoid
import System.IO (stderr, hFlush, hClose, hPutStrLn, hGetContents
       , hSetBuffering, BufferMode (..) )
import System.Process
import Control.Monad ( when )
import Control.Concurrent
import Control.Exception
import qualified Control.Exception as C

import qualified Data.Map as M

solve = using "/usr/bin/minisat2"

using fp = Satchmo.Solve.solve $ minisat fp

minisat :: FilePath -> Satchmo.Solve.Implementation
minisat fp cs Header{numVars=numVars, numClauses=numClauses} = do
    let header = mkDimacsHeader numVars numClauses
        cs'    = BS.pack header `mappend` cs
    let debug = False
    if debug
       then BS.hPut stderr cs'
       else hPutStrLn stderr header >> hFlush stderr

-- copied from
-- http://hackage.haskell.org/packages/archive/process/1.0.1.5/doc/html/src/System-Process.html#readProcessWithExitCode

    ( Just inh, Just outh, Just errh, pid ) <- 
       createProcess ( proc fp  [ "/dev/stdin", "/dev/stdout" ] )
           { std_in  = CreatePipe, std_out = CreatePipe, std_err = CreatePipe }

    outMVar <- newEmptyMVar

    -- fork off a thread to start consuming stdout
    out  <- hGetContents outh
    _ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()

    -- fork off a thread to start consuming stderr
    err  <- hGetContents errh
    _ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()

    -- now write and flush any input
    do BS.hPut  inh cs'; hFlush inh ; hClose inh -- done with stdin

    -- wait on the output
    takeMVar outMVar `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do 
        terminateProcess pid
    takeMVar outMVar `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do 
        terminateProcess pid
    hClose outh ; hClose errh

    -- wait on the process
    ex <- waitForProcess pid

    hPutStrLn stderr $ unwords [ "output", "length", show ( length out ) ]
    -- hPutStrLn stderr out

    case lines out of
        "SAT" : xs : _ -> do
           let dict = Just $ M.fromList $ do
                            l <- map read $ takeWhile ( /= "0" ) $ words xs
                            return ( variable l, positive l )
           when debug $ print dict
           return dict
        _ -> return $ Nothing