nx_indexed_subsume_test.nx source
↩ module page · 107 lines · 4249 B
1// nx_indexed_subsume_test.nx -- discrim-tree-backed forward subsumption.
2// Verifies the indexed lookup gives the same answer as the linear scan.
3
4import "nx_syscalls.nx"
5import "nx_runtime.nx"
6import "nx_tier.nx"
7import "nx_result.nx"
8import "nx_unify.nx"
9import "nx_resolution.nx"
10import "nx_subsumption.nx"
11import "nx_tautology.nx"
12import "nx_disctree.nx"
13import "nx_saturation.nx"
14
15const SYM_A: nx_int = 100
16const SYM_B: nx_int = 101
17const SYM_P: nx_int = 200
18const SYM_Q: nx_int = 201
19const VAR_X: nx_int = 0
20
21func mk_p(p_sym: nx_int, c_sym: nx_int) -> *Term {
22 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
23 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
24 return nx_term_app(p_sym, 1, arg)
25}
26
27func mk_p_var(p_sym: nx_int, var_id: nx_int) -> *Term {
28 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
29 arg.kind = NX_TERM_VAR; arg.sym = var_id; arg.n_args = 0; arg.args = 0 as *Term
30 return nx_term_app(p_sym, 1, arg)
31}
32
33func mk_unit(atom: *Term) -> *Clause {
34 let c: *Clause = nx_clause_new()
35 let _r: *NxResult = nx_clause_add(c, nx_lit_make(NX_LIT_POS, atom))
36 return c
37}
38
39// Push a clause into processed and immediately index it.
40func push(s: *Saturation, c: *Clause) {
41 let _m: *NxResult = nx_sat_move_to_processed(s, c)
42 nx_sat_index_clause(s, s.n_processed - 1)
43}
44
45// Compare indexed vs linear lookup on a query clause.
46func compare(name: *u8, s: *Saturation, q: *Clause, expected: nx_int) -> nx_int {
47 let lin: nx_int = nx_sat_proc_subsumes(s, q)
48 let idx: nx_int = nx_sat_proc_subsumes_indexed(s, q)
49 print(" " as *u8); print(name)
50 print(" -> linear=" as *u8); print_i64(lin); print(" indexed=" as *u8); print_i64(idx)
51 print(" expected=" as *u8); print_i64(expected); println("" as *u8)
52 if lin == expected {
53 if idx == expected {
54 println(" match PASS" as *u8); return 0
55 }
56 println(" indexed disagrees with linear FAIL" as *u8); return 1
57 }
58 println(" linear disagrees with expected FAIL" as *u8); return 1
59}
60
61func main() -> nx_exit {
62 println("=== Discrim-tree-backed forward subsumption smoke ===" as *u8)
63 var fails: nx_int = 0
64
65 // Build a processed set: {p(X)}, {q(a)}.
66 let s: *Saturation = nx_saturation_new(50)
67 push(s, mk_unit(mk_p_var(SYM_P, VAR_X))) // proc[0] = {p(X)}
68 push(s, mk_unit(mk_p(SYM_Q, SYM_A))) // proc[1] = {q(a)}
69
70 // ---------- Test 1: query subsumed by p(X) -------------------
71 // Query {p(a)}: proc[0]={p(X)} subsumes it. Expected 1.
72 let q1: *Clause = mk_unit(mk_p(SYM_P, SYM_A))
73 fails = fails + compare("1. {p(a)}" as *u8, s, q1, 1)
74
75 // ---------- Test 2: query subsumed by q(a) (exact) -----------
76 // Query {q(a)}: proc[1]={q(a)} subsumes it. Expected 1.
77 let q2: *Clause = mk_unit(mk_p(SYM_Q, SYM_A))
78 fails = fails + compare("2. {q(a)}" as *u8, s, q2, 1)
79
80 // ---------- Test 3: query NOT subsumed (different head) -----
81 // Query {q(b)}: q(a) doesn't subsume q(b) (a != b). No proc has
82 // a generalization of q(b). Expected 0.
83 let q3: *Clause = mk_unit(mk_p(SYM_Q, SYM_B))
84 fails = fails + compare("3. {q(b)}" as *u8, s, q3, 0)
85
86 // ---------- Test 4: query with p(b) -- still subsumed by p(X) -
87 let q4: *Clause = mk_unit(mk_p(SYM_P, SYM_B))
88 fails = fails + compare("4. {p(b)}" as *u8, s, q4, 1)
89
90 // ---------- Test 5: empty processed set ---------------------
91 let s_empty: *Saturation = nx_saturation_new(10)
92 let lin5: nx_int = nx_sat_proc_subsumes(s_empty, q1)
93 let idx5: nx_int = nx_sat_proc_subsumes_indexed(s_empty, q1)
94 print(" 5. empty processed -> linear=" as *u8); print_i64(lin5); print(" indexed=" as *u8); print_i64(idx5); println("" as *u8)
95 if lin5 == 0 {
96 if idx5 == 0 { println(" both 0 PASS" as *u8) }
97 else { println(" indexed wrong FAIL" as *u8); fails = fails + 1 }
98 } else { println(" linear wrong FAIL" as *u8); fails = fails + 1 }
99
100 println("" as *u8)
101 if fails == 0 {
102 println("=== ALL 5 indexed-subsumption tests PASS ===" as *u8)
103 return 0
104 }
105 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
106 return 1
107}