Struct z3tracer::model::TermData[−][src]

pub struct TermData {
    pub term: Term,
    pub enode_qi_dependencies: BTreeSet<QIKey>,
    pub assignment: Option<bool>,
    pub instantiations: Vec<QIKey>,
    pub proofs: Vec<Ident>,
    pub timestamp: usize,
}

Information on a term in the model.

Fields

term: Term

Term definition.

enode_qi_dependencies: BTreeSet<QIKey>

QIs that made this term an active “enode”.

assignment: Option<bool>

Last truth assignment, if any.

instantiations: Vec<QIKey>

Known instantiations (applicable when term is a quantified expression).

proofs: Vec<Ident>

Known proofs of this term (applicable when term is a boolean formula).

timestamp: usize

Track the relative creation time of this term. Currently, this is the line number in the Z3 log.

Trait Implementations

impl Clone for TermData[src]

impl Debug for TermData[src]

Auto Trait Implementations

Blanket Implementations

impl<T> Any for T where
    T: 'static + ?Sized, [src]

impl<T> Borrow<T> for T where
    T: ?Sized, [src]

impl<T> BorrowMut<T> for T where
    T: ?Sized, [src]

impl<T> From<T> for T[src]

impl<T, U> Into<U> for T where
    U: From<T>, [src]

impl<T> ToOwned for T where
    T: Clone, [src]

type Owned = T

The resulting type after obtaining ownership.

impl<T, U> TryFrom<U> for T where
    U: Into<T>, [src]

type Error = Infallible

The type returned in the event of a conversion error.

impl<T, U> TryInto<U> for T where
    U: TryFrom<T>, [src]

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.