yices- Haskell programming interface to Yices SMT solver

MaintainerAhn, Ki Yung <kya@pdx.edu>
Safe HaskellSafe-Infered



Inter-process communication to Yices through pipe.



type YicesIPC = (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)Source

type abbrevation for IPC handle quadruple

data ResY Source

To read in the result of the (check) command


Sat [ExpY] 
Unknown [ExpY] 
UnSat [Integer] 
InCon [String] 


createYicesPipe :: FilePath -> [String] -> IO YicesIPCSource

Start yices on a given path with given options. The first argumnet yPath is the path binary file of yices (e.g. homekyagrdyices-1.0.21bin/yices). By default -i and -e options are already present, and yOpts argument appens more options

runCmdsY' :: YicesIPC -> [CmdY] -> IO ()Source

send yices commands without flushing

runCmdsY :: YicesIPC -> [CmdY] -> IO ()Source

send yices commands and flush

checkY :: YicesIPC -> IO ResYSource

send check command and reads the result

exitY :: YicesIPC -> IO ()Source

send exit command and flush

flushY :: YicesIPC -> IO ()Source

flush the input pipe to yices (needed after actions like runCmdsY')

quickCheckY :: String -> [String] -> [CmdY] -> IO ResYSource

sends a bunch of commands followed by a check command and reads the resulting model. This function should be the preferred option when large expressions are involved.

quickCheckY' :: String -> [String] -> [CmdY] -> IO ResYSource

sends a bunch of commands and reads the result. This function is similar to quickCheckY but does not append a check command. It can be useful if you intend to