Math.SMT.Yices.Pipe

Inter-process communication to Yices through pipe.

Documentation

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

type abbrevation for IPC handle quadruple

data ResY

To read in the result of the (check) command

Constructors

Sat [ExpY]

Unknown [ExpY]

UnSat [Integer]

InCon [String]

Instances

Show ResY

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

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 ()

send yices commands without flushing

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

send yices commands and flush

checkY :: YicesIPC -> IO ResY

send check command and reads the result

exitY :: YicesIPC -> IO ()

send exit command and flush

flushY :: YicesIPC -> IO ()

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

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

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 ResY

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