Struct z3::Optimize

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

Context for solving optimization queries.

Methods

impl<'ctx> Optimize<'ctx>

pub fn new(ctx: &'ctx Context) -> Optimize<'ctx>

Create a new optimize context.

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

Assert hard constraint to the optimization context.

See also:

• Optimize::maximize()
• Optimize::minimize()

pub fn maximize(&self, ast: &impl Ast<'ctx>)

Add a maximization constraint.

See also:

• Optimize::assert()
• Optimize::minimize()

pub fn minimize(&self, ast: &impl Ast<'ctx>)

Add a minimization constraint.

See also:

• Optimize::assert()
• Optimize::maximize()

pub fn push(&self)

Create a backtracking point.

The optimize solver contains a set of rules, added facts and assertions. The set of rules, facts and assertions are restored upon calling Optimize::pop().

See also:

• Optimize::pop()

pub fn pop(&self)

Backtrack one level.

Preconditions:

• The number of calls to Optimize::pop cannot exceed the number of calls to Optimize::push().

See also:

• Optimize::push()

pub fn check(&self, assumptions: &[Bool<'ctx>]) -> SatResult

Check consistency and produce optimal values.

See also:

• Optimize::get_model()

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

Retrieve the model for the last Optimize::check()

The error handler is invoked if a model is not available because the commands above were not invoked for the given optimization solver, or if the result was Z3_L_FALSE.

pub fn get_reason_unknown(&self) -> Option<String>

Retrieve a string that describes the last status returned by Optimize::check().

Use this method when Optimize::check() returns SatResult::Unknown.

Trait Implementations

impl<'ctx> Drop for Optimize<'ctx>

fn drop(&mut self)

Executes the destructor for this type.

impl<'ctx> Display for Optimize<'ctx>

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

Formats the value using the given formatter.