Struct ExprEncodingCtxt

struct ExprEncodingCtxt<'genv, 'tcx> {
    genv: GlobalEnv<'genv, 'tcx>,
    local_var_env: LocalVarEnv,
    global_var_gen: IndexGen<GlobalVar>,
    const_map: FxIndexMap<Key<'tcx>, ConstInfo>,
    def_map: FxIndexMap<FluxDefId, Var>,
    errors: Errors<'genv>,
    def_span: Span,
}

Fields

genv: GlobalEnv<'genv, 'tcx>

local_var_env: LocalVarEnv

global_var_gen: IndexGen<GlobalVar>

const_map: FxIndexMap<Key<'tcx>, ConstInfo>

def_map: FxIndexMap<FluxDefId, Var>

errors: Errors<'genv>

def_span: Span

Implementations

impl<'genv, 'tcx> ExprEncodingCtxt<'genv, 'tcx>

fn new(genv: GlobalEnv<'genv, 'tcx>, def_span: Span) -> Self

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

fn variant_to_fixpoint( &self, scx: &mut SortEncodingCtxt, enum_def_id: &DefId, idx: VariantIdx, ) -> Expr

fn fields_to_fixpoint( &mut self, flds: &[Expr], scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn expr_to_fixpoint( &mut self, expr: &Expr, scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn exprs_to_fixpoint<'b>( &mut self, exprs: impl IntoIterator<Item = &'b Expr>, scx: &mut SortEncodingCtxt, ) -> QueryResult<Vec<Expr>>

fn proj_to_fixpoint( &mut self, e: &Expr, proj: FieldProj, scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn un_op_to_fixpoint( &mut self, op: UnOp, e: &Expr, scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn bv_rel_to_fixpoint(&self, rel: &BinRel) -> Expr

fn bv_op_to_fixpoint(&self, op: &BinOp) -> Expr

fn bin_op_to_fixpoint( &mut self, op: &BinOp, e1: &Expr, e2: &Expr, scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

fn bin_rel_to_fixpoint( &mut self, sort: &Sort, rel: BinRel, e1: &Expr, e2: &Expr, scx: &mut SortEncodingCtxt, ) -> QueryResult<Expr>

A binary relation is encoded as a structurally recursive relation between aggregate sorts. For “leaf” expressions, we encode them as an interpreted relation if the sort supports it, otherwise we use an uninterpreted function. For example, consider the following relation between two tuples of sort (int, int -> int)

(0, λv. v + 1) <= (1, λv. v + 1)

The encoding in fixpoint will be

0 <= 1 && (le (λv. v + 1) (λv. v + 1))

Where <= is the (interpreted) less than or equal relation between integers and le is an uninterpreted relation between (the encoding of) lambdas.

fn apply_bin_rel_rec( &mut self, sorts: &[Sort], rel: BinRel, e1: &Expr, e2: &Expr, scx: &mut SortEncodingCtxt, mk_proj: impl Fn(u32) -> FieldProj, ) -> QueryResult<Expr>

Apply binary relation recursively over aggregate expressions

fn imm( &mut self, arg: &Expr, sort: &Sort, scx: &mut SortEncodingCtxt, bindings: &mut Vec<Bind>, ) -> QueryResult<Var>

fn register_def(&mut self, def_id: FluxDefId) -> Var

fn register_uif(&mut self, def_id: FluxDefId, scx: &mut SortEncodingCtxt) -> Var

fn register_rust_const( &mut self, def_id: DefId, scx: &mut SortEncodingCtxt, info: &ConstantInfo, ) -> Var

fn register_const_for_alias_reft( &mut self, alias_reft: &AliasReft, fsort: FuncSort, scx: &mut SortEncodingCtxt, ) -> Var

returns the ‘constant’ UIF for Var used to represent the alias_pred, creating and adding it to the const_map if necessary

fn register_const_for_lambda( &mut self, lam: &Lambda, scx: &mut SortEncodingCtxt, ) -> Var

We encode lambdas with uninterpreted constant. Two syntactically equal lambdas will be encoded with the same constant.

fn assume_const_values( &mut self, constraint: Constraint, scx: &mut SortEncodingCtxt, ) -> QueryResult<Constraint>

fn qualifiers_for( &mut self, def_id: LocalDefId, scx: &mut SortEncodingCtxt, ) -> QueryResult<Vec<Qualifier>>

fn define_funs( &mut self, def_id: LocalDefId, scx: &mut SortEncodingCtxt, ) -> QueryResult<(Vec<FunDecl>, Vec<ConstDecl>)>

fn body_to_fixpoint( &mut self, body: &Binder<Expr>, scx: &mut SortEncodingCtxt, ) -> QueryResult<(Vec<(Var, Sort)>, Expr)>

fn qualifier_to_fixpoint( &mut self, qualifier: &Qualifier, scx: &mut SortEncodingCtxt, ) -> QueryResult<Qualifier>