Struct z3::Optimize

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

Context for solving optimization queries.

Implementations

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::assert_soft()
• Optimize::maximize()
• Optimize::minimize()

pub fn assert_soft(
    &self,
    ast: &impl Ast<'ctx>,
    weight: impl Weight,
    group: Option<Symbol>
)

Assert soft constraint to the optimization context. Weight is a positive, rational penalty for violating the constraint. Group is an optional identifier to group soft constraints.

See also:

• Optimize::assert()
• 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) -> Option<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_objectives(&self) -> Vec<Dynamic<'ctx>>

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

This contains maximize/minimize objectives and grouped soft constraints.

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> Debug for Optimize<'ctx>

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

Formats the value using the given formatter.

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

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

Formats the value using the given formatter.

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

fn drop(&mut self)

Executes the destructor for this type.