Struct Heap 

pub struct Heap {
    pub map: HashMap<u64, u64>,
}

A simple heap: a finite partial map from addresses to values.

Fields

map: HashMap<u64, u64>

Map from address to value.

Implementations

impl Heap

pub fn empty() -> Self

Create an empty heap.

pub fn singleton(addr: u64, val: u64) -> Self

Create a singleton heap {addr ↦ val}.

pub fn disjoint(&self, other: &Heap) -> bool

Check if two heaps have disjoint domains.

pub fn union(&self, other: &Heap) -> Option<Heap>

Union of two disjoint heaps.

pub fn size(&self) -> usize

Size of the heap (number of mapped addresses).

pub fn read(&self, addr: u64) -> Option<u64>

Read a value from the heap.

pub fn write(&self, addr: u64, val: u64) -> Heap

Write a value to the heap (returns a new heap).

pub fn sep_split<P, Q>(&self, p: P, q: Q) -> Option<(Heap, Heap)>

where P: Fn(&Heap) -> bool, Q: Fn(&Heap) -> bool,

Check separating conjunction: h ⊨ P * Q. Returns Some((h1, h2)) if h splits as h1 satisfying P and h2 satisfying Q.

Trait Implementations

impl Clone for Heap

fn clone(&self) -> Heap

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Heap

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

Formats the value using the given formatter.

impl PartialEq for Heap

fn eq(&self, other: &Heap) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Heap

impl StructuralPartialEq for Heap