Struct cop::offset::Offset

pub struct Offset<T> { /* private fields */ }

An object with an usize offset for variables.

For example, when we want to create a fresh clause copy, instead of creating a new clause by applying an offset to every variable (taking linear time), we simply wrap a clause pointer with an Offset (taking constant time). This approach (wrapping objects in an Offset) also avoids mixing up offsets for different objects or forgetting to consider an offset.

A principal design idea of this type is that we should not be able to obtain the original, non-offset object once it is offset. This is to prevent that the offset is “forgotten”.

Implementations

impl<'t, P, C> Offset<&'t Contrapositive<&'t Lit<P, C, usize>>>

pub fn lit(&self) -> OLit<'t, P, C>

The literal corresponding to the contrapositive.

pub fn rest(&self) -> Offset<&'t Clause<&'t Lit<P, C, usize>>>

The clause minus the literal corresponding to the contrapositive.

impl<T> Offset<&T>

pub fn ptr_eq(self, other: Self) -> bool

Return true if the offsets and the pointers are equal.

impl<T: Copy> Offset<&T>

pub fn copied(self) -> Offset<T>

Copy the contained object.

impl<T> Offset<T>

pub fn new(o: usize, x: T) -> Offset<T>

Create a new offset object.

pub fn map<U>(self, f: impl FnOnce(T) -> U) -> Offset<U>

Apply a function to the contained object.

impl<'t, C> Offset<&'t Term<C, usize>>

pub fn whnf(self, sub: &Sub<'t, C>) -> Self

Substitute the head of the term until a fix point is reached.

let mut sub: Sub<&str> = Sub::default();
sub.set_dom_max(3);

let tm0: Term<&str, _> = Term::V(0);
let tm1: Term<&str, _> = Term::V(1);
let ot0 = OTerm::new(2, &tm0);
let ot1 = OTerm::new(0, &tm1);
sub.insert(2, ot1);

// 0+2 should be substituted to 1+0 and terminate there
assert!(ot0.whnf(&sub).ptr_eq(ot1))

impl<'t, C: Eq> Offset<&'t Args<Term<C, usize>>>

pub fn eq_mod(self, sub: &Sub<'t, C>, other: Self) -> bool

Return true if two offset argument sequences are equal modulo substitution.

pub fn unify(self, sub: &mut Sub<'t, C>, other: Self) -> bool

Return true if two offset argument sequences can be unified under the substitution, updating the substitution.

impl<'t, P, C> Offset<&'t App<P, Args<Term<C, usize>>>>

pub fn head(&self) -> &P

Head of the literal.

pub fn args(&self) -> OArgs<'t, C>

Offset arguments of the literal.

impl<'t, P: Eq, C: Eq> Offset<&'t App<P, Args<Term<C, usize>>>>

pub fn eq_mod(&self, sub: &Sub<'t, C>, other: &Self) -> bool

Return true if two offset literals are equal modulo substitution.

impl<'t, P: Eq + Neg<Output = P> + Clone, C: Eq> Offset<&'t App<P, Args<Term<C, usize>>>>

pub fn neg_eq_mod(&self, sub: &Sub<'t, C>, other: &Self) -> bool

Return true if the negation of an offset literals equals another offset literal, modulo substitution.

impl<'t, L, M> Offset<&'t LitMat<L, M>>

pub fn transpose(self) -> LitMat<Offset<&'t L>, Offset<&'t M>>

Propagate the offset of a litmat to its contained literal/matrix.

Trait Implementations

impl<T: Clone> Clone for Offset<T>

fn clone(&self) -> Offset<T>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<T: Debug> Debug for Offset<T>

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

Formats the value using the given formatter.

impl<'t, L> Display for Offset<&'t Clause<L>>where Offset<&'t L>: Display,

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

Formats the value using the given formatter.

impl<'t, P: Display, C: Display> Display for Offset<&'t Contrapositive<&'t Lit<P, C, usize>>>

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

Formats the value using the given formatter.

impl<'t, L: 't, M: 't> Display for Offset<&'t LitMat<L, M>>where Offset<&'t L>: Display, Offset<&'t M>: Display,

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

Formats the value using the given formatter.

impl<'t, C: 't> Display for Offset<&'t Matrix<C>>where Offset<&'t C>: Display,

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

Formats the value using the given formatter.

impl<'t, L: 't, V> Display for Offset<&'t VClause<L, V>>where Offset<&'t L>: Display,

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

Formats the value using the given formatter.

impl<T, I: IntoIterator<Item = T>> IntoIterator for Offset<I>

Convert an offset of a collection of Ts to a collection of offset Ts.

type Item = Offset<T>

The type of the elements being iterated over.

type IntoIter = Map<Zip<Repeat<usize>, <I as IntoIterator>::IntoIter>, fn(_: (usize, T)) -> Offset<T>>

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.

impl<T: Copy> Copy for Offset<T>