Struct Dbm 

pub struct Dbm<B: Bound, L: Layout<B> = LinearLayout<B>> { /* private fields */ }

An implementation of Zone as difference bound matrix.

Uses LinearLayout as the default storage layout.

Trait Implementations

impl<B: Clone + Bound, L: Clone + Layout<B>> Clone for Dbm<B, L>

fn clone(&self) -> Dbm<B, L>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<B: Debug + Bound, L: Debug + Layout<B>> Debug for Dbm<B, L>

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

Formats the value using the given formatter.

impl<B: Hash + Bound, L: Hash + Layout<B>> Hash for Dbm<B, L>

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<B: PartialEq + Bound, L: PartialEq + Layout<B>> PartialEq for Dbm<B, L>

fn eq(&self, other: &Dbm<B, L>) -> 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<B: Bound, L: Layout<B>> Zone for Dbm<B, L>

type Bound = B

fn new_unconstrained(num_variables: usize) -> Self

Constructs a new zone without any constraints besides clocks being positive.

fn new_zero(num_variables: usize) -> Self

Constructs a new zone where all clocks are set to zero.

fn with_constraints<U>(num_variables: usize, constraints: U) -> Self

where U: IntoIterator<Item = Constraint<B>>,

Constructs a new zone from the given iterable of constraints.

fn num_variables(&self) -> usize

Returns the number of clock variables of this zone.

fn num_clocks(&self) -> usize

Returns the number of clocks of this zone.

fn get_bound(&self, left: impl AnyClock, right: impl AnyClock) -> &B

Retrieves the difference bound for left - right.

fn is_empty(&self) -> bool

Checks whether the zone is empty.

fn add_constraint(&mut self, constraint: Constraint<B>)

Adds a constraint to the zone.

fn add_constraints<U>(&mut self, constraints: U)

where U: IntoIterator<Item = Constraint<B>>,

Adds all constraints from the given iterable to the zone.

fn intersect(&mut self, other: &Self)

Intersects two zones.

fn future(&mut self)

Computes the future of the zone by removing all upper bounds.

fn past(&mut self)

Computes the past of the zone by removing all lower bounds.

fn reset(&mut self, clock: Variable, value: B::Constant)

Resets the given clock variable to the specified constant.

fn is_unbounded(&self, clock: impl AnyClock) -> bool

Checks whether the value of the given clock is unbounded.

fn get_upper_bound(&self, clock: impl AnyClock) -> Option<B::Constant>

Returns the upper bound for the value of the given clock.

fn get_lower_bound(&self, clock: impl AnyClock) -> Option<B::Constant>

Returns the lower bound for the value of the given clock.

fn is_satisfied(&self, constraint: Constraint<B>) -> bool

Checks whether the given constraint is satisfied by the zone.

fn includes(&self, other: &Self) -> bool

Checks whether the zone includes the other zone.

fn resize(&self, num_variables: usize) -> Self

Creates a resized copy of the zone by adding or removing clocks.

impl<B: Eq + Bound, L: Eq + Layout<B>> Eq for Dbm<B, L>

impl<B: Bound, L: Layout<B>> StructuralPartialEq for Dbm<B, L>