Struct mm0_util::Modifiers

pub struct Modifiers { /* fields omitted */ }

Visibility and sort modifiers for Sort statements and Declarations.

Implementations

impl Modifiers

pub const PURE: Modifiers

The pure sort modifier, used to indicate that term constructors can not target this sort.

pub const STRICT: Modifiers

The strict sort modifier, used to indicate that bound variables (in the sense of [LocalKind::is_bound]) of this sort are not allowed.

pub const PROVABLE: Modifiers

The provable sort modifier, used to indicate that this sort can appear as the sort of hypotheses and conclusions of axiom and theorem declarations.

pub const FREE: Modifiers

The free sort modifier, used to indicate that dummy variables of this sort (in def and theorem) are not allowed.

pub const PUB: Modifiers

The pub visibility modifier, used on theorem to indicate that a theorem appears in the specification file (otherwise the theorem is only usable in the proof file).

pub const ABSTRACT: Modifiers

The abstract visibility modifier, used on def to indicate that the definition should not be supplied in the specification file.

pub const LOCAL: Modifiers

The local visibility modifier, the opposite of pub and used on def, because defs have default public visibility. A local def will not appear in the specification file at all.

pub const fn empty() -> Modifiers

Returns an empty set of flags

pub const fn all() -> Modifiers

Returns the set containing all flags.

pub const fn bits(&self) -> u8

Returns the raw value of the flags currently stored.

pub fn from_bits(bits: u8) -> Option<Modifiers>

Convert from underlying bit representation, unless that representation contains bits that do not correspond to a flag.

pub const fn from_bits_truncate(bits: u8) -> Modifiers

Convert from underlying bit representation, dropping any bits that do not correspond to flags.

pub const unsafe fn from_bits_unchecked(bits: u8) -> Modifiers

Convert from underlying bit representation, preserving all bits (even those not corresponding to a defined flag).

pub const fn is_empty(&self) -> bool

Returns true if no flags are currently stored.

pub const fn is_all(&self) -> bool

Returns true if all flags are currently set.

pub const fn intersects(&self, other: Modifiers) -> bool

Returns true if there are flags common to both self and other.

pub const fn contains(&self, other: Modifiers) -> bool

Returns true all of the flags in other are contained within self.

pub fn insert(&mut self, other: Modifiers)

Inserts the specified flags in-place.

pub fn remove(&mut self, other: Modifiers)

Removes the specified flags in-place.

pub fn toggle(&mut self, other: Modifiers)

Toggles the specified flags in-place.

pub fn set(&mut self, other: Modifiers, value: bool)

Inserts or removes the specified flags depending on the passed value.

impl Modifiers

pub const NONE: Modifiers

The null modifier set. Modifiers are represented as bitfields, so this is the same as 0.

#[must_use]

pub fn new(bits: u8) -> Self

Construct a Modifiers from a byte.

#[must_use]

pub fn sort_data() -> Modifiers

The set of all valid sort modifiers. One can check if a modifier set is valid for a sort using sort_data().contains(m).

#[must_use]

pub fn from_name(s: &[u8]) -> Modifiers

Parses a string into a singleton Modifiers, or NONE if the string is not valid.

Trait Implementations

impl Binary for Modifiers

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

Formats the value using the given formatter.

impl BitAnd<Modifiers> for Modifiers

type Output = Modifiers

The resulting type after applying the & operator.

fn bitand(self, other: Modifiers) -> Modifiers

Returns the intersection between the two sets of flags.

impl BitAndAssign<Modifiers> for Modifiers

fn bitand_assign(&mut self, other: Modifiers)

Disables all flags disabled in the set.

impl BitOr<Modifiers> for Modifiers

type Output = Modifiers

The resulting type after applying the | operator.

fn bitor(self, other: Modifiers) -> Modifiers

Returns the union of the two sets of flags.

impl BitOrAssign<Modifiers> for Modifiers

fn bitor_assign(&mut self, other: Modifiers)

Adds the set of flags.

impl BitXor<Modifiers> for Modifiers

type Output = Modifiers

The resulting type after applying the ^ operator.

fn bitxor(self, other: Modifiers) -> Modifiers

Returns the left flags, but with all the right flags toggled.

impl BitXorAssign<Modifiers> for Modifiers

fn bitxor_assign(&mut self, other: Modifiers)

Toggles the set of flags.

impl Clone for Modifiers

fn clone(&self) -> Modifiers

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Copy for Modifiers

impl Debug for Modifiers

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

Formats the value using the given formatter.

impl DeepSizeOf for Modifiers

fn deep_size_of_children(&self, _: &mut Context) -> usize

Returns an estimation of the heap-managed storage of this object. This does not include the size of the object itself.

pub fn deep_size_of(&self) -> usize

Returns an estimation of a total size of memory owned by the object, including heap-managed storage.

pub fn deep_size_of_with(&self, context: &mut Context) -> usize

Returns an estimation of a total size of memory owned by the object, including heap-managed storage.

impl Display for Modifiers

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

Formats the value using the given formatter.

impl Eq for Modifiers

impl Extend<Modifiers> for Modifiers

fn extend<T: IntoIterator<Item = Modifiers>>(&mut self, iterator: T)

Extends a collection with the contents of an iterator.

pub fn extend_one(&mut self, item: A)

🔬 This is a nightly-only experimental API. (extend_one)

Extends a collection with exactly one element.

pub fn extend_reserve(&mut self, additional: usize)

🔬 This is a nightly-only experimental API. (extend_one)

Reserves capacity in a collection for the given number of additional elements.

impl FromIterator<Modifiers> for Modifiers

fn from_iter<T: IntoIterator<Item = Modifiers>>(iterator: T) -> Modifiers

Creates a value from an iterator.

impl Hash for Modifiers

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

Feeds this value into the given Hasher.

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

Feeds a slice of this type into the given Hasher.

impl LowerHex for Modifiers

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

Formats the value using the given formatter.

impl Not for Modifiers

type Output = Modifiers

The resulting type after applying the ! operator.

fn not(self) -> Modifiers

Returns the complement of this set of flags.

impl Octal for Modifiers

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

Formats the value using the given formatter.

impl Ord for Modifiers

fn cmp(&self, other: &Modifiers) -> Ordering

This method returns an Ordering between self and other.

#[must_use]

pub fn max(self, other: Self) -> Self

Compares and returns the maximum of two values.

#[must_use]

pub fn min(self, other: Self) -> Self

Compares and returns the minimum of two values.

#[must_use]

pub fn clamp(self, min: Self, max: Self) -> Self

Restrict a value to a certain interval.

impl PartialEq<Modifiers> for Modifiers

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

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

impl PartialOrd<Modifiers> for Modifiers

fn partial_cmp(&self, other: &Modifiers) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

#[must_use]

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

This method tests less than (for self and other) and is used by the < operator.

#[must_use]

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

This method tests less than or equal to (for self and other) and is used by the <= operator.

#[must_use]

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

This method tests greater than (for self and other) and is used by the > operator.

#[must_use]

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

This method tests greater than or equal to (for self and other) and is used by the >= operator.

impl StructuralEq for Modifiers

impl StructuralPartialEq for Modifiers

impl Sub<Modifiers> for Modifiers

type Output = Modifiers

The resulting type after applying the - operator.

fn sub(self, other: Modifiers) -> Modifiers

Returns the set difference of the two sets of flags.

impl SubAssign<Modifiers> for Modifiers

fn sub_assign(&mut self, other: Modifiers)

Disables all flags enabled in the set.

impl UpperHex for Modifiers

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

Formats the value using the given formatter.