nx_tautology.nx source
↩ module page · 77 lines · 2844 B
1// nx_tautology.nx -- syntactic tautology detection on clauses.
2//
3// Per Vampire-displacement roadmap Phase 1 step 4. A clause is a
4// tautology when its truth is forced regardless of interpretation;
5// such clauses add nothing to the search space and are dropped
6// before they enter the passive set.
7//
8// Two patterns recognised here:
9// (a) Reflexive equality: + eq(t, t) for any term t.
10// (b) Propositional pair: contains both +L and -L over identical atoms.
11//
12// Equality predicate symbol id is a parameter -- the caller (TPTP
13// parser, kernel API) names whichever sym_id "=" was registered
14// under. Avoids a magic constant baked into substrate.
15//
16// Sealed verdict {NX_TAUTOLOGY, NX_NOT_TAUTOLOGY}. This is the
17// purely syntactic check; semantic tautology detection (E-resolution
18// across equivalent atoms) is a Phase 2 extension.
19
20// nx_safety_envelope:
21// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
22// sil_target: SIL1
23// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
24// verdict: NOT_YET_EVALUATED
25
26import "nx_syscalls.nx"
27import "nx_runtime.nx"
28import "nx_tier.nx"
29import "nx_result.nx"
30import "nx_unify.nx"
31import "nx_resolution.nx"
32
33const NX_TAUTOLOGY: nx_int = 1
34const NX_NOT_TAUTOLOGY: nx_int = 0
35
36// Returns 1 iff the literal is +eq(t, t) for some t -- i.e. a positive
37// equality with syntactically identical sides under the chosen
38// equality symbol id.
39func nx_lit_is_reflexive_eq(l: *Literal, eq_sym: nx_int) -> nx_int {
40 if l.sign != NX_LIT_POS { return 0 }
41 if l.atom.kind != NX_TERM_APP { return 0 }
42 if l.atom.sym != eq_sym { return 0 }
43 if l.atom.n_args != 2 { return 0 }
44 let lhs: *Term = nx_term_arg(l.atom, 0)
45 let rhs: *Term = nx_term_arg(l.atom, 1)
46 return nx_term_eq(lhs, rhs)
47}
48
49// Main entry: O(n^2) over clause length, which is fine for clauses
50// of typical bounded size (NX_CLAUSE_MAX_LITS = 64 in nx_resolution).
51func nx_is_tautology(c: *Clause, eq_sym: nx_int) -> nx_int {
52 var i: nx_int = 0
53 while i < c.n_lits {
54 let li: *Literal = nx_clause_lit_at(c, i)
55
56 // (a) reflexive equality
57 if nx_lit_is_reflexive_eq(li, eq_sym) == 1 { return NX_TAUTOLOGY }
58
59 // (b) propositional pair: scan for a complementary literal
60 var j: nx_int = i + 1
61 while j < c.n_lits {
62 let lj: *Literal = nx_clause_lit_at(c, j)
63 if li.sign == (0 - lj.sign) {
64 if nx_term_eq(li.atom, lj.atom) == 1 { return NX_TAUTOLOGY }
65 }
66 j = j + 1
67 }
68 i = i + 1
69 }
70 return NX_NOT_TAUTOLOGY
71}
72
73func nx_tautology_verdict_name(v: nx_int) -> *u8 {
74 if v == NX_TAUTOLOGY { return "TAUTOLOGY" as *u8 }
75 if v == NX_NOT_TAUTOLOGY { return "NOT_TAUTOLOGY" as *u8 }
76 return "?" as *u8
77}