Struct z3tracer::model::Model [−][src]
Main state of the Z3 tracer.
Implementations
impl Model
[src]
pub fn new(config: ModelConfig) -> Self
[src]
Build a new Z3 tracer.
Experimental. Use Model::default()
instead if possible.
pub fn process<R>(&mut self, path_name: Option<String>, input: R) -> Result<()> where
R: BufRead,
[src]
R: BufRead,
Process some input.
pub fn terms(&self) -> &BTreeMap<Ident, TermData>
[src]
All terms in the model.
pub fn instantiations(&self) -> &BTreeMap<QiKey, QuantInstantiation>
[src]
All instantiations in the model.
pub fn processed_logs(&self) -> usize
[src]
Number of Z3 logs that were processed.
pub fn most_instantiated_terms(&self) -> BinaryHeap<(usize, Ident)>
[src]
Construct a max-heap of the (most) instantiated quantified terms.
pub fn term(&self, id: &Ident) -> RawResult<&Term>
[src]
Retrieve a particular term.
pub fn term_data(&self, id: &Ident) -> RawResult<&TermData>
[src]
Retrieve a particular term, including metadata.
pub fn id_to_sexp(
&self,
venv: &BTreeMap<u64, Symbol>,
id: &Ident
) -> RawResult<String>
[src]
&self,
venv: &BTreeMap<u64, Symbol>,
id: &Ident
) -> RawResult<String>
Display a term given by id.
pub fn term_to_sexp(
&self,
venv: &BTreeMap<u64, Symbol>,
term: &Term
) -> RawResult<String>
[src]
&self,
venv: &BTreeMap<u64, Symbol>,
term: &Term
) -> RawResult<String>
Display a term by id.
Trait Implementations
impl Debug for Model
[src]
impl Default for Model
[src]
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<()>
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, m: 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]
Auto Trait Implementations
impl RefUnwindSafe for Model
impl Send for Model
impl Sync for Model
impl Unpin for Model
impl UnwindSafe for Model
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,