ATSLIB/contrib/SMT/Z3/z3

This package contains an API for programming the SMT-solver Z3 in ATS.

Z3_mk_config

fun Z3_mk_config (): Z3_config = "mac#%"

fun Z3_del_config (cfg: Z3_config): void = "mac#%"

fun Z3_set_param_value
(
  cfg: !Z3_config, p_id: Z3_string, p_val: Z3_string
) : void = "mac#%" // end of [Z3_set_param_value]

Synopsis for [Z3_mk_context] is unavailable.

fun Z3_mk_context_rc (cfg: !Z3_config): Z3_context = "mac#%"

fun Z3_del_context (ctx: Z3_context): void

fun Z3_inc_ref{l:addr}
  (ctx: !Z3_context, a: !Z3_ast l): Z3_ast (l) = "mac#%"

fun Z3_dec_ref (ctx: !Z3_context, a: Z3_ast): void = "mac#%"

fun Z3_get_param_value
(
  ctx: !Z3_context, p_id: Z3_string, p_val: &ptr? >> opt (Z3_string, b)
) : #[b:bool] bool (b) = "mac#%"

fun Z3_update_param_value
  (ctx: !Z3_context, p_id: Z3_string, p_val: Z3_string): void = "mac#%"

fun Z3_interrupt (ctx: !Z3_context): void = "mac#%"