Function mk_const

pub unsafe extern "C" fn mk_const(
    tm: *mut TermManager,
    sort: Sort,
    symbol: *const c_char,
) -> Term

Expand description

Create a free constant.

SMT-LIB:

\verbatim embed:rst:leading-asterisk .. code:: smtlib

(declare-const <symbol> <sort>)
(declare-fun <symbol> () <sort>)

\endverbatim

@param tm The term manager instance. @param sort The sort of the constant. @param symbol The name of the constant, may be NULL. @return The constant.

mk_const