nx_subsumption.nx source
↩ module page · 91 lines · 3534 B
1// nx_subsumption.nx -- forward subsumption for clause sets.
2//
3// Per Vampire-displacement roadmap Phase 1 step 2: clause C subsumes
4// clause D iff there exists a substitution sigma such that for every
5// literal Lc in C, there is a literal Ld in D with the same polarity
6// AND Lc[sigma] = Ld. When C subsumes D, D is redundant and can be
7// dropped from the passive set -- this is the single biggest pruner
8// in saturation provers.
9//
10// Algorithm: backtracking match. For each literal of C in order, try
11// every same-polarity literal of D as a match candidate. Snapshot
12// substitution length before each attempt; on failure, roll back by
13// resetting s.n. Subst bindings are append-only (see nx_unify), so
14// truncating restores the prior state exactly.
15//
16// One-way matching (nx_match) is required, not full unification --
17// only C's variables get bound; D is treated as fixed.
18//
19// Bits-up nx_int, Result-typed errors via underlying primitives,
20// scale-agnostic via nx_tier.
21
22// nx_safety_envelope:
23// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
24// sil_target: SIL1
25// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
26// verdict: NOT_YET_EVALUATED
27
28import "nx_syscalls.nx"
29import "nx_runtime.nx"
30import "nx_tier.nx"
31import "nx_result.nx"
32import "nx_unify.nx"
33import "nx_resolution.nx"
34
35// Sealed verdict. Subsumption is genuinely binary -- there is no
36// "incomparable" case the way there is for KBO.
37const NX_SUBSUMES_YES: nx_int = 1
38const NX_SUBSUMES_NO: nx_int = 0
39
40// Recursive backtracking entry: try to match C[c_idx..] against D
41// using accumulated substitution s. Returns 1 if subsumed, 0 if not.
42func nx_subsumes_from(c: *Clause, c_idx: nx_int,
43 d: *Clause, s: *Subst) -> nx_int {
44 // Base case: matched all of C -- subsumes.
45 if c_idx >= c.n_lits { return NX_SUBSUMES_YES }
46
47 let lc: *Literal = nx_clause_lit_at(c, c_idx)
48
49 var j: nx_int = 0
50 while j < d.n_lits {
51 let ld: *Literal = nx_clause_lit_at(d, j)
52 if lc.sign == ld.sign {
53 // Snapshot subst state for rollback.
54 let snapshot: nx_int = s.n
55 let r: *NxResult = nx_match(lc.atom, ld.atom, s)
56 if nx_result_is_err(r) == 0 {
57 // Match succeeded; recurse on the next literal of C.
58 if nx_subsumes_from(c, c_idx + 1, d, s) == NX_SUBSUMES_YES {
59 return NX_SUBSUMES_YES
60 }
61 }
62 // Rollback: drop any bindings added by this trial.
63 s.n = snapshot
64 }
65 j = j + 1
66 }
67 return NX_SUBSUMES_NO
68}
69
70// Forward subsumption: does clause c subsume clause d?
71//
72// Optimization: |C| > |D| -> impossible (each Lc must hit a distinct
73// or shared Ld; matching a literal can't create new ones). Strictly
74// the count check is for the multiset case; in propositional / FO
75// without duplicate literals it's also a valid early reject.
76func nx_subsumes(c: *Clause, d: *Clause) -> nx_int {
77 if c.n_lits == 0 {
78 // Empty clause subsumes everything (vacuous; useful for the
79 // tautology-deletion pipeline).
80 return NX_SUBSUMES_YES
81 }
82 if c.n_lits > d.n_lits { return NX_SUBSUMES_NO }
83 let s: *Subst = nx_subst_new()
84 return nx_subsumes_from(c, 0, d, s)
85}
86
87func nx_subsumes_verdict_name(v: nx_int) -> *u8 {
88 if v == NX_SUBSUMES_YES { return "SUBSUMES" as *u8 }
89 if v == NX_SUBSUMES_NO { return "NOT_SUBSUMES" as *u8 }
90 return "?" as *u8
91}