pub struct Goal<'ctx> { /* private fields */ }
Expand description
Set of formulas that can be solved and/or transformed using tactics and solvers.
Implementations§
source§impl<'ctx> Goal<'ctx>
impl<'ctx> Goal<'ctx>
pub fn new( ctx: &'ctx Context, models: bool, unsat_cores: bool, proofs: bool ) -> Goal<'ctx>
sourcepub fn is_inconsistent(&self) -> bool
pub fn is_inconsistent(&self) -> bool
Return true if the given goal contains the formula false
.
sourcepub fn get_depth(&self) -> u32
pub fn get_depth(&self) -> u32
Return the depth of the given goal. It tracks how many transformations were applied to it.
sourcepub fn get_num_expr(&self) -> u32
pub fn get_num_expr(&self) -> u32
Return the number of formulas, subformulas and terms in the given goal.
sourcepub fn is_decided_sat(&self) -> bool
pub fn is_decided_sat(&self) -> bool
Return true if the goal is empty, and it is precise or the product of a under approximation.
sourcepub fn is_decided_unsat(&self) -> bool
pub fn is_decided_unsat(&self) -> bool
Return true if the goal contains false, and it is precise or the product of an over approximation.
sourcepub fn translate<'dest_ctx>(self, ctx: &'dest_ctx Context) -> Goal<'dest_ctx>
pub fn translate<'dest_ctx>(self, ctx: &'dest_ctx Context) -> Goal<'dest_ctx>
Copy a goal g
from the context source
to the context target
.
sourcepub fn get_precision(&self) -> GoalPrec
pub fn get_precision(&self) -> GoalPrec
Return the “precision” of the given goal. Goals can be transformed using over and under approximations.
pub fn iter_formulas<'a, T>(&'a self) -> impl Iterator<Item = T> + 'awhere T: Ast<'a>,
sourcepub fn get_formulas<T>(&self) -> Vec<T>where
T: Ast<'ctx>,
pub fn get_formulas<T>(&self) -> Vec<T>where T: Ast<'ctx>,
Return a vector of the formulas from the given goal.
Trait Implementations§
Auto Trait Implementations§
impl<'ctx> RefUnwindSafe for Goal<'ctx>
impl<'ctx> !Send for Goal<'ctx>
impl<'ctx> !Sync for Goal<'ctx>
impl<'ctx> Unpin for Goal<'ctx>
impl<'ctx> UnwindSafe for Goal<'ctx>
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