Struct Cursor

pub struct Cursor<'a> {
    tree: &'a mut RefineTree,
    ptr: NodePtr,
}

A cursor into the refinement tree. More specifically, a Cursor represents a path from the root to some internal node in a refinement tree.

Fields

tree: &'a mut RefineTree

ptr: NodePtr

Implementations

impl<'a> Cursor<'a>

pub(crate) fn move_to( &mut self, marker: &Marker, clear_children: bool, ) -> Option<Cursor<'_>>

Moves the cursor to the specified marker. If clear_children is true, all children of the node are removed after moving the cursor, invalidating any markers pointing to a node within those children.

pub(crate) fn marker(&self) -> Marker

Returns a marker to the current node

pub(crate) fn branch(&mut self) -> Cursor<'_>

pub(crate) fn vars(&self) -> impl Iterator<Item = (Var, Sort)>

pub(crate) fn push_trace(&mut self, trace: TypeTrace)

pub(crate) fn define_var(&mut self, sort: &Sort) -> Name

Defines a fresh refinement variable with the given sort and advance the cursor to the new node. It returns the freshly generated name for the variable.

pub(crate) fn assume_pred(&mut self, pred: impl Into<Expr>)

Pushes an assumption and moves the cursor into the new node.

pub(crate) fn check_pred(&mut self, pred: impl Into<Expr>, tag: Tag)

Pushes a predicate that must be true assuming variables and predicates in the current branch of the tree (i.e., it pushes a NodeKind::Head). This methods does not advance the cursor.

pub(crate) fn check_impl( &mut self, pred1: impl Into<Expr>, pred2: impl Into<Expr>, tag: Tag, )

Convenience method to push an assumption followed by a predicate that needs to be checked. This method does not advance the cursor.

pub(crate) fn hoister( &mut self, assume_invariants: AssumeInvariants, ) -> Hoister<Unpacker<'_, 'a>>

pub(crate) fn assume_invariants(&mut self, ty: &Ty, overflow_checking: bool)

Trait Implementations

impl Debug for Cursor<'_>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Pretty for Cursor<'_>

fn fmt(&self, cx: &PrettyCx<'_, '_>, f: &mut Formatter<'_>) -> Result

fn default_cx(tcx: TyCtxt<'_>) -> PrettyCx<'_, '_>