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)