[−][src]Struct rate_common::clause::Clause
An index uniquely identifying a clause or lemma during the lifetime of the program
Fields
index: ClauseIdentifierType
Methods
impl Clause
[src]
pub fn new(index: ClauseIdentifierType) -> Clause
[src]
pub fn from_usize(index: usize) -> Clause
[src]
Create the clause index with the given usize ID.
Panics
Panics if the index exceeds the internal limit.
pub fn range(
start: impl Offset,
end: impl Offset
) -> impl Iterator<Item = Clause>
[src]
start: impl Offset,
end: impl Offset
) -> impl Iterator<Item = Clause>
Create an iterator from clause indices start
up to (excluding) end
.
pub const MAX_ID: ClauseIdentifierType
[src]
The maximum value a regular Clause
can assume.
pub const DOES_NOT_EXIST: Clause
[src]
We need one special value for deleted clauses that do not actually exist.
We cannot simply drop those deletions from the proof because sick-check
relies on the line in the proof.
pub const UNINITIALIZED: Clause
[src]
A special value for clause IDs. Used in places where we are sure that the value is written before being used as an actual clause ID.
Trait Implementations
impl Offset for Clause
[src]
impl Clone for Clause
[src]
impl Copy for Clause
[src]
impl Default for Clause
[src]
impl Eq for Clause
[src]
impl Ord for Clause
[src]
fn cmp(&self, other: &Clause) -> Ordering
[src]
fn max(self, other: Self) -> Self
1.21.0[src]
fn min(self, other: Self) -> Self
1.21.0[src]
fn clamp(self, min: Self, max: Self) -> Self
[src]
impl PartialEq<Clause> for Clause
[src]
impl PartialOrd<Clause> for Clause
[src]
fn partial_cmp(&self, other: &Clause) -> Option<Ordering>
[src]
fn lt(&self, other: &Clause) -> bool
[src]
fn le(&self, other: &Clause) -> bool
[src]
fn gt(&self, other: &Clause) -> bool
[src]
fn ge(&self, other: &Clause) -> bool
[src]
impl Display for Clause
[src]
impl Debug for Clause
[src]
impl Sub<u32> for Clause
[src]
type Output = Clause
The resulting type after applying the -
operator.
fn sub(self, value: ClauseIdentifierType) -> Clause
[src]
impl Add<Clause> for Clause
[src]
type Output = Clause
The resulting type after applying the +
operator.
fn add(self, rhs: Clause) -> Clause
[src]
impl Add<u32> for Clause
[src]
type Output = Clause
The resulting type after applying the +
operator.
fn add(self, value: ClauseIdentifierType) -> Clause
[src]
impl AddAssign<u32> for Clause
[src]
fn add_assign(&mut self, value: ClauseIdentifierType)
[src]
impl SubAssign<u32> for Clause
[src]
fn sub_assign(&mut self, value: ClauseIdentifierType)
[src]
impl Hash for Clause
[src]
Auto Trait Implementations
impl Send for Clause
impl Sync for Clause
impl Unpin for Clause
impl UnwindSafe for Clause
impl RefUnwindSafe for Clause
Blanket Implementations
impl<T> HeapSpace for T where
T: Copy,
[src]
T: Copy,
fn heap_space(&Self) -> usize
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> From<T> for T
[src]
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T> ToString for T where
T: Display + ?Sized,
[src]
T: Display + ?Sized,
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,