Struct FuncInterp 

pub struct FuncInterp { /* 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 FuncInterp

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], value: &Dynamic)

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

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 Debug for FuncInterp

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

Formats the value using the given formatter.

impl Display for FuncInterp

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

Formats the value using the given formatter.

impl Drop for FuncInterp

fn drop(&mut self)

Executes the destructor for this type.