Trait z3tracer::parser::LogVisitor [−][src]
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]
&mut self,
key: QIKey,
inst: QuantInstantiation
) -> RawResult<()>
fn start_instance(
&mut self,
key: QIKey,
data: QuantInstantiationData
) -> RawResult<()>
[src]
&mut self,
key: QIKey,
data: QuantInstantiationData
) -> RawResult<()>
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]
Implementors
impl LogVisitor for &mut Model
[src]
fn add_term(&mut self, ident: Ident, term: Term) -> RawResult<()>
[src]
fn add_instantiation(
&mut self,
key: QIKey,
inst: QuantInstantiation
) -> RawResult<()>
[src]
&mut self,
key: QIKey,
inst: QuantInstantiation
) -> RawResult<()>
fn start_instance(
&mut self,
key: QIKey,
data: QuantInstantiationData
) -> RawResult<()>
[src]
&mut self,
key: QIKey,
data: QuantInstantiationData
) -> RawResult<()>