Struct z3::Model

pub struct Model<'ctx> { /* fields omitted */ }

Model for the constraints inserted into the logical context.

Methods

impl<'ctx> Model<'ctx>

pub fn of_solver(slv: &Solver<'ctx>) -> Model<'ctx>

pub fn of_optimize(opt: &Optimize<'ctx>) -> Model<'ctx>

pub fn eval<T>(&self, ast: &T) -> Option<T> where
    T: Ast<'ctx>, 

Trait Implementations

impl<'ctx> Drop for Model<'ctx>

fn drop(&mut self)

Executes the destructor for this type.

impl<'ctx> Display for Model<'ctx>

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

Formats the value using the given formatter.