Struct z3::Goal

pub struct Goal<'ctx> { /* fields omitted */ }

Set of formulas that can be solved and/or transformed using tactics and solvers.

Implementations

impl<'ctx> Goal<'ctx>

pub fn new_from_z3_type(
    ctx: &'ctx Context,
    z3_goal: Z3_goal,
    models: bool,
    unsat_cores: bool,
    proofs: bool
) -> Goal<'ctx>

pub fn new(
    ctx: &'ctx Context,
    models: bool,
    unsat_cores: bool,
    proofs: bool
) -> Goal<'ctx>

pub fn assert(&self, ast: &impl Ast<'ctx>)

Add a new formula a to the given goal.

pub fn is_inconsistent(&self) -> bool

Return true if the given goal contains the formula false.

pub fn get_depth(&self) -> u32

Return the depth of the given goal. It tracks how many transformations were applied to it.

pub fn get_size(&self) -> u32

Return the number of formulas in the given goal.

pub fn get_num_expr(&self) -> u32

Return the number of formulas, subformulas and terms in the given goal.

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.

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.

pub fn reset(&self)

Erase all formulas from the given goal.

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.

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> + 'a where
    T: Ast<'a>, 

pub fn get_formulas<T>(&self) -> Vec<T> where
    T: Ast<'ctx>, 

Return a vector of the formulas from the given goal.

Trait Implementations

impl<'ctx> Clone for Goal<'ctx>

fn clone(&self) -> Self

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<'ctx> Debug for Goal<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Display for Goal<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Drop for Goal<'ctx>

fn drop(&mut self)

Executes the destructor for this type.