{-# language PatternSignatures #-}

-- | textual interface to Precosat/Picosat solver,
-- cf. http://fmv.jku.at/precosat/

module Satchmo.Solver.Pcosat

( solve
, using
)

where

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

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

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

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

solve = using "precosat"

using fp = Satchmo.Solve.solve $ pcosat fp

debug :: Bool
debug = False

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

    ( hin, hout, herr, proc ) <- 
        System.Process.runInteractiveCommand
            $ unwords [ fp ] 

    container <- newEmptyMVar
    forkIO $ do 
        -- hPutStrLn stderr "before hPut"
        BS.hPut hin cs'
        -- waitForProcess proc
        -- hPutStrLn stderr "before hGetContents"
        ds <- hGetContents hout
        hPutStrLn stderr $ unwords [ "output", "length", show ( length ds ) ]
        putMVar container ds

    out <- takeMVar container 
        `Control.Exception.catch` \ ( _ :: AsyncException ) ->  do 
            -- hPutStrLn stderr "caught exception"
            terminateProcess proc
            return ""

    when debug $ hPutStrLn stdout out
    let core = filter ( \ cs -> take 1 cs /= "c" ) $ lines out

{-
        assign = M.fromList $ do
                'v' : xs <- core
                l <- map read $ takeWhile ( /= "0" ) $ words xs
                return ( variable l, positive l )
-}

        assign = A.array (1, numVars) $ do
                'v' : xs <- core
                l <- map read $ takeWhile ( /= "0" ) $ words xs
                return ( variable l, positive l )
            

        status = filter ( \ cs -> take 1 cs == "s" ) $ lines out
    case status of
        "s SATISFIABLE" : post  -> do
            when debug $ hPutStrLn stderr $ show assign
            return $ Just assign
        _ -> do
            return $ Nothing