Function z3_sys::Z3_get_ast_id

pub unsafe extern "C" fn Z3_get_ast_id(c: Z3_context, t: Z3_ast) -> c_uint

Return a unique identifier for t.

The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.