Struct Goal 

pub struct Goal { /* private fields */ }

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

Implementations

impl Goal

pub fn new(models: bool, unsat_cores: bool, proofs: bool) -> Goal

pub fn assert(&self, ast: &impl Ast)

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 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,

pub fn get_formulas(&self) -> Vec<Bool>

Return a vector of the formulas from the given goal.

Though not guaranteed by Z3’s type system, goals and subgoals are conceptually always going to be expressions of the Bool Sort.

Trait Implementations

impl Clone for Goal

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Goal

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

Formats the value using the given formatter.

impl Display for Goal

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

Formats the value using the given formatter.

impl Drop for Goal

fn drop(&mut self)

Executes the destructor for this type.

impl Translate for Goal

fn translate(&self, ctx: &Context) -> Goal