Function mk_op

Source

pub unsafe extern "C" fn mk_op(
    tm: *mut TermManager,
    kind: Kind,
    size: usize,
    idxs: *const u32,
) -> Op

Expand description

Create operator of Kind:

#CVC5_KIND_BITVECTOR_EXTRACT
#CVC5_KIND_BITVECTOR_REPEAT
#CVC5_KIND_BITVECTOR_ROTATE_LEFT
#CVC5_KIND_BITVECTOR_ROTATE_RIGHT
#CVC5_KIND_BITVECTOR_SIGN_EXTEND
#CVC5_KIND_BITVECTOR_ZERO_EXTEND
#CVC5_KIND_DIVISIBLE
#CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_FP
#CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_IEEE_BV
#CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_REAL
#CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_SBV
#CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_UBV
#CVC5_KIND_FLOATINGPOINT_TO_SBV
#CVC5_KIND_FLOATINGPOINT_TO_UBV
#CVC5_KIND_INT_TO_BITVECTOR
#CVC5_KIND_TUPLE_PROJECT

See Cvc5Kind for a description of the parameters.

@param tm The term manager instance. @param kind The kind of the operator. @param size The number of indices of the operator. @param idxs The indices.

@note If idxs is empty, the Cvc5Op simply wraps the Cvc5Kind. The Cvc5Kind can be used in cvc5_mk_term directly without creating a Cvc5Op first.

mk_op

Function mk_op Copy item path

Function mk_op