Module fixpoint_encoding 

Encoding of the refinement tree into a fixpoint constraint.

Modules

decoding

fixpoint

Structs

Answer

ConstEnv 🔒

ExprEncodingCtxt

FixpointCtxt

KVarDecl 🔒

KVarEncodingCtxt 🔒

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.

KVarGen

KVarSolutions

KvarSolutionTrace

LocalVarEnv 🔒

Environment used to map from rty::Var to a fixpoint::LocalVar.

ParsedResult

SexpParseCtxt 🔒

SolutionTrace

A very explicit representation of Solution for debugging/tracing/serialization ONLY.

SortDeps

SortEncodingCtxt

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

TagIdx

Enums

Backend

ConstKey 🔒

KVarEncoding

How an rty::KVar is encoded in the fixpoint constraint

Functions

bv_size_to_fixpoint 🔒

const_to_fixpoint 🔒

mk_implies 🔒

parse_data_ctor 🔒

parse_data_proj 🔒

parse_global_var 🔒

parse_kvid 🔒

parse_local_var 🔒

parse_param 🔒

Type Aliases

ClosedSolution

ConstMap 🔒

FixQueryCache

FixpointSolution

FunDeclMap

Solution

A type to represent Solutions for KVars