Trait z3tracer::parser::LogVisitor[−][src]

pub trait LogVisitor {
    fn add_term(&mut self, id: Ident, term: Term) -> RawResult<()>;

    fn add_instantiation(
        &mut self, 
        key: QIKey, 
        inst: QuantInstantiation
    ) -> RawResult<()>;

    fn start_instance(
        &mut self, 
        key: QIKey, 
        data: QuantInstantiationData
    ) -> RawResult<()>;

    fn end_instance(&mut self) -> RawResult<()>;

    fn add_equality(&mut self, id: Ident, eq: Equality) -> RawResult<()>;

    fn attach_meaning(&mut self, id: Ident, meaning: Meaning) -> RawResult<()>;

    fn attach_var_names(
        &mut self, 
        id: Ident, 
        names: Vec<VarName>
    ) -> RawResult<()>;

    fn attach_enode(&mut self, id: Ident, generation: u64) -> RawResult<()>;

    fn tool_version(&mut self, s1: String, s2: String) -> RawResult<()>;

    fn begin_check(&mut self, i: u64) -> RawResult<()>;

    fn assign(&mut self, lit: Literal, s: String) -> RawResult<()>;

    fn conflict(&mut self, lits: Vec<Literal>, s: String) -> RawResult<()>;

    fn push(&mut self, i: u64) -> RawResult<()>;

    fn pop(&mut self, i: u64, j: u64) -> RawResult<()>;

    fn resolve_lit(&mut self, i: u64, lit: Literal) -> RawResult<()>;

    fn resolve_process(&mut self, lit: Literal) -> RawResult<()>;
}

Actions taken when visiting Z3 logs.

Required methods

fn add_term(&mut self, id: Ident, term: Term) -> RawResult<()>[src]

fn add_instantiation(
    &mut self,
    key: QIKey,
    inst: QuantInstantiation
) -> RawResult<()>[src]

fn start_instance(
    &mut self,
    key: QIKey,
    data: QuantInstantiationData
) -> RawResult<()>[src]

fn end_instance(&mut self) -> RawResult<()>[src]

fn add_equality(&mut self, id: Ident, eq: Equality) -> RawResult<()>[src]

fn attach_meaning(&mut self, id: Ident, meaning: Meaning) -> RawResult<()>[src]

fn attach_var_names(&mut self, id: Ident, names: Vec<VarName>) -> RawResult<()>[src]

fn attach_enode(&mut self, id: Ident, generation: u64) -> RawResult<()>[src]

fn tool_version(&mut self, s1: String, s2: String) -> RawResult<()>[src]

fn begin_check(&mut self, i: u64) -> RawResult<()>[src]

fn assign(&mut self, lit: Literal, s: String) -> RawResult<()>[src]

fn conflict(&mut self, lits: Vec<Literal>, s: String) -> RawResult<()>[src]

fn push(&mut self, i: u64) -> RawResult<()>[src]

fn pop(&mut self, i: u64, j: u64) -> RawResult<()>[src]

fn resolve_lit(&mut self, i: u64, lit: Literal) -> RawResult<()>[src]

fn resolve_process(&mut self, lit: Literal) -> RawResult<()>[src]

Loading content...

Implementors

impl LogVisitor for &mut Model[src]

Loading content...