implementation module Z3

import StdString

import System.Process
import Text

:: Z3 =
	{ handle :: ProcessHandle
	, stdIn  :: WritePipe
	, stdOut :: ReadPipe
	, stdErr :: ReadPipe
	}

startZ3 :: !*World -> (!Z3, !*World)
startZ3 w
# (err, w) = runProcessIO "z3" ["-smt2", "-in"] Nothing w
# (handle, {ProcessIO | stdIn, stdOut, stdErr}) = fromOk err
# z3 = { Z3 |
		handle = handle,
		stdIn  = stdIn,
		stdOut = stdOut,
		stdErr = stdErr
	}
= (z3, w)

addAssert :: !Z3 !String !*World -> *World
addAssert z3 s w
# (_, w) = writePipe ("(assert " <+ s <+ ")\n") z3.Z3.stdIn w
= w

addVariable :: !Z3 !String !*World -> *World
addVariable z3 s w
# (_, w) = writePipe ("(declare-const " <+ s <+ " Real)\n") z3.Z3.stdIn w
= w

checkSat :: !Z3 !*World -> (!Bool, !*World)
checkSat z3 w
# (_, w) = writePipe "(check-sat)\n" z3.Z3.stdIn w
# (out, w) = readPipeBlocking z3.Z3.stdOut w
# out = fromOk out
= (startsWith "sat" out, w)

getModel :: !Z3 !*World -> (!String, !*World)
getModel z3 w
# (_, w) = writePipe "(get-model)\n" z3.Z3.stdIn w
# (_, w) = writePipe "(exit)\n" z3.Z3.stdIn w
# (_, w) = waitForProcess z3.Z3.handle w
# (out, w) = readPipeNonBlocking z3.Z3.stdOut w
# out = fromOk out
= (out, w)