Struct NormalizeInfo

pub struct NormalizeInfo {
    pub body: Binder<Expr>,
    pub inline: bool,
    pub rank: usize,
}

This type represents what we know about a flux-def after normalization, i.e. after “inlining” all or some transitively called flux-defs.

• When FLUX_SMT_DEFINE_FUN=1 is set we inline all polymorphic flux-defs, since they cannot be represented as define-fun in SMTLIB but leave all monomorphic flux-defs un-inlined.
• When the above flag is not set, we replace every flux-def with its (transitively) inlined body

Fields

body: Binder<Expr>

the actual definition, with the Binder representing the parameters

inline: bool

whether or not this function is inlined (i.e. NOT represented as define-fun)

rank: usize

the rank of this defn in the topological sort of all the flux-defs, needed so we can specify the define-fun in the correct order, without any “forward” dependencies which the SMT solver cannot handle

Trait Implementations

impl Clone for NormalizeInfo

fn clone(&self) -> NormalizeInfo

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<__D: TyDecoder> Decodable<__D> for NormalizeInfo

fn decode(__decoder: &mut __D) -> Self

impl<__E: TyEncoder> Encodable<__E> for NormalizeInfo

fn encode(&self, __encoder: &mut __E)