Struct KVarEncodingCtxt 

struct KVarEncodingCtxt {
    ranges: FxIndexMap<KVid, Range<KVid>>,
}

During encoding into fixpoint we generate multiple fixpoint kvars per kvar in flux. A KVarEncodingCtxt is used to keep track of the state needed for this.

See KVarEncoding

Fields

ranges: FxIndexMap<KVid, Range<KVid>>

A map from a rty::KVid to the range of fixpoint::KVids that will be used to encode it.

Implementations

impl KVarEncodingCtxt

fn declare(&mut self, kvid: KVid, decl: &KVarDecl) -> Range<KVid>

Declares that a kvar has to be encoded into fixpoint and assigns a range of fixpoint::KVid’s to it.

fn encode_kvars( &self, kvars: &KVarGen, scx: &mut SortEncodingCtxt, ) -> Vec<KVarDecl>

fn group_kvar_solution( &self, items: Vec<(KVid, Binder<Expr>)>, ) -> HashMap<KVid, Binder<Expr>>

For each rty::KVid $k, this function collects all predicates associated with the fixpoint::KVids that encode $k and combines them into a single predicate by conjoining them.

A group (i.e., a combined predicate) is included in the result only if all fixpoint::KVids in the encoding range of $k are present in the input.

Trait Implementations

impl Default for KVarEncodingCtxt

fn default() -> KVarEncodingCtxt

Returns the “default value” for a type.