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)