mk_fresh_const method

Z3_ast mk_fresh_const(
  1. Z3_context c,
  2. Z3_string prefix,
  3. Z3_sort ty
)

\brief Declare and create a fresh constant.

This function is a shorthand for: \code Z3_func_decl d = Z3_mk_fresh_func_decl(c, prefix, 0, 0, ty); Z3_ast n = Z3_mk_app(c, d, 0, 0); \endcode

\remark If \c prefix is \c NULL, then it is assumed to be the empty string.

\sa Z3_mk_app \sa Z3_mk_const \sa Z3_mk_fresh_func_decl \sa Z3_mk_func_decl

def_API('Z3_mk_fresh_const', AST, (_in(CONTEXT), _in(STRING), _in(SORT)))

Implementation

Z3_ast mk_fresh_const(
  Z3_context c,
  Z3_string prefix,
  Z3_sort ty,
) {
  return _mk_fresh_const(
    c,
    prefix,
    ty,
  );
}