1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
implementation module Z3
import System.Process
import Text
import StdString
import StdDebug
:: 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 (trace_s ("(assert " <+ s <+ ")\n")) z3.Z3.stdIn w
= w
addVariable :: !Z3 !String !*World -> *World
addVariable z3 s w
# (_, w) = writePipe (trace_s ("(declare-const " <+ s <+ " Real)\n")) z3.Z3.stdIn w
= w
checkSat :: !Z3 !*World -> (!Bool, !*World)
checkSat z3 w
# (_, w) = writePipe (trace_s "(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 (trace_s "(get-model)\n") z3.Z3.stdIn w
# (_, w) = writePipe (trace_s "(exit)\n") z3.Z3.stdIn w
# (_, w) = waitForProcess z3.Z3.handle w
# (out, w) = readPipeNonBlocking z3.Z3.stdOut w
# out = fromOk out
= (out, w)
trace_s :: String -> String
trace_s s = trace s s
|
