Struct SortEncodingCtxt

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

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

Implementations

impl SortEncodingCtxt

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_adt(&mut self, did: DefId) -> AdtId

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

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

fn into_data_decls(self, genv: GlobalEnv<'_, '_>) -> QueryResult<Vec<DataDecl>>

Trait Implementations

impl Default for SortEncodingCtxt

fn default() -> SortEncodingCtxt

Returns the “default value” for a type.