pub struct Optimize { /* private fields */ }Expand description
Context for solving optimization queries.
Implementations§
Source§impl Optimize
impl Optimize
Sourcepub fn from_string<T: Into<Vec<u8>>>(&self, source_string: T)
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.
Sourcepub fn get_context(&self) -> &Context
pub fn get_context(&self) -> &Context
Get this optimizers ’s context.
Sourcepub fn assert(&self, ast: &impl Ast)
pub fn assert(&self, ast: &impl Ast)
Assert hard constraint to the optimization context.
§See also:
Sourcepub fn assert_and_track(&self, ast: &Bool, p: &Bool)
pub fn assert_and_track(&self, ast: &Bool, p: &Bool)
Assert a constraint a into the solver, and track it (in the
unsat) core using the Boolean constant p.
This API is an alternative to
Optimize::check()
for extracting unsat cores. Both APIs can be used in the same solver.
The unsat core will contain a combination of the Boolean variables
provided using Optimize::assert_and_track()
and the Boolean literals provided using
Optimize::check().
§See also:
Sourcepub fn assert_soft(
&self,
ast: &impl Ast,
weight: impl Weight,
group: Option<Symbol>,
)
pub fn assert_soft( &self, ast: &impl Ast, 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:
Sourcepub fn get_unsat_core(&self) -> Vec<Bool>
pub fn get_unsat_core(&self) -> Vec<Bool>
Return a subset of the assumptions provided to either the last
Optimize::checkcall, or- sequence of
Optimize::assert_and_trackcalls followed by anOptimize::checkcall.
These are the assumptions Z3 used in the unsatisfiability proof. Assumptions are available in Z3. They are used to extract unsatisfiable cores. They may be also used to “retract” assumptions. Note that, assumptions are not really “soft constraints”, but they can be used to implement them.
By default, the unsat core will not be minimized. Generation of a minimized
unsat core can be enabled via the "sat.core.minimize" and "smt.core.minimize"
settings for SAT and SMT cores respectively. Generation of minimized unsat cores
will be more expensive.
§See also:
Sourcepub fn push(&self)
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:
Sourcepub fn pop(&self)
pub fn pop(&self)
Backtrack one level.
§Preconditions:
- The number of calls to
Optimize::popcannot exceed the number of calls toOptimize::push().
§See also:
Sourcepub fn get_model(&self) -> Option<Model>
pub fn get_model(&self) -> Option<Model>
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.
Sourcepub fn get_objectives(&self) -> Vec<Dynamic>
pub fn get_objectives(&self) -> Vec<Dynamic>
Retrieve the objectives for the last Optimize::check().
This contains maximize/minimize objectives and grouped soft constraints.
Sourcepub fn get_reason_unknown(&self) -> Option<String>
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.
Sourcepub fn set_params(&self, params: &Params)
pub fn set_params(&self, params: &Params)
Configure the parameters for this Optimize.
Sourcepub fn get_statistics(&self) -> Statistics
pub fn get_statistics(&self) -> Statistics
Retrieve the statistics for the last Optimize::check().