Struct Literal 

pub struct Literal {
    pub atom: TLExpr,
    pub polarity: bool,
}

A literal is an atomic formula or its negation.

Fields

atom: TLExpr

The underlying atomic formula

polarity: bool

True if positive literal, false if negative

Implementations

impl Literal

pub fn positive(atom: TLExpr) -> Self

Create a positive literal from an atomic formula.

pub fn negative(atom: TLExpr) -> Self

Create a negative literal from an atomic formula.

pub fn negate(&self) -> Self

Negate this literal.

pub fn is_complementary(&self, other: &Literal) -> bool

Check if this literal is complementary to another (same atom, opposite polarity).

For ground literals (no variables), this checks exact equality.

pub fn try_unify(&self, other: &Literal) -> Option<Substitution>

Attempt to unify this literal with another for resolution.

Returns the most general unifier (MGU) if the atoms can be unified and the polarities are opposite.

This is used for first-order resolution with variables.

Examples

use tensorlogic_ir::{TLExpr, Term, Literal};

// P(x) and ¬P(a) can be unified with {x/a}
let p_x = Literal::positive(TLExpr::pred("P", vec![Term::var("x")]));
let not_p_a = Literal::negative(TLExpr::pred("P", vec![Term::constant("a")]));

let mgu = p_x.try_unify(&not_p_a);
assert!(mgu.is_some());

pub fn apply_substitution(&self, subst: &Substitution) -> Literal

Apply a substitution to this literal.

This creates a new literal with the substitution applied to all terms.

pub fn is_positive(&self) -> bool

Check if this is a positive literal.

pub fn is_negative(&self) -> bool

Check if this is a negative literal.

pub fn free_vars(&self) -> HashSet<String>

Get the free variables in this literal.

Trait Implementations

impl Clone for Literal

fn clone(&self) -> Literal

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Literal

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Literal

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for Literal

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

Tests for self and other values to be equal, and is used by ==.

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

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for Literal

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for Literal