Struct z3::Optimize [−][src]
pub struct Optimize<'ctx> { /* fields omitted */ }
Expand description
Context for solving optimization queries.
Implementations
Assert hard constraint to the optimization context.
See also:
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:
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:
Backtrack one level.
Preconditions:
- The number of calls to
Optimize::pop
cannot exceed the number of calls toOptimize::push()
.
See also:
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
.
Retrieve the objectives for the last Optimize::check()
This contains maximize/minimize objectives and grouped soft constraints.
Retrieve a string that describes the last status returned by Optimize::check()
.
Use this method when Optimize::check()
returns SatResult::Unknown
.
Trait Implementations
Auto Trait Implementations
impl<'ctx> RefUnwindSafe for Optimize<'ctx>
impl<'ctx> UnwindSafe for Optimize<'ctx>