Enum resolution_prover::ClausePart

pub enum ClausePart {
    Term(String),
    NegatedTerm(String),
}

A term or negated term that is part of a clause.

For example, p and ~q can be represented as the following.

let p = resolution_prover::ClausePart::Term("p".to_string());

let not_q = resolution_prover::ClausePart::NegatedTerm("q".to_string());

Variants

Term(String)NegatedTerm(String)

Methods

impl ClausePart

pub fn negate(&self) -> ClausePart

Returns the negated version of the clause part.

let clausePart = resolution_prover::ClausePart::Term("p".to_string());

let neg = clausePart.negate();

let expected_1 =
    resolution_prover::ClausePart::NegatedTerm("p".to_string());

assert_eq!(neg, expected_1);

let double_neg = neg.negate();

assert_eq!(double_neg, clausePart);

Trait Implementations

impl Clone for ClausePart

fn clone(&self) -> ClausePart

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for ClausePart

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

Formats the value using the given formatter.

impl Eq for ClausePart

impl Hash for ClausePart

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,

Feeds a slice of this type into the given [Hasher].

impl PartialEq for ClausePart

fn eq(&self, other: &ClausePart) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &ClausePart) -> bool

This method tests for !=.