Enum Z3Solver 

pub enum Z3Solver<'a> {
    Solve(Solver<'a>),
    Optimize(Optimize<'a>),
}

Variants

Solve(Solver<'a>)

Optimize(Optimize<'a>)

Implementations

impl<'a> Z3Solver<'a>

pub fn assert(&self, ast: &Bool<'a>)

pub fn set_threads(&self, ctx: &'a Context, threads: u32)

pub fn check(&self) -> SatResult

pub fn get_model(&self) -> Option<Model<'_>>

pub fn minimize_int(&self, expr: &Int<'_>)

pub fn maximize_int(&self, expr: &Int<'_>)

pub fn minimize_real(&self, expr: &Real<'_>)

pub fn maximize_real(&self, expr: &Real<'_>)

Trait Implementations

impl<'a> Display for Z3Solver<'a>

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

Formats the value using the given formatter.