Function z3_sys::Z3_mk_const

source · 
pub unsafe extern "C" fn Z3_mk_const(
    c: Z3_context,
    s: Z3_symbol,
    ty: Z3_sort
) -> Z3_ast
Expand description

Declare and create a constant.

This function is a shorthand for:

Z3_func_decl d = Z3_mk_func_decl(c, s, 0, 0, ty);
Z3_ast n             = Z3_mk_app(c, d, 0, 0);

See also: