#[repr(u32)]pub enum GoalPrec {
Precise,
Under,
Over,
UnderOver,
}
Expand description
Precision of a given goal. Some goals can be transformed using over/under approximations.
This corresponds to Z3_goal_prec
in the C API.
Variants§
Precise
Approximations/Relaxations were not applied on the goal (sat and unsat answers were preserved).
This corresponds to Z3_GOAL_PRECISE
in the C API.
Under
Goal is the product of a under-approximation (sat answers are preserved).
This corresponds to Z3_GOAL_UNDER
in the C API.
Over
Goal is the product of an over-approximation (unsat answers are preserved).
This corresponds to Z3_GOAL_OVER
in the C API.
UnderOver
Goal is garbage (it is the product of over- and under-approximations, sat and unsat answers are not preserved).
This corresponds to Z3_GOAL_UNDER_OVER
in the C API.
Trait Implementations§
source§impl PartialEq<GoalPrec> for GoalPrec
impl PartialEq<GoalPrec> for GoalPrec
impl Copy for GoalPrec
impl Eq for GoalPrec
impl StructuralEq for GoalPrec
impl StructuralPartialEq for GoalPrec
Auto Trait Implementations§
impl RefUnwindSafe for GoalPrec
impl Send for GoalPrec
impl Sync for GoalPrec
impl Unpin for GoalPrec
impl UnwindSafe for GoalPrec
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more