Struct SortEncodingCtxt 

pub struct SortEncodingCtxt {
    tuples: UnordSet<usize>,
    adt_sorts: FxIndexSet<DefId>,
    user_sorts: FxIndexSet<FluxDefId>,
}

Keep track of all the data sorts that we need to define in fixpoint to encode the constraint.

Fields

tuples: UnordSet<usize>

Set of all the tuple arities that need to be defined

adt_sorts: FxIndexSet<DefId>

Set of all the AdtDefSortDef that need to be declared as Fixpoint data-decls

user_sorts: FxIndexSet<FluxDefId>

Set of all opaque types that need to be defined

Implementations

impl SortEncodingCtxt

pub fn sort_to_fixpoint(&mut self, sort: &Sort) -> Sort

fn func_sort_to_fixpoint(&mut self, fsort: &PolyFuncSort) -> Sort

fn declare_tuple(&mut self, arity: usize)

pub fn declare_opaque_sort(&mut self, def_id: FluxDefId)

pub fn declare_adt(&mut self, did: DefId) -> AdtId

pub fn user_sorts_to_fixpoint( &mut self, genv: GlobalEnv<'_, '_>, ) -> Vec<SortDecl>

fn append_adt_decls( &mut self, genv: GlobalEnv<'_, '_>, decls: &mut Vec<DataDecl>, ) -> QueryResult

fn append_tuple_decls(tuples: &UnordSet<usize>, decls: &mut Vec<DataDecl>)

pub fn encode_data_decls( &mut self, genv: GlobalEnv<'_, '_>, ) -> QueryResult<Vec<DataDecl>>

Trait Implementations

impl Default for SortEncodingCtxt

fn default() -> SortEncodingCtxt

Returns the “default value” for a type.