Struct seer_z3::Solver [−][src]
pub struct Solver<'ctx> { /* fields omitted */ }Methods
impl<'ctx> Solver<'ctx>[src]
impl<'ctx> Solver<'ctx>pub fn new(ctx: &Context) -> Solver[src]
pub fn new(ctx: &Context) -> Solverpub fn assert(&self, ast: &Ast<'ctx>)[src]
pub fn assert(&self, ast: &Ast<'ctx>)pub fn check(&self) -> bool[src]
pub fn check(&self) -> boolpub fn get_model(&self) -> Model<'ctx>[src]
pub fn get_model(&self) -> Model<'ctx>