nx_sine_test.nx source
↩ module page · 147 lines · 6520 B
1// nx_sine_test.nx -- Sine selection smoke.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_result.nx"
7import "nx_unify.nx"
8import "nx_resolution.nx"
9import "nx_sine.nx"
10
11const SYM_A: nx_int = 100
12const SYM_B: nx_int = 101
13const SYM_P: nx_int = 200
14const SYM_Q: nx_int = 201
15const SYM_R: nx_int = 202
16const SYM_S: nx_int = 203
17const SYM_X: nx_int = 204
18
19// Build atom with one constant arg.
20func mk_p(p_sym: nx_int, c_sym: nx_int) -> *Term {
21 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
22 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
23 return nx_term_app(p_sym, 1, arg)
24}
25
26// Single-literal positive clause.
27func mk_unit(atom: *Term) -> *Clause {
28 let c: *Clause = nx_clause_new()
29 let _r: *NxResult = nx_clause_add(c, nx_lit_make(NX_LIT_POS, atom))
30 return c
31}
32
33// Pack a clause into the i-th slot of a flat axiom array.
34func place(arr: *Clause, i: nx_int, src: *Clause) {
35 let dest: *Clause = ((arr as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
36 dest.n_lits = src.n_lits
37 dest.lits = src.lits
38}
39
40func main() -> nx_exit {
41 println("=== Sine selection smoke ===" as *u8)
42 var fails: nx_int = 0
43
44 // ---------- Test 1: directly relevant axioms get selected -----
45 // Axioms: a0 = {p(a)}, a1 = {q(a)}, a2 = {r(b)}
46 // Conjecture: {p(a) | q(a)} (uses p and q -- not r)
47 // Expected: a0, a1 selected; a2 NOT.
48 let axioms: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
49 place(axioms, 0, mk_unit(mk_p(SYM_P, SYM_A)))
50 place(axioms, 1, mk_unit(mk_p(SYM_Q, SYM_A)))
51 place(axioms, 2, mk_unit(mk_p(SYM_R, SYM_B)))
52
53 let conj1: *Clause = nx_clause_new()
54 let _rc1a: *NxResult = nx_clause_add(conj1, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
55 let _rc1b: *NxResult = nx_clause_add(conj1, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
56
57 let sel: *nx_int = (sys_mmap((10 * 8) as i64)) as *nx_int
58 let n_sel: nx_int = nx_sine_select(axioms, 3, conj1, 1024, sel)
59 print(" 1. {p,q,r-axioms}, conjecture uses p+q -> selected=" as *u8); print_i64(n_sel); println("" as *u8)
60 if n_sel == 2 {
61 if sel[0] == 1 {
62 if sel[1] == 1 {
63 if sel[2] == 0 {
64 println(" a0+a1 selected, a2 excluded PASS" as *u8)
65 } else { println(" a2 unexpectedly selected FAIL" as *u8); fails = fails + 1 }
66 } else { println(" a1 not selected FAIL" as *u8); fails = fails + 1 }
67 } else { println(" a0 not selected FAIL" as *u8); fails = fails + 1 }
68 } else { println(" wrong selection count FAIL" as *u8); fails = fails + 1 }
69
70 // ---------- Test 2: transitive selection through shared symbol -
71 // Axioms: a0 = {p(a)}, a1 = {p(a) | q(a)}, a2 = {q(a) | r(a)},
72 // a3 = {s(b)}
73 // Conjecture: {p(a)}
74 // Sine should: pick a0 (p direct). a0 has only p; q never gets
75 // triggered. a3 (s) excluded.
76 // The transitive case requires looser tolerance.
77 let axioms2: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
78 place(axioms2, 0, mk_unit(mk_p(SYM_P, SYM_A)))
79
80 let a1: *Clause = nx_clause_new()
81 let _r2a: *NxResult = nx_clause_add(a1, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
82 let _r2b: *NxResult = nx_clause_add(a1, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
83 place(axioms2, 1, a1)
84
85 let a2: *Clause = nx_clause_new()
86 let _r2c: *NxResult = nx_clause_add(a2, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
87 let _r2d: *NxResult = nx_clause_add(a2, nx_lit_make(NX_LIT_POS, mk_p(SYM_R, SYM_A)))
88 place(axioms2, 2, a2)
89
90 place(axioms2, 3, mk_unit(mk_p(SYM_S, SYM_B)))
91
92 let conj2: *Clause = mk_unit(mk_p(SYM_P, SYM_A))
93
94 let sel2: *nx_int = (sys_mmap((10 * 8) as i64)) as *nx_int
95 let n_sel2: nx_int = nx_sine_select(axioms2, 4, conj2, 2048, sel2) // tolerance 2.0
96 print(" 2. transitive p->q->r at T=2.0 -> selected=" as *u8); print_i64(n_sel2); println("" as *u8)
97 if sel2[3] == 0 {
98 println(" a3 (irrelevant s) excluded PASS" as *u8)
99 } else { println(" a3 incorrectly selected FAIL" as *u8); fails = fails + 1 }
100
101 // ---------- Test 3: empty conjecture symbols selects nothing --
102 // If conjecture has no symbols (e.g. only variables), nothing is
103 // selected.
104 let conj3: *Clause = nx_clause_new()
105 // Add a literal with only a variable -- no symbols counted.
106 let var_only: *Term = nx_term_var(SYM_X)
107 let _rc3: *NxResult = nx_clause_add(conj3, nx_lit_make(NX_LIT_POS, var_only))
108
109 let sel3: *nx_int = (sys_mmap((10 * 8) as i64)) as *nx_int
110 let n_sel3: nx_int = nx_sine_select(axioms, 3, conj3, 1024, sel3)
111 print(" 3. var-only conjecture -> selected=" as *u8); print_i64(n_sel3); println("" as *u8)
112 if n_sel3 == 0 {
113 println(" no axioms selected PASS" as *u8)
114 } else { println(" unexpected selection FAIL" as *u8); fails = fails + 1 }
115
116 // ---------- Test 4: tolerance widens definers ----------------
117 // Axioms: a0 = {p(a)}, a1 = {q(a)}, a2 = {p(a) | q(a)}
118 // freq(p) = 2, freq(q) = 2.
119 // Conjecture: {p(a)}.
120 // T=1.0: a0 is definer of p (min freq is 2, 2 <= 2*1.0). a2 also
121 // contains p with min_freq 2 -- 2 <= 2*1.0 so also a definer.
122 // Once a0 + a2 selected, q gets queued; a1 + a2 are q-definers.
123 // Result: all 3 selected.
124 let axioms4: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
125 place(axioms4, 0, mk_unit(mk_p(SYM_P, SYM_A)))
126 place(axioms4, 1, mk_unit(mk_p(SYM_Q, SYM_A)))
127 let a4_2: *Clause = nx_clause_new()
128 let _r4a: *NxResult = nx_clause_add(a4_2, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
129 let _r4b: *NxResult = nx_clause_add(a4_2, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
130 place(axioms4, 2, a4_2)
131
132 let conj4: *Clause = mk_unit(mk_p(SYM_P, SYM_A))
133 let sel4: *nx_int = (sys_mmap((10 * 8) as i64)) as *nx_int
134 let n_sel4: nx_int = nx_sine_select(axioms4, 3, conj4, 1024, sel4)
135 print(" 4. p,q symmetric T=1.0 -> selected=" as *u8); print_i64(n_sel4); println("" as *u8)
136 if n_sel4 == 3 {
137 println(" all 3 reached transitively PASS" as *u8)
138 } else { println(" unexpected count FAIL" as *u8); fails = fails + 1 }
139
140 println("" as *u8)
141 if fails == 0 {
142 println("=== ALL 4 Sine selection tests PASS ===" as *u8)
143 return 0
144 }
145 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
146 return 1
147}