pub trait Z3LogParser {
Show 26 methods
// Required methods
fn version_info<'a>(
&mut self,
l: impl Iterator<Item = &'a str>,
) -> Result<()>;
fn mk_quant<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
fn mk_lambda<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
fn mk_var<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
fn mk_app<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
fn mk_proof<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
fn attach_meaning<'a>(
&mut self,
l: impl Iterator<Item = &'a str>,
) -> Result<()>;
fn attach_var_names<'a>(
&mut self,
l: impl Iterator<Item = &'a str>,
) -> Result<()>;
fn attach_enode<'a>(
&mut self,
l: impl Iterator<Item = &'a str>,
) -> Result<()>;
fn eq_expl<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
fn new_match<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
fn inst_discovered<'a>(
&mut self,
l: impl Iterator<Item = &'a str>,
) -> Result<()>;
fn instance<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>;
fn end_of_instance<'a>(
&mut self,
l: impl Iterator<Item = &'a str>,
) -> Result<()>;
fn push<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>;
fn pop<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>;
fn eof(&mut self);
// Provided methods
fn newline(&mut self) { ... }
fn decide_and_or<'a>(
&mut self,
_l: impl Iterator<Item = &'a str>,
) -> Result<()> { ... }
fn decide<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> { ... }
fn assign<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> { ... }
fn begin_check<'a>(
&mut self,
_l: impl Iterator<Item = &'a str>,
) -> Result<()> { ... }
fn query_done<'a>(
&mut self,
_l: impl Iterator<Item = &'a str>,
) -> Result<()> { ... }
fn resolve_process<'a>(
&mut self,
_l: impl Iterator<Item = &'a str>,
) -> Result<()> { ... }
fn resolve_lit<'a>(
&mut self,
_l: impl Iterator<Item = &'a str>,
) -> Result<()> { ... }
fn conflict<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()> { ... }
}Required Methods§
fn version_info<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn mk_quant<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn mk_lambda<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn mk_var<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn mk_app<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn mk_proof<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn attach_meaning<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn attach_var_names<'a>( &mut self, l: impl Iterator<Item = &'a str>, ) -> Result<()>
fn attach_enode<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn eq_expl<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn new_match<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn inst_discovered<'a>( &mut self, l: impl Iterator<Item = &'a str>, ) -> Result<()>
fn instance<'a>(&mut self, l: impl Iterator<Item = &'a str>) -> Result<()>
fn end_of_instance<'a>( &mut self, l: impl Iterator<Item = &'a str>, ) -> Result<()>
fn push<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
fn pop<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
fn eof(&mut self)
Provided Methods§
fn newline(&mut self)
fn decide_and_or<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
fn decide<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
fn assign<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
fn begin_check<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
fn query_done<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
fn resolve_process<'a>( &mut self, _l: impl Iterator<Item = &'a str>, ) -> Result<()>
fn resolve_lit<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
fn conflict<'a>(&mut self, _l: impl Iterator<Item = &'a str>) -> Result<()>
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.