Struct FixpointCtxt

pub struct FixpointCtxt<'genv, 'tcx, T: Eq + Hash> {
    comments: Vec<String>,
    genv: GlobalEnv<'genv, 'tcx>,
    kvars: KVarGen,
    scx: SortEncodingCtxt,
    kcx: KVarEncodingCtxt,
    ecx: ExprEncodingCtxt<'genv, 'tcx>,
    tags: IndexVec<TagIdx, T>,
    tags_inv: UnordMap<T, TagIdx>,
    def_id: MaybeExternId,
}

Fields

comments: Vec<String>

genv: GlobalEnv<'genv, 'tcx>

kvars: KVarGen

scx: SortEncodingCtxt

kcx: KVarEncodingCtxt

ecx: ExprEncodingCtxt<'genv, 'tcx>

tags: IndexVec<TagIdx, T>

tags_inv: UnordMap<T, TagIdx>

def_id: MaybeExternId

DefId of the item being checked. This can be a function/method or an adt when checking invariants.

Implementations

impl<'genv, 'tcx, Tag> FixpointCtxt<'genv, 'tcx, Tag>

where Tag: Hash + Eq + Copy,

pub fn new( genv: GlobalEnv<'genv, 'tcx>, def_id: MaybeExternId, kvars: KVarGen, ) -> Self

pub fn check( self, cache: &mut FixQueryCache, constraint: Constraint, scrape_quals: bool, solver: SmtSolver, ) -> QueryResult<Vec<Tag>>

fn run_task_with_cache( task: Task, key: String, cache: &mut FixQueryCache, ) -> FixpointResult<TagIdx>

fn tag_idx(&mut self, tag: Tag) -> TagIdx

where Tag: Debug,

pub(crate) fn with_name_map<R>( &mut self, name: Name, f: impl FnOnce(&mut Self, LocalVar) -> R, ) -> R

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

pub(crate) fn var_to_fixpoint(&self, var: &Var) -> Var

pub(crate) fn head_to_fixpoint( &mut self, expr: &Expr, mk_tag: impl Fn(Option<ESpan>) -> Tag + Copy, ) -> QueryResult<Constraint>

where Tag: Debug,

Encodes an expression in head position as a fixpoint::Constraint “peeling out” implications and foralls.

pub(crate) fn assumption_to_fixpoint( &mut self, pred: &Expr, ) -> QueryResult<(Vec<Bind>, Pred)>

Encodes an expression in assumptive position as a fixpoint::Pred. Returns the encoded predicate and a list of bindings produced by ANF-ing kvars.

fn assumption_to_fixpoint_aux( &mut self, expr: &Expr, bindings: &mut Vec<Bind>, preds: &mut Vec<Pred>, ) -> QueryResult

Auxiliary function to merge nested conjunctions in a single predicate

fn kvar_to_fixpoint( &mut self, kvar: &KVar, bindings: &mut Vec<Bind>, ) -> QueryResult<Pred>

fn def_span(&self) -> Span