Struct HeapPred 

pub struct HeapPred(/* private fields */);

A heap predicate: a set of heaps satisfying a property. Represented here as a Rust closure for simplicity.

Implementations

impl HeapPred

pub fn new(f: impl Fn(&Heap) -> bool + 'static) -> Self

Create a heap predicate from a closure.

pub fn satisfies(&self, h: &Heap) -> bool

Check whether a heap satisfies this predicate.

pub fn sep_star(p: HeapPred, q: HeapPred) -> HeapPred

Separating conjunction P ∗ Q.

pub fn emp() -> HeapPred

The emp predicate: satisfied only by the empty heap.

pub fn points_to(l: u64, v: u64) -> HeapPred

Points-to predicate: l ↦ v.