Struct SortCstr 

pub struct SortCstr(<SortCstr as PublicFlags>::Internal);

A sort constraint is a set of operations a sort must support.

During sort checking, we accumulate the operations required for each sort variable. As unification progresses, these constraints become more specific, i.e, a sort must support more operations to satisfy them.

Tuple Fields

0: <SortCstr as PublicFlags>::Internal

Implementations

impl SortCstr

pub const BOT: Self

An empty constraint (any sort satisfies it)

pub const MUL: Self

*

pub const DIV: Self

/

pub const MOD: Self

%

pub const ADD: Self

+

pub const SUB: Self

-

pub const BIT_OR: Self

|

pub const BIT_AND: Self

&

pub const BIT_SHL: Self

>>

pub const BIT_SHR: Self

<<

pub const BIT_XOR: Self

^

pub const NUMERIC: Self

The set of operations supported by all numeric sorts.

pub const INT: Self

The set of operations supported by integers.

pub const REAL: Self

The set of operations supported by reals.

pub const BITVEC: Self

The set of operations supported by bit vectors.

pub const SET: Self

The set of operations supported by sets.

impl SortCstr

pub const fn empty() -> Self

Get a flags value with all bits unset.

pub const fn all() -> Self

Get a flags value with all known bits set.

pub const fn bits(&self) -> u16

Get the underlying bits value.

The returned value is exactly the bits set in this flags value.

pub const fn from_bits(bits: u16) -> Option<Self>

Convert from a bits value.

This method will return None if any unknown bits are set.

pub const fn from_bits_truncate(bits: u16) -> Self

Convert from a bits value, unsetting any unknown bits.

pub const fn from_bits_retain(bits: u16) -> Self

Convert from a bits value exactly.

pub fn from_name(name: &str) -> Option<Self>

Get a flags value with the bits of a flag with the given name set.

This method will return None if name is empty or doesn’t correspond to any named flag.

pub const fn is_empty(&self) -> bool

Whether all bits in this flags value are unset.

pub const fn is_all(&self) -> bool

Whether all known bits in this flags value are set.

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

Whether any set bits in a source flags value are also set in a target flags value.

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

Whether all set bits in a source flags value are also set in a target flags value.

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

The bitwise or (|) of the bits in two flags values.

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

The intersection of a source flags value with the complement of a target flags value (&!).

This method is not equivalent to self & !other when other has unknown bits set. remove won’t truncate other, but the ! operator will.

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

The bitwise exclusive-or (^) of the bits in two flags values.

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

Call insert when value is true or remove when value is false.

pub const fn intersection(self, other: Self) -> Self

The bitwise and (&) of the bits in two flags values.

pub const fn union(self, other: Self) -> Self

The bitwise or (|) of the bits in two flags values.

pub const fn difference(self, other: Self) -> Self

The intersection of a source flags value with the complement of a target flags value (&!).

This method is not equivalent to self & !other when other has unknown bits set. difference won’t truncate other, but the ! operator will.

pub const fn symmetric_difference(self, other: Self) -> Self

The bitwise exclusive-or (^) of the bits in two flags values.

pub const fn complement(self) -> Self

The bitwise negation (!) of the bits in a flags value, truncating the result.

impl SortCstr

pub const fn iter(&self) -> Iter<SortCstr>

Yield a set of contained flags values.

Each yielded flags value will correspond to a defined named flag. Any unknown bits will be yielded together as a final flags value.

pub const fn iter_names(&self) -> IterNames<SortCstr>

Yield a set of contained named flags values.

This method is like iter, except only yields bits in contained named flags. Any unknown bits, or bits not corresponding to a contained flag will not be yielded.

impl SortCstr

pub fn from_bin_op(op: BinOp) -> Self

Returns a constraint that only requires the specified binary operation.

fn satisfy(self, sort: &Sort) -> bool

Returns whether a sort satisfies this constraint

Trait Implementations

impl Binary for SortCstr

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

Formats the value using the given formatter.

impl BitAnd for SortCstr

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

The bitwise and (&) of the bits in two flags values.

type Output = SortCstr

The resulting type after applying the & operator.

impl BitAndAssign for SortCstr

fn bitand_assign(&mut self, other: Self)

The bitwise and (&) of the bits in two flags values.

impl BitOr for SortCstr

fn bitor(self, other: SortCstr) -> Self

The bitwise or (|) of the bits in two flags values.

type Output = SortCstr

The resulting type after applying the | operator.

impl BitOrAssign for SortCstr

fn bitor_assign(&mut self, other: Self)

The bitwise or (|) of the bits in two flags values.

impl BitXor for SortCstr

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

