Assignment2/src/Z3.dcl


1
2
3
4
5
6
7
8
9
10
11
12
13

definition module Z3

from System.Process import :: ProcessHandle, :: ProcessIO

:: Z3

startZ3 :: *World -> (Z3, *World)
addAssert :: Z3 String *World -> *World
addVariable :: Z3 String *World -> *World
checkSat :: Z3 *World -> (Bool, *World)

// Note: getModel terminates z3
getModel :: Z3 *World -> (String, *World)