Enum z3_sys::GoalPrec [−][src]
#[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
Approximations/Relaxations were not applied on the goal (sat and unsat answers were preserved).
This corresponds to Z3_GOAL_PRECISE
in the C API.
Goal is the product of a under-approximation (sat answers are preserved).
This corresponds to Z3_GOAL_UNDER
in the C API.
Goal is the product of an over-approximation (unsat answers are preserved).
This corresponds to Z3_GOAL_OVER
in the C API.
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
Auto Trait Implementations
impl RefUnwindSafe for GoalPrec
impl UnwindSafe for GoalPrec
Blanket Implementations
Mutably borrows from an owned value. Read more