Struct z3::Solver

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

Methods

impl<'ctx> Solver<'ctx>

fn new(ctx: &Context) -> Solver

fn assert(&self, ast: &Ast<'ctx>)

fn check(&self) -> bool

fn get_model(&self) -> Model<'ctx>

Trait Implementations

impl<'ctx> Drop for Solver<'ctx>

fn drop(&mut self)

A method called when the value goes out of scope.