module Math.SMT.Yices.Pipe (
YicesIPC, ResY(..), createYicesPipe,
runCmdsY', runCmdsY, checkY, exitY, flushY
) where
import Math.SMT.Yices.Syntax
import Math.SMT.Yices.Parser
import List
import Monad
import System.IO
import System.Process
type YicesIPC = (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)
data ResY
= Sat [ExpY]
| UnSat [Int]
| InCon [String]
deriving Show
createYicesPipe :: FilePath -> [String] -> IO YicesIPC
createYicesPipe yPath yOpts = createProcess $
(proc yPath $ "-i":"-e":yOpts){std_in=CreatePipe,std_out=CreatePipe}
_BEGIN_OUTPUT = "_![<[BEGIN_OUTPUT]>]!_"
_END_OUTPUT = "_![<[END_OUTPUT]>]!_"
runCmdStringY yp s = runCmdStringY' yp s >> flushY yp
runCmdStringY' (Just hin, _, _, _) = hPutStrLn hin
runCmdsY :: YicesIPC -> [CmdY] -> IO ()
runCmdsY yp cmds = runCmdsY' yp cmds >> flushY yp
runCmdsY' :: YicesIPC -> [CmdY] -> IO ()
runCmdsY' (Just hin, _, _, _) = mapM_ (hPutStrLn hin . show)
exitY :: YicesIPC -> IO ()
exitY (Just hin, _, _, _) = hPutStrLn hin (show EXIT) >> hFlush hin
flushY :: YicesIPC -> IO ()
flushY (Just hin, _, _, _) = hFlush hin
checkY :: YicesIPC -> IO ResY
checkY yp@(_, Just hout, _, _) =
do runCmdsY yp [ECHO('\n':_BEGIN_OUTPUT), CHECK, ECHO('\n':_END_OUTPUT)]
(s:ss) <- hGetOutLines hout
return $
case s of
"sat" -> Sat (map parseExpY ss)
"unsat" -> UnSat (map read.words.tail.dropWhile (/=':').head $ ss)
_ -> InCon (s:ss)
stripYicesPrompt line | yprompt `isPrefixOf` line = drop (length yprompt) line
| otherwise = line
where yprompt = "yices > "
hGetOutLines h = liftM ( filter (not . null) . map stripYicesPrompt .
tail . dropWhile (/=_BEGIN_OUTPUT) )
(hGetLinesWhile (/= _END_OUTPUT) h)
hGetLinesWhile p h = do line <- hGetLine h
if p line
then liftM (line:) (hGetLinesWhile p h)
else return []
hGetReadyString1 h = liftM2 (:) (hGetChar h) (hGetReadyString h)
hGetReadyString h =
do ready <- hReady h
if ready then liftM2 (:) (hGetChar h) (hGetReadyString h) else return []