nx_hyperres.nx source
↩ module page · 126 lines · 5098 B
1// nx_hyperres.nx -- N-electron hyperresolution.
2//
3// Per Vampire-displacement roadmap Phase 2. Generalization of binary
4// resolution: combine one nucleus clause with N "electron" clauses in
5// a single inference step. Each electron contributes one positive
6// literal that resolves with one chosen negative literal of the
7// nucleus, all under a composed unifier.
8//
9// Robinson + Wos 1965 standard formulation:
10//
11// Nucleus: C ∨ ~a_1 ∨ ~a_2 ∨ ... ∨ ~a_n
12// Electrons: E_i ∨ b_i (one per i, b_i positive)
13// Unifier: σ = compose(unify(a_1,b_1), unify(a_2,b_2), ...)
14// Derive: (C ∨ E_1 ∨ E_2 ∨ ... ∨ E_n)σ
15//
16// where C is the residual non-consumed part of the nucleus and each
17// E_i is the residual non-consumed part of electron i.
18//
19// API: caller picks the consumed literals by index. Each negative
20// literal in nucleus targeted at neg_indices[i] is paired with the
21// positive literal in electrons[i] at pos_indices[i]. Variable
22// renaming across input clauses is the caller's responsibility
23// (matches nx_resolve's contract).
24//
25// Bits-up nx_int. Result-typed for fallible API.
26
27// nx_safety_envelope:
28// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
29// sil_target: SIL1
30// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
31// verdict: NOT_YET_EVALUATED
32
33import "nx_syscalls.nx"
34import "nx_runtime.nx"
35import "nx_tier.nx"
36import "nx_result.nx"
37import "nx_unify.nx"
38import "nx_resolution.nx"
39
40const NX_HYPERRES_MAX_ELECTRONS: nx_int = 16
41
42// True iff index `i` appears in the consumed-indices array.
43func nx_hyper_is_consumed(consumed: *nx_int, n: nx_int, i: nx_int) -> nx_int {
44 var k: nx_int = 0
45 while k < n {
46 if consumed[k] == i { return 1 }
47 k = k + 1
48 }
49 return 0
50}
51
52// Main entry. c_out is caller-allocated; populated with the
53// hyperresolvent. Returns Result<n_lits, NX_ERR_*>:
54// NX_ERR_OUT_OF_RANGE -- bad index
55// NX_ERR_TAG_MISMATCH -- nucleus's chosen literal not negative,
56// or electron's chosen literal not positive
57// NX_ERR_INVALID_STATE -- electron count exceeds capacity, or one
58// of the unifications failed
59func nx_hyperresolve(nucleus: *Clause,
60 neg_indices: *nx_int, n_neg: nx_int,
61 electrons: *Clause,
62 pos_indices: *nx_int, n_electrons: nx_int,
63 c_out: *Clause) -> *NxResult {
64 if n_neg != n_electrons { return nx_result_err(NX_ERR_INVALID_STATE) }
65 if n_electrons > NX_HYPERRES_MAX_ELECTRONS { return nx_result_err(NX_ERR_INVALID_STATE) }
66
67 // Bounds + polarity validation; collect handles for all consumed
68 // literals up front so the unification phase can run linearly.
69 var i: nx_int = 0
70 while i < n_electrons {
71 if neg_indices[i] < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
72 if neg_indices[i] >= nucleus.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
73 if pos_indices[i] < 0 { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
74
75 let elec: *Clause = ((electrons as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
76 if pos_indices[i] >= elec.n_lits { return nx_result_err(NX_ERR_OUT_OF_RANGE) }
77
78 let nlit: *Literal = nx_clause_lit_at(nucleus, neg_indices[i])
79 if nlit.sign != NX_LIT_NEG { return nx_result_err(NX_ERR_TAG_MISMATCH) }
80
81 let plit: *Literal = nx_clause_lit_at(elec, pos_indices[i])
82 if plit.sign != NX_LIT_POS { return nx_result_err(NX_ERR_TAG_MISMATCH) }
83
84 i = i + 1
85 }
86
87 // Compose the unifier across all (nucleus_neg, electron_pos) pairs.
88 let s: *Subst = nx_subst_new()
89 var j: nx_int = 0
90 while j < n_electrons {
91 let elec_j: *Clause = ((electrons as nx_int) + (j * NX_CLAUSE_BYTES)) as *Clause
92 let nl: *Literal = nx_clause_lit_at(nucleus, neg_indices[j])
93 let pl: *Literal = nx_clause_lit_at(elec_j, pos_indices[j])
94 let r: *NxResult = nx_unify(nl.atom, pl.atom, s)
95 if nx_result_is_err(r) == 1 { return r }
96 j = j + 1
97 }
98
99 // Build resolvent: residual nucleus + each electron's residual,
100 // all under sigma.
101 var k: nx_int = 0
102 while k < nucleus.n_lits {
103 if nx_hyper_is_consumed(neg_indices, n_neg, k) == 0 {
104 let lk: *Literal = nx_clause_lit_at(nucleus, k)
105 let lk_sub: *Literal = nx_lit_apply_subst(lk, s)
106 let _ra: *NxResult = nx_clause_add(c_out, lk_sub)
107 }
108 k = k + 1
109 }
110 var e: nx_int = 0
111 while e < n_electrons {
112 let elec_e: *Clause = ((electrons as nx_int) + (e * NX_CLAUSE_BYTES)) as *Clause
113 var m: nx_int = 0
114 while m < elec_e.n_lits {
115 if m != pos_indices[e] {
116 let lm: *Literal = nx_clause_lit_at(elec_e, m)
117 let lm_sub: *Literal = nx_lit_apply_subst(lm, s)
118 let _rb: *NxResult = nx_clause_add(c_out, lm_sub)
119 }
120 m = m + 1
121 }
122 e = e + 1
123 }
124
125 return nx_result_ok(c_out.n_lits)
126}