{-# language PatternSignatures #-}

-- | http://www.cs.uni-potsdam.de/clasp/

module Satchmo.Solver.Clasp

( 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.Char8 as S
import qualified Data.ByteString.Lazy.Char8 as BS
-- import qualified Data.ByteString.Lazy as BS

import qualified Data.Map as M

solve = using "clasp"

using fp = Satchmo.Solve.solve $ clasp fp

clasp :: FilePath -> Satchmo.Solve.Implementation
clasp fp cs Header{numVars=numVars, numClauses=numClauses}   = do
    let header = mkDimacsHeader numVars numClauses
        cs'    = BS.pack ( header ++ "\n" ) `mappend` cs
    let debug = False
    if debug 
       then BS.hPut stderr cs'
       else hPutStrLn stderr header 

    ( hin, hout, herr, proc ) <- 
        System.Process.runInteractiveCommand
            $ unwords [ fp, "--dimacs",  "--number=1",  "--sat-p=20,25,150"
                      , "--hParam=0,512"  ] 

    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 
        assign = M.fromList $ do
                'v' : xs <- lines out
                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
            return $ Just assign
        _ -> do
            return $ Nothing