tensorlogic-ir 0.1.0

Intermediate representation (IR) and AST types for TensorLogic
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150

//! Theta-subsumption tests for [`super::Clause`].

use super::*;

#[test]
fn test_subsumption_identical() {
    // {P(a)} subsumes {P(a)} (same clause)
    let p_a = Literal::positive(TLExpr::pred("P", vec![Term::constant("a")]));
    let c = Clause::unit(p_a);

    assert!(c.subsumes(&c));
}

#[test]
fn test_subsumption_variable_to_constant() {
    // {P(x)} subsumes {P(a)} with θ = {x/a}
    let p_x = Literal::positive(TLExpr::pred("P", vec![Term::var("x")]));
    let p_a = Literal::positive(TLExpr::pred("P", vec![Term::constant("a")]));

    let c_general = Clause::unit(p_x);
    let c_specific = Clause::unit(p_a);

    assert!(c_general.subsumes(&c_specific));
}

#[test]
fn test_subsumption_not_reverse() {
    // {P(a)} does NOT subsume {P(x)} (constant is less general than variable)
    let p_x = Literal::positive(TLExpr::pred("P", vec![Term::var("x")]));
    let p_a = Literal::positive(TLExpr::pred("P", vec![Term::constant("a")]));

    let c_general = Clause::unit(p_x);
    let c_specific = Clause::unit(p_a);

    assert!(!c_specific.subsumes(&c_general));
}

#[test]
fn test_subsumption_smaller_clause() {
    // {P(x)} subsumes {P(a), Q(a)} with θ = {x/a}
    let p_x = Literal::positive(TLExpr::pred("P", vec![Term::var("x")]));
    let p_a = Literal::positive(TLExpr::pred("P", vec![Term::constant("a")]));
    let q_a = Literal::positive(TLExpr::pred("Q", vec![Term::constant("a")]));

    let c1 = Clause::unit(p_x);
    let c2 = Clause::from_literals(vec![p_a, q_a]);

    assert!(c1.subsumes(&c2));
}

#[test]
fn test_subsumption_multiple_literals() {
    // {P(x), Q(x)} subsumes {P(a), Q(a), R(a)} with θ = {x/a}
    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 c1 = Clause::from_literals(vec![p_x, q_x]);

    let p_a = Literal::positive(TLExpr::pred("P", vec![Term::constant("a")]));
    let q_a = Literal::positive(TLExpr::pred("Q", vec![Term::constant("a")]));
    let r_a = Literal::positive(TLExpr::pred("R", vec![Term::constant("a")]));
    let c2 = Clause::from_literals(vec![p_a, q_a, r_a]);

    assert!(c1.subsumes(&c2));
}

#[test]
fn test_subsumption_fails_different_pred() {
    // {P(x)} does not subsume {Q(a)} (different predicate names)
    let p_x = Literal::positive(TLExpr::pred("P", vec![Term::var("x")]));
    let q_a = Literal::positive(TLExpr::pred("Q", vec![Term::constant("a")]));

    let c1 = Clause::unit(p_x);
    let c2 = Clause::unit(q_a);

    assert!(!c1.subsumes(&c2));
}

#[test]
fn test_subsumption_fails_too_many_literals() {
    // {P(x), Q(x), R(x)} does not subsume {P(a), Q(a)} (c1 has more literals)
    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 r_x = Literal::positive(TLExpr::pred("R", vec![Term::var("x")]));
    let c1 = Clause::from_literals(vec![p_x, q_x, r_x]);

    let p_a = Literal::positive(TLExpr::pred("P", vec![Term::constant("a")]));
    let q_a = Literal::positive(TLExpr::pred("Q", vec![Term::constant("a")]));
    let c2 = Clause::from_literals(vec![p_a, q_a]);

    assert!(!c1.subsumes(&c2));
}

#[test]
fn test_subsumption_empty_clause() {
    // Empty clause only subsumes itself
    let empty = Clause::empty();
    let p_a = Literal::positive(TLExpr::pred("P", vec![Term::constant("a")]));
    let non_empty = Clause::unit(p_a);

    assert!(empty.subsumes(&empty));
    assert!(!empty.subsumes(&non_empty));
    assert!(!non_empty.subsumes(&empty));
}

#[test]
fn test_subsumption_polarity_matters() {
    // {P(x)} does not subsume {¬P(a)} (different polarity)
    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 c1 = Clause::unit(p_x);
    let c2 = Clause::unit(not_p_a);

    assert!(!c1.subsumes(&c2));
}

#[test]
fn test_subsumption_two_variables() {
    // {P(x, y)} subsumes {P(a, b)} with θ = {x/a, y/b}
    let p_xy = Literal::positive(TLExpr::pred("P", vec![Term::var("x"), Term::var("y")]));
    let p_ab = Literal::positive(TLExpr::pred(
        "P",
        vec![Term::constant("a"), Term::constant("b")],
    ));

    let c1 = Clause::unit(p_xy);
    let c2 = Clause::unit(p_ab);

    assert!(c1.subsumes(&c2));
}

#[test]
fn test_subsumption_in_prover() {
    // Test that subsumption is actually used in the prover to reduce search space
    let mut prover = ResolutionProver::new();

    // Add {P(x), Q(x)} - more general
    let p_x = Literal::positive(TLExpr::pred("P", vec![Term::var("x")]));
    let q_x = Literal::positive(TLExpr::pred("Q", vec![Term::var("x")]));
    prover.add_clause(Clause::from_literals(vec![p_x, q_x]));

    // This clause would be subsumed by the first
    let p_a = Literal::positive(TLExpr::pred("P", vec![Term::constant("a")]));
    let q_a = Literal::positive(TLExpr::pred("Q", vec![Term::constant("a")]));
    let r_a = Literal::positive(TLExpr::pred("R", vec![Term::constant("a")]));
    let subsumed_clause = Clause::from_literals(vec![p_a, q_a, r_a]);

    // Check if subsumption works
    assert!(prover.clauses[0].subsumes(&subsumed_clause));
}