Function z3_sys::Z3_mk_fresh_const

source · 
pub unsafe extern "C" fn Z3_mk_fresh_const(
    c: Z3_context,
    prefix: Z3_string,
    ty: Z3_sort
) -> Z3_ast
Expand description

Declare and create a fresh constant.

This function is a shorthand for:

Z3_func_decl d = Z3_mk_fresh_func_decl(c, prefix, 0, 0, ty);
Z3_ast n = Z3_mk_app(c, d, 0, 0);

NOTE: If prefix is NULL, then it is assumed to be the empty string.

See also: