pub struct Optimize<'ctx> { /* private fields */ }
Implementations
sourceimpl<'ctx> Optimize<'ctx>
impl<'ctx> Optimize<'ctx>
sourcepub fn assert(&self, ast: &Ast<'ctx>)
pub fn assert(&self, ast: &Ast<'ctx>)
Assert hard constraint to the optimization context.
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::pop
cannot exceed the number of calls toOptimize::push()
.
See also:
sourcepub fn get_model(&self) -> Model<'ctx>
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
.
Trait Implementations
Auto Trait Implementations
impl<'ctx> RefUnwindSafe for Optimize<'ctx>
impl<'ctx> !Send for Optimize<'ctx>
impl<'ctx> !Sync for Optimize<'ctx>
impl<'ctx> Unpin for Optimize<'ctx>
impl<'ctx> UnwindSafe for Optimize<'ctx>
Blanket Implementations
sourceimpl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more