Skip to main content

mk_ff_elem

Function mk_ff_elem 

Source
pub unsafe extern "C" fn mk_ff_elem(
    tm: *mut TermManager,
    value: *const c_char,
    sort: Sort,
    base: u32,
) -> Term
Expand description

Create a finite field constant in a given field from a given string of base n.

@param tm The term manager instance. @param value The string representation of the constant. @param sort The field sort. @param base The base of the string representation of value.

If size is the field size, the constant needs not be in the range [0,size). If it is outside this range, it will be reduced modulo size before being constructed.