Module refine_tree

Modules§

Cursor: A cursor into the refinement tree. More specifically, a Cursor represents a path from the root to some internal node in a refinement tree.
Marker: A marker is a pointer to a node in the refinement tree that can be used to query information about that node or to move the cursor. A marker may become invalid if the underlying node is cleared.
Node 🔒
NodePtr 🔒
ParentsIter 🔒
RcxBind 🔒
RefineCtxtTrace: An explicit representation of a path in the RefineTree used for debugging/tracing/serialization ONLY.
RefineTree: A refinement tree tracks the “tree-like structure” of refinement variables and predicates generated during refinement type-checking. This tree can be encoded as a fixpoint constraint whose satisfiability implies the safety of a function.
Scope: A list of refinement variables and their sorts.
WeakNodePtr 🔒