Struct Z3Model 

pub struct Z3Model { /* private fields */ }

Analogue of z3::Model.

Produced by Z3Solver::get_model after a Sat result.

Implementations

impl Z3Model

pub fn get_func_interp(&self, f: &FuncDecl) -> Option<Z3FuncInterp>

Return the full interpretation of an uninterpreted function f in this model, or None if f was not declared or is not present in the model.

The returned Z3FuncInterp contains the finite set of (args → value) entries that the solver determined, plus an else_value for all other inputs.

Stub note

When the EUF e-graph does not contain any application of f (e.g. the function was declared but never constrained), num_entries() will be 0 and else_value() will be the default value for the return sort. This is a valid (conservative) interpretation: the solver is free to choose any value for unconstrained applications.

impl Z3Model

pub fn eval_const(&self, name: &str) -> Option<&str>

Evaluate a constant (identified by name) in the model.

Returns Some(value_string) if the constant was found, None otherwise.

pub fn entries(&self) -> &[(String, String, String)]

Return all model entries as (name, sort, value) slices.

pub fn func_interp_raw( &self, func_name: &str, ) -> Option<&(Vec<(Vec<String>, String)>, String, usize)>

Return the raw function interpretation data for the function named func_name, if it was declared and the model is available.

This is a low-level accessor; prefer Z3Model::get_func_interp (defined in ext2) for the typed wrapper.

Trait Implementations

impl Display for Z3Model

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.