The bitwise exclusive-or (^) of the bits in two flags values.

type Output = SortCstr

The resulting type after applying the ^ operator.

impl BitXorAssign for SortCstr

fn bitxor_assign(&mut self, other: Self)

The bitwise exclusive-or (^) of the bits in two flags values.

impl Clone for SortCstr

fn clone(&self) -> SortCstr

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SortCstr

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

Formats the value using the given formatter.

impl Extend<SortCstr> for SortCstr

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

The bitwise or (|) of the bits in each flags value.

fn extend_one(&mut self, item: A)

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

Extends a collection with exactly one element.

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 Flags for SortCstr

const FLAGS: &'static [Flag<SortCstr>]

The set of defined flags.

type Bits = u16

The underlying bits type.

fn bits(&self) -> u16

Get the underlying bits value.

fn from_bits_retain(bits: u16) -> SortCstr

Convert from a bits value exactly.

fn empty() -> Self

Get a flags value with all bits unset.

fn all() -> Self

Get a flags value with all known bits set.

fn contains_unknown_bits(&self) -> bool

This method will return true if any unknown bits are set.

fn from_bits(bits: Self::Bits) -> Option<Self>

Convert from a bits value.

fn from_bits_truncate(bits: Self::Bits) -> Self

Convert from a bits value, unsetting any unknown bits.

fn from_name(name: &str) -> Option<Self>

Get a flags value with the bits of a flag with the given name set.

fn iter(&self) -> Iter<Self>

Yield a set of contained flags values.

fn iter_names(&self) -> IterNames<Self>

Yield a set of contained named flags values.

fn is_empty(&self) -> bool

Whether all bits in this flags value are unset.

fn is_all(&self) -> bool

Whether all known bits in this flags value are set.

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

where Self: Sized,

Whether any set bits in a source flags value are also set in a target flags value.

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

where Self: Sized,

Whether all set bits in a source flags value are also set in a target flags value.

fn truncate(&mut self)

where Self: Sized,

Remove any unknown bits from the flags.

fn insert(&mut self, other: Self)

where Self: Sized,

The bitwise or (|) of the bits in two flags values.

fn remove(&mut self, other: Self)

where Self: Sized,

The intersection of a source flags value with the complement of a target flags value (&!).

fn toggle(&mut self, other: Self)

where Self: Sized,

The bitwise exclusive-or (^) of the bits in two flags values.

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

where Self: Sized,

Call [Flags::insert] when value is true or [Flags::remove] when value is false.

fn clear(&mut self)

where Self: Sized,

Unsets all bits in the flags.

fn intersection(self, other: Self) -> Self

The bitwise and (&) of the bits in two flags values.

fn union(self, other: Self) -> Self

The bitwise or (|) of the bits in two flags values.

fn difference(self, other: Self) -> Self

The intersection of a source flags value with the complement of a target flags value (&!).

fn symmetric_difference(self, other: Self) -> Self

The bitwise exclusive-or (^) of the bits in two flags values.

fn complement(self) -> Self

The bitwise negation (!) of the bits in a flags value, truncating the result.

impl FromIterator<SortCstr> for SortCstr

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

The bitwise or (|) of the bits in each flags value.

impl Hash for SortCstr

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 IntoIterator for SortCstr

type Item = SortCstr

The type of the elements being iterated over.

type IntoIter = Iter<SortCstr>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl LowerHex for SortCstr

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

Formats the value using the given formatter.

impl Not for SortCstr

fn not(self) -> Self

The bitwise negation (!) of the bits in a flags value, truncating the result.

type Output = SortCstr

The resulting type after applying the ! operator.

impl Octal for SortCstr

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

Formats the value using the given formatter.

impl PartialEq for SortCstr

fn eq(&self, other: &SortCstr) -> 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 PublicFlags for SortCstr

type Primitive = u16

The type of the underlying storage.

type Internal = InternalBitFlags

The type of the internal field on the generated flags type.

impl Sub for SortCstr

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

The intersection of a source flags value with the complement of a target flags value (&!).

This method is not equivalent to self & !other when other has unknown bits set. difference won’t truncate other, but the ! operator will.

type Output = SortCstr

The resulting type after applying the - operator.

impl SubAssign for SortCstr

fn sub_assign(&mut self, other: Self)

The intersection of a source flags value with the complement of a target flags value (&!).

This method is not equivalent to self & !other when other has unknown bits set. difference won’t truncate other, but the ! operator will.

impl UpperHex for SortCstr

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

Formats the value using the given formatter.

impl Copy for SortCstr

impl Eq for SortCstr

impl StructuralPartialEq for SortCstr