blob: 5cff8939fcf5029bd48b1a42c9268ce8e67071fd (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
definition module Z3
from System.Process import :: ProcessHandle, :: ProcessIO
:: Z3
:: Satisfaction
= Sat
| Unsat
| Unknown
startZ3 :: !*World -> (!Z3, !*World)
addAssert :: !Z3 !String !*World -> *World
addMinimize :: !Z3 !String !*World -> *World
addVariable :: !Z3 !String !String !*World -> *World
checkSat :: !Z3 !*World -> (!Satisfaction, !*World)
// Note: getModel terminates z3
getModel :: !Z3 !*World -> (!String, !*World)
|
