Struct Term 

pub struct Term {
    pub id: TermId,
    pub child_ids: BoxSlice<TermIdx>,
    /* private fields */
}

A Z3 term and associated data.

Fields

id: TermId

child_ids: BoxSlice<TermIdx>

Takes up 2 * size_of::<usize>() space and avoids heap allocation for lens <= 1.

Implementations

impl Term

pub fn new<'a>( id: TermId, kind: TermKind, child_ids: BoxSlice<TermIdx>, t: impl Fn(TermIdx) -> &'a Term, ) -> Self

pub fn kind(&self) -> TermKind

pub fn var_idx(&self) -> Option<NonMaxU32>

pub fn app_name(&self) -> Option<IString>

pub fn quant_idx(&self) -> Option<QuantIdx>

pub fn has_var(&self) -> Option<bool>

Does this term contain a free variable? Returns None if the term contains a quantifier (which may or may not bind all the free vars).

pub fn can_match(&self, other: &Self) -> bool

Checks if this term can match another term. That is, if they have the same kind and the same number of children. The children may still be different.

impl Term

pub fn as_any(&self) -> &AnyTerm

Trait Implementations

impl Clone for Term

fn clone(&self) -> Term

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Term

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl HasTermId for Term

fn term_id(&self) -> TermId

impl Hash for Term

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Term

fn eq(&self, other: &Term) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Term

impl StructuralPartialEq for Term