Struct cop::lean::Contrapositive

pub struct Contrapositive<'t, L, V> {
    pub contra: Contrapositive<&'t L>,
    pub vars: Option<V>,
}

Clausal contrapositive for a literal lit with some inferred information about it.

This is usually produced by super::Matrix::contrapositives.

Fields

contra: Contrapositive<&'t L>

the actual contrapositive, i.e. the clause containing lit minus lit

vars: Option<V>

the maximum variable of the clause

Implementations

impl<'t, P: Clone, C, V> Contrapositive<'t, Lit<P, C, V>, V>

pub fn db_entry(self) -> (P, Self)

Convert the contrapositive into a form that allows it to be inserted into the database.

Trait Implementations

impl<'t, L: Debug, V: Debug> Debug for Contrapositive<'t, L, V>

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

Formats the value using the given formatter.

impl<'t, L: Display, V> Display for Contrapositive<'t, L, V>

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

Formats the value using the given formatter.