Enum cop::LitMat

pub enum LitMat<L, M> {
    Lit(L),
    Mat(M),
}

A litmat is either a literal or a matrix.

This is used for nonclausal proof search.

Variants

Lit(L)

literal

Mat(M)

matrix

Implementations

impl<P: Clone, C: Clone, V: Clone> LitMat<Lit<Signed<P>, C, V>, Matrix<Lit<Signed<P>, C, V>, V>>

pub fn positive(&self) -> Option<Self>

A litmat is positive if it is a negative literal or if it is a non-empty positive matrix.

impl<L, M> LitMat<L, M>

pub fn lit(self) -> Option<L>

Return literal if the litmat is one.

impl<P, C, V, M> LitMat<Lit<P, C, V>, M>

pub fn is_ground(&self) -> bool

A litmat is ground if it is a ground literal.

Trait Implementations

impl<L: Clone, M: Clone> Clone for LitMat<L, M>

fn clone(&self) -> LitMat<L, M>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<L: Debug, M: Debug> Debug for LitMat<L, M>

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

Formats the value using the given formatter.

impl<L: Display, M: Display> Display for LitMat<L, M>

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

Formats the value using the given formatter.