Struct Axiom 

pub struct Axiom {
    pub def_id: FluxLocalDefId,
    pub body: Binder<AxiomBody>,
}

An Axiom is a (global) fact, typically about uninterpreted functions, that is assumed to hold for all values of the variables bound in body.

Fields

def_id: FluxLocalDefId

body: Binder<AxiomBody>

Implementations

impl Axiom

pub fn new( genv: GlobalEnv<'_, '_>, def_id: FluxLocalDefId, body: Binder<Expr>, ) -> Result<Self, UncoveredAxiomVar>

Creates an axiom, computing its patterns from body, which must have already been reduced so that the applications are the ones that will be sent to the solver.

A function is considered uninterpreted if it has no body or if it is hidden. We also include the arithmetic and bitwise operations that can be encoded as UIFs (e.g., [&](x, y) on int, or x * y under uif_ops), the casts that have no interpretation, and associated refinements. (Whether a hidden function is revealed, or an operation is uninterpreted, depends on the item being checked, so those are candidates that are filtered when encoding the axiom.) Applications mentioning variables bound inside the body (by a let or a quantifier) are skipped as they are not valid outside of their binder.

Fails if some variable bound by the axiom does not occur in any of the patterns, as the axiom could then never be instantiated.

Trait Implementations

impl TypeFoldable for Axiom

fn try_fold_with<__F: FallibleTypeFolder>( &self, __folder: &mut __F, ) -> Result<Self, __F::Error>

fn fold_with<F: TypeFolder>(&self, folder: &mut F) -> Self

fn reduce(&self, genv: GlobalEnv<'_, '_>) -> Self

Reduces expressions by

fn replace_holes( &self, f: impl FnMut(&[BoundVariableKinds], HoleKind) -> Expr, ) -> Self

Replaces all holes with the result of calling a closure. The closure takes a list with all the layers of bound variables at the point the hole was found. Each layer corresponds to the list of bound variables at that level. The list is ordered from outermost to innermost binder, i.e., the last element is the binder closest to the hole.

fn with_holes(&self) -> Self

Remove all refinements and turn each underlying BaseTy into a TyKind::Exists with a TyKind::Constr and a hole. For example, Vec<{v. i32[v] | v > 0}>[n] becomes {n. Vec<{v. i32[v] | *}>[n] | *}.

fn replace_evars( &self, f: &mut impl FnMut(EVid) -> Option<Expr>, ) -> Result<Self, EVid>

fn shift_horizontally(&self, amount: usize) -> Self

Shift the BoundVar of all the the variables at index INNERMOST “horizontally” to the right by the specified amount.

fn shift_in_escaping(&self, amount: u32) -> Self

fn shift_out_escaping(&self, amount: u32) -> Self

fn erase_regions(&self) -> Self

fn erase_regions_including_bound(&self) -> Self

Like TypeFoldable::erase_regions, but also erases bound regions.

impl TypeVisitable for Axiom

fn visit_with<__V: TypeVisitor>( &self, __visitor: &mut __V, ) -> ControlFlow<__V::BreakTy>

fn has_escaping_bvars(&self) -> bool

fn has_escaping_bvars_at_or_above(&self, binder: DebruijnIndex) -> bool

Returns true if self has any late-bound vars that are either bound by binder or bound by some binder outside of binder. If binder is ty::INNERMOST, this indicates whether there are any late-bound vars that appear free.

fn fvars(&self) -> FxHashSet<Name>

Returns the set of all free variables. For example, Vec<i32[n]>{v : v > m} returns {n, m}.

fn early_params(&self) -> FxHashSet<EarlyReftParam>

fn redundant_bvars(&self) -> UnordSet<BoundVar>

Gives the indices of the provided bvars which: