Struct z3::FuncInterp

pub struct FuncInterp<'ctx> { /* private fields */ }

Stores the interpretation of a function in a Z3 model. https://z3prover.github.io/api/html/classz3py_1_1_func_interp.html

Implementations

impl<'ctx> FuncInterp<'ctx>

pub fn get_arity(&self) -> usize

Returns the number of arguments in the function interpretation.

pub fn get_num_entries(&self) -> u32

Returns the number of entries in the function interpretation.

pub fn add_entry(&self, args: &[Dynamic<'ctx>], value: &Dynamic<'ctx>)

Adds an entry to the function interpretation.

pub fn get_entries(&self) -> Vec<FuncEntry<'_>>

Returns the entries of the function interpretation.

pub fn get_else(&self) -> Dynamic<'ctx>

Returns the else value of the function interpretation. Returns None if the else value is not set by Z3.

pub fn set_else(&self, ast: &Dynamic<'_>)

Sets the else value of the function interpretation.

Trait Implementations

impl<'ctx> Debug for FuncInterp<'ctx>

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

Formats the value using the given formatter.

impl<'ctx> Display for FuncInterp<'ctx>

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

Formats the value using the given formatter.

impl<'ctx> Drop for FuncInterp<'ctx>

fn drop(&mut self)

Executes the destructor for this type.