nx_sine.nx source
↩ module page · 216 lines · 7815 B
1// nx_sine.nx -- Sine (Sumo INference Engine) axiom selection.
2//
3// Per Vampire-displacement roadmap Phase 2. Critical for the CASC
4// LTB (Large Theory Batch) division -- problems may have thousands
5// of axioms but the conjecture only needs a few dozen. Sine picks
6// the relevant subset before saturation, often shrinking the search
7// space by 100x or more.
8//
9// Hoder + Voronkov 2011 standard formulation:
10//
11// tolerance T (typically 1.0 to 3.0)
12// For each symbol s in the problem, count freq(s) = number of
13// axioms containing s.
14//
15// For each symbol s, the "D-relation" picks definitional axioms:
16// d(s) = { axiom A : s ∈ symbols(A)
17// ∧ freq(s) ≤ T * min { freq(t) : t ∈ symbols(A) } }
18//
19// Selection algorithm (fixpoint):
20// selected = ∅
21// queue = symbols(conjecture)
22// while queue not empty:
23// s = pop(queue)
24// for each A in d(s) not in selected:
25// add A to selected
26// add new symbols of A to queue
27// return selected
28//
29// Output: subset of axioms reachable from the conjecture's symbols
30// through definition chains.
31//
32// Bits-up nx_int, no f64. tolerance is Q10 (1024 = 1.0).
33
34// nx_safety_envelope:
35// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
36// sil_target: SIL1
37// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
38// verdict: NOT_YET_EVALUATED
39
40import "nx_syscalls.nx"
41import "nx_runtime.nx"
42import "nx_tier.nx"
43import "nx_result.nx"
44import "nx_unify.nx"
45import "nx_resolution.nx"
46const NX_MAGIC_9223372036854775807: i64 = 9223372036854775807
47const NX_MAGIC_1024: i64 = 1024
48
49const NX_SINE_MAX_SYMS: nx_int = 1024
50const NX_SINE_MAX_AXIOMS: nx_int = 512
51
52struct SineCtx {
53 sym_freq: *nx_int, // [NX_SINE_MAX_SYMS] -- # axioms containing each sym
54 sym_seen: *nx_int, // [NX_SINE_MAX_SYMS] -- 1 if seen at all
55 selected: *nx_int, // [NX_SINE_MAX_AXIOMS] -- 1 if axiom selected
56 queue: *nx_int, // sym ids to process
57 n_queue: nx_int,
58 queue_head: nx_int,
59 sym_in_queue: *nx_int, // [NX_SINE_MAX_SYMS] -- 1 if currently queued
60 tolerance_q10: nx_int,
61}
62
63const NX_SINE_CTX_BYTES: nx_int = 64
64
65// Walk a Term tree marking symbol occurrences in `seen`. Variables
66// don't count -- only constant / function / predicate symbols.
67func nx_sine_collect_term_syms(t: *Term, seen: *nx_int) {
68 if t.kind == NX_TERM_VAR { return }
69 if t.sym >= 0 {
70 if t.sym < NX_SINE_MAX_SYMS { seen[t.sym] = 1 }
71 }
72 if t.kind == NX_TERM_CONST { return }
73 var i: nx_int = 0
74 while i < t.n_args {
75 nx_sine_collect_term_syms(nx_term_arg(t, i), seen)
76 i = i + 1
77 }
78}
79
80// Mark all symbols appearing in clause `c`. `seen` is reset by caller
81// each call (per-clause or per-axiom semantics differ -- caller's
82// choice).
83func nx_sine_collect_clause_syms(c: *Clause, seen: *nx_int) {
84 var i: nx_int = 0
85 while i < c.n_lits {
86 let l: *Literal = nx_clause_lit_at(c, i)
87 nx_sine_collect_term_syms(l.atom, seen)
88 i = i + 1
89 }
90}
91
92// Build the symbol-frequency table over all axioms. freq[s] = number
93// of axioms in which s appears.
94func nx_sine_build_freq(ctx: *SineCtx, axioms: *Clause, n_axioms: nx_int) {
95 var i: nx_int = 0
96 while i < n_axioms {
97 // Reset per-axiom seen bitmap.
98 let local_seen: *nx_int = (sys_mmap((NX_SINE_MAX_SYMS * 8) as i64)) as *nx_int
99 let c: *Clause = ((axioms as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
100 nx_sine_collect_clause_syms(c, local_seen)
101 var s: nx_int = 0
102 while s < NX_SINE_MAX_SYMS {
103 if local_seen[s] == 1 {
104 ctx.sym_freq[s] = ctx.sym_freq[s] + 1
105 ctx.sym_seen[s] = 1
106 }
107 s = s + 1
108 }
109 i = i + 1
110 }
111}
112
113// True iff axiom `c` is a definer of `s` under the current tolerance:
114// s ∈ symbols(c) ∧ freq(s) ≤ tolerance * min_freq_in_c
115func nx_sine_is_definer(ctx: *SineCtx, c: *Clause, s: nx_int) -> nx_int {
116 let local_seen: *nx_int = (sys_mmap((NX_SINE_MAX_SYMS * 8) as i64)) as *nx_int
117 nx_sine_collect_clause_syms(c, local_seen)
118 if local_seen[s] == 0 { return 0 } // s not in clause
119
120 // Find min freq of symbols in c.
121 var min_freq: nx_int = NX_MAGIC_9223372036854775807 // i64 max
122 var i: nx_int = 0
123 while i < NX_SINE_MAX_SYMS {
124 if local_seen[i] == 1 {
125 if ctx.sym_freq[i] < min_freq { min_freq = ctx.sym_freq[i] }
126 }
127 i = i + 1
128 }
129 // freq(s) <= T * min_freq? In Q10: freq(s) * 1024 <= T_q10 * min_freq.
130 let lhs: nx_int = ctx.sym_freq[s] * NX_MAGIC_1024
131 let rhs: nx_int = ctx.tolerance_q10 * min_freq
132 if lhs <= rhs { return 1 }
133 return 0
134}
135
136// Add a symbol to the work queue if not already there.
137func nx_sine_enqueue(ctx: *SineCtx, s: nx_int) {
138 if s < 0 { return }
139 if s >= NX_SINE_MAX_SYMS { return }
140 if ctx.sym_in_queue[s] == 1 { return }
141 if ctx.n_queue >= NX_SINE_MAX_SYMS { return }
142 ctx.queue[ctx.n_queue] = s
143 ctx.n_queue = ctx.n_queue + 1
144 ctx.sym_in_queue[s] = 1
145}
146
147// Main entry: select axioms relevant to the conjecture.
148//
149// out_selected[i] = 1 iff axiom i is selected; caller pre-allocates
150// the array (size n_axioms).
151//
152// tolerance_q10: 1024 = 1.0 (strict definer; minimum-frequency only).
153// Higher values include more axioms (looser threshold).
154//
155// Returns: number of selected axioms.
156func nx_sine_select(axioms: *Clause, n_axioms: nx_int,
157 conjecture: *Clause,
158 tolerance_q10: nx_int,
159 out_selected: *nx_int) -> nx_int {
160 let ctx: *SineCtx = (sys_mmap(NX_SINE_CTX_BYTES as i64)) as *SineCtx
161 ctx.sym_freq = (sys_mmap((NX_SINE_MAX_SYMS * 8) as i64)) as *nx_int
162 ctx.sym_seen = (sys_mmap((NX_SINE_MAX_SYMS * 8) as i64)) as *nx_int
163 ctx.selected = out_selected
164 ctx.queue = (sys_mmap((NX_SINE_MAX_SYMS * 8) as i64)) as *nx_int
165 ctx.n_queue = 0
166 ctx.queue_head = 0
167 ctx.sym_in_queue = (sys_mmap((NX_SINE_MAX_SYMS * 8) as i64)) as *nx_int
168 ctx.tolerance_q10 = tolerance_q10
169
170 // Step 1: build frequency table.
171 nx_sine_build_freq(ctx, axioms, n_axioms)
172
173 // Step 2: seed queue with conjecture symbols.
174 let conj_seen: *nx_int = (sys_mmap((NX_SINE_MAX_SYMS * 8) as i64)) as *nx_int
175 nx_sine_collect_clause_syms(conjecture, conj_seen)
176 var s: nx_int = 0
177 while s < NX_SINE_MAX_SYMS {
178 if conj_seen[s] == 1 { nx_sine_enqueue(ctx, s) }
179 s = s + 1
180 }
181
182 // Step 3: fixpoint loop.
183 while ctx.queue_head < ctx.n_queue {
184 let cur: nx_int = ctx.queue[ctx.queue_head]
185 ctx.queue_head = ctx.queue_head + 1
186
187 // For each axiom, check if it's a definer of cur.
188 var i: nx_int = 0
189 while i < n_axioms {
190 if out_selected[i] == 0 {
191 let c: *Clause = ((axioms as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
192 if nx_sine_is_definer(ctx, c, cur) == 1 {
193 out_selected[i] = 1
194 // Add new symbols of c to queue.
195 let ax_seen: *nx_int = (sys_mmap((NX_SINE_MAX_SYMS * 8) as i64)) as *nx_int
196 nx_sine_collect_clause_syms(c, ax_seen)
197 var t: nx_int = 0
198 while t < NX_SINE_MAX_SYMS {
199 if ax_seen[t] == 1 { nx_sine_enqueue(ctx, t) }
200 t = t + 1
201 }
202 }
203 }
204 i = i + 1
205 }
206 }
207
208 // Count selected.
209 var count: nx_int = 0
210 var k: nx_int = 0
211 while k < n_axioms {
212 if out_selected[k] == 1 { count = count + 1 }
213 k = k + 1
214 }
215 return count
216}