Struct Node 

struct Node {
    kind: NodeKind,
    nbindings: usize,
    parent: Option<WeakNodePtr>,
    children: Vec<NodePtr>,
}

Fields

kind: NodeKind

nbindings: usize

Number of bindings between the root and this node’s parent, i.e., we have as an invariant that nbindings equals the number of NodeKind::ForAll nodes from the parent of this node to the root.

parent: Option<WeakNodePtr>

children: Vec<NodePtr>

Implementations

impl Node

fn simplify( &mut self, phase: SimplifyPhase<'_, '_>, assumed_preds: &mut SnapshotMap<Expr, ()>, )

fn is_leaf(&self) -> bool

fn replace_evars(&mut self, evars: &EVarStore) -> Result<(), EVid>

fn to_fixpoint( &self, cx: &mut FixpointCtxt<'_, '_, Tag>, ) -> QueryResult<Option<Constraint>>

fn is_forall(&self) -> bool

Returns true if the node kind is ForAll.

fn is_head(&self) -> bool

Returns true if the node kind is Head.

impl Node

fn simplify_bot(&mut self)

replace bot-kvars with false

fn simplify_top(&mut self)

replace top-kvars with true

fn simplify_with_assignment(&mut self, assignment: &Assignment)

simplifies assumptions and heads using the TOP/BOT kvar assignment; follow with a call to simplify to delete constraints with FALSE assm.