mk_const method

Z3_ast mk_const(
  1. Z3_context c,
  2. Z3_symbol s,
  3. Z3_sort ty
)

\brief Declare and create a constant.

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

\sa Z3_mk_app \sa Z3_mk_fresh_const \sa Z3_mk_func_decl

def_API('Z3_mk_const', AST, (_in(CONTEXT), _in(SYMBOL), _in(SORT)))

Implementation

Z3_ast mk_const(
  Z3_context c,
  Z3_symbol s,
  Z3_sort ty,
) {
  return _mk_const(
    c,
    s,
    ty,
  );
}