Struct z3::Optimize

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

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 from_string<T: Into<Vec<u8>>>(&self, source_string: T)

Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimizer.

pub fn get_context(&self) -> &'ctx Context

Get this optimizers ’s 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 SatResult::Unsat.

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.

pub fn get_statistics(&self) -> Statistics<'ctx>

Retrieve the statistics for the last Optimize::check().

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.