Module fixpoint_encoding

Encoding of the refinement tree into a fixpoint constraint.

Modules

fixpoint

Structs

ConstInfo 🔒

ExprEncodingCtxt 🔒

FixpointCtxt

FixpointKVar 🔒

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

LocalVarEnv 🔒

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

SortEncodingCtxt 🔒

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

TagIdx

Enums

KVarEncoding

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

Key 🔒

Functions

bv_size_to_fixpoint 🔒

const_to_fixpoint 🔒

mk_implies 🔒

Type Aliases

ConstMap 🔒

DefMap 🔒

FixQueryCache