Struct Clause 

pub struct Clause {
    pub literals: Vec<Literal>,
}

A clause is a disjunction of literals: L₁ ∨ L₂ ∨ ... ∨ Lₙ.

Special cases:

• Empty clause (∅): contradiction, no literals
• Unit clause: single literal
• Horn clause: at most one positive literal

Fields

literals: Vec<Literal>

The literals in this clause (disjunction)

Implementations

impl Clause

pub fn from_literals(literals: Vec<Literal>) -> Self

Create a new clause from a list of literals.

pub fn empty() -> Self

Create an empty clause (contradiction).

pub fn unit(literal: Literal) -> Self

Create a unit clause (single literal).

pub fn is_empty(&self) -> bool

Check if this is the empty clause (contradiction).

pub fn is_unit(&self) -> bool

Check if this is a unit clause (single literal).

pub fn is_horn(&self) -> bool

Check if this is a Horn clause (at most one positive literal).

pub fn len(&self) -> usize

Get the number of literals in this clause.

pub fn is_len_zero(&self) -> bool

Check if clause is empty (different from is_empty which checks for contradiction).

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

Get all free variables in this clause.

pub fn subsumes(&self, other: &Clause) -> bool

Check if this clause subsumes another (is more general).

Theta-Subsumption: Clause C subsumes D (C ⪯ D) if there exists a substitution θ such that Cθ ⊆ D.

This means C is more general than D. For example:

• {P(x)} subsumes {P(a), Q(a)} with θ = {x/a}
• {P(x), Q(x)} subsumes {P(a), Q(a), R(a)} with θ = {x/a}

Implementation

We try to find a substitution by:

1. For each literal in C, try to unify it with some literal in D
2. Check if all substitutions are consistent
3. If successful, C subsumes D

Examples

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

// {P(x)} subsumes {P(a)}
let c = Clause::unit(Literal::positive(TLExpr::pred("P", vec![Term::var("x")])));
let d = Clause::unit(Literal::positive(TLExpr::pred("P", vec![Term::constant("a")])));
assert!(c.subsumes(&d));

// {P(a)} does not subsume {P(x)} (x is more general than a)
assert!(!d.subsumes(&c));

impl Clause

pub fn is_tautology(&self) -> bool

Check if this clause is tautology (contains complementary literals).

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

Apply a substitution to this clause.

This creates a new clause with the substitution applied to all literals.

pub fn rename_variables(&self, suffix: &str) -> Clause

Rename all variables in this clause with a suffix.

This is used for standardizing apart clauses before resolution to avoid variable name conflicts.

Example

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

// P(x) ∨ Q(x)
let p_x = Literal::positive(TLExpr::pred("P", vec![Term::var("x")]));
let q_x = Literal::positive(TLExpr::pred("Q", vec![Term::var("x")]));
let clause = Clause::from_literals(vec![p_x, q_x]);

// Rename to P(x_1) ∨ Q(x_1)
let renamed = clause.rename_variables("1");

Trait Implementations

impl Clone for Clause

fn clone(&self) -> Clause

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Clause

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Clause

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

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for Clause

fn eq(&self, other: &Clause) -> 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 Clause

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 Clause