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

pub trait LogVisitor {

Show 16 methods    fn add_term(&mut self, id: Ident, term: Term) -> RawResult<()>;

    fn add_instantiation(&mut self, key: QiKey, frame: QiFrame) -> RawResult<()>;

    fn start_instance(
        &mut self, 
        key: QiKey, 
        instance: QiInstance
    ) -> 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<()>;

}
Expand description

Actions taken when visiting Z3 logs.

Required methods

Implementors