Struct z3::Symbol

pub struct Symbol<'ctx> { /* private fields */ }

Symbols are used to name several term and type constructors.

Creation:

Symbols can be created with either Symbol::from_int() or Symbol::from_string().

Implementations

impl<'ctx> Symbol<'ctx>

pub fn from_int(ctx: &Context, i: u32) -> Symbol<'_>

Create a Z3 symbol using an integer.

NB. Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.

See also:

• Symbol::from_string()

pub fn from_string(ctx: &'ctx Context, s: &str) -> Symbol<'ctx>

Create a Z3 symbol using a string.

See also:

• Symbol::from_int()