nx_backward_subsume_test.nx source
↩ module page · 150 lines · 6273 B
1// nx_backward_subsume_test.nx -- backward subsumption smoke.
2//
3// Setup: load specific-then-general clauses into the queue. After the
4// general clause arrives in `processed`, the older specific clause it
5// subsumes should be removed by backward subsumption -- so the final
6// n_processed reflects only the survivors.
7
8import "nx_syscalls.nx"
9import "nx_runtime.nx"
10import "nx_tier.nx"
11import "nx_result.nx"
12import "nx_unify.nx"
13import "nx_resolution.nx"
14import "nx_subsumption.nx"
15import "nx_tautology.nx"
16import "nx_saturation.nx"
17
18const SYM_A: nx_int = 100
19const SYM_P: nx_int = 200
20const SYM_Q: nx_int = 201
21const SYM_EQ: nx_int = 50
22
23const VAR_X: nx_int = 0
24
25func mk_p(p_sym: nx_int, c_sym: nx_int) -> *Term {
26 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
27 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
28 return nx_term_app(p_sym, 1, arg)
29}
30
31func mk_p_var(p_sym: nx_int, var_id: nx_int) -> *Term {
32 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
33 arg.kind = NX_TERM_VAR; arg.sym = var_id; arg.n_args = 0; arg.args = 0 as *Term
34 return nx_term_app(p_sym, 1, arg)
35}
36
37func main() -> nx_exit {
38 println("=== Backward subsumption smoke ===" as *u8)
39 var fails: nx_int = 0
40
41 // ---------- Test 1: general arrives after specific -----------
42 // Queue order:
43 // c1 = {p(a), q(a)} -- specific (lands in processed first)
44 // c2 = {p(X)} -- general (subsumes c1)
45 // Expected after run:
46 // - c1 enters processed
47 // - c2 enters processed -- its arrival triggers backward
48 // subsumption, which drops c1 (since c2 subsumes c1).
49 // - n_processed = 1 (only c2 survives)
50 let c1: *Clause = nx_clause_new()
51 let _r1a: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
52 let _r1b: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
53
54 let c2: *Clause = nx_clause_new()
55 let _r2: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
56
57 let s: *Saturation = nx_saturation_new(50)
58 let _u1: *NxResult = nx_sat_add_unproc(s, c1)
59 let _u2: *NxResult = nx_sat_add_unproc(s, c2)
60 let _v: nx_int = nx_sat_run_discount(s, SYM_EQ)
61 // n_processed semantics: under tombstone path, slots aren't
62 // physically removed -- just marked deleted=1. Count the LIVE
63 // (non-tombstoned) entries.
64 var live1: nx_int = 0
65 var i1: nx_int = 0
66 while i1 < s.n_processed {
67 if s.proc_deleted[i1] == 0 { live1 = live1 + 1 }
68 i1 = i1 + 1
69 }
70 print(" 1. specific then general -> n_processed=" as *u8); print_i64(s.n_processed); print(" live=" as *u8); print_i64(live1); println("" as *u8)
71 if live1 == 1 {
72 println(" general clause survives, specific tombstoned PASS" as *u8)
73 } else {
74 println(" unexpected live count -- backward subsume not firing FAIL" as *u8)
75 fails = fails + 1
76 }
77
78 // ---------- Test 2: direct backward_subsume call --------------
79 // Build processed = [{p(a)}, {p(a),q(a)}, {q(a)}] manually, then
80 // call backward_subsume({p(X)}) -- should remove the first two,
81 // keep the third.
82 let s2: *Saturation = nx_saturation_new(10)
83 let pa: *Clause = nx_clause_new()
84 let _ra: *NxResult = nx_clause_add(pa, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
85 let paqa: *Clause = nx_clause_new()
86 let _rb: *NxResult = nx_clause_add(paqa, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
87 let _rc: *NxResult = nx_clause_add(paqa, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
88 let qa: *Clause = nx_clause_new()
89 let _rd: *NxResult = nx_clause_add(qa, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
90
91 let _m1: *NxResult = nx_sat_move_to_processed(s2, pa)
92 let _m2: *NxResult = nx_sat_move_to_processed(s2, paqa)
93 let _m3: *NxResult = nx_sat_move_to_processed(s2, qa)
94
95 let general: *Clause = nx_clause_new()
96 let _re: *NxResult = nx_clause_add(general, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
97
98 let removed: nx_int = nx_sat_backward_subsume(s2, general)
99 var live2: nx_int = 0
100 var i2: nx_int = 0
101 while i2 < s2.n_processed {
102 if s2.proc_deleted[i2] == 0 { live2 = live2 + 1 }
103 i2 = i2 + 1
104 }
105 print(" 2. direct backward_subsume({p(X)}) -> removed=" as *u8); print_i64(removed); print(" live=" as *u8); print_i64(live2); println("" as *u8)
106 if removed == 2 {
107 if live2 == 1 {
108 println(" tombstoned {p(a)} and {p(a),q(a)}, kept {q(a)} PASS" as *u8)
109 } else {
110 println(" live count off FAIL" as *u8); fails = fails + 1
111 }
112 } else {
113 println(" wrong removal count FAIL" as *u8); fails = fails + 1
114 }
115
116 // ---------- Test 3: no backward subsumption when nothing applies
117 // Build processed = [{p(a)}, {q(a)}], call backward_subsume({r(a)})
118 // Should remove 0.
119 let s3: *Saturation = nx_saturation_new(10)
120 let pa3: *Clause = nx_clause_new()
121 let _r3a: *NxResult = nx_clause_add(pa3, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
122 let qa3: *Clause = nx_clause_new()
123 let _r3b: *NxResult = nx_clause_add(qa3, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
124 let _m3a: *NxResult = nx_sat_move_to_processed(s3, pa3)
125 let _m3b: *NxResult = nx_sat_move_to_processed(s3, qa3)
126
127 let SYM_R: nx_int = 202
128 let unrelated: *Clause = nx_clause_new()
129 let _r3c: *NxResult = nx_clause_add(unrelated, nx_lit_make(NX_LIT_POS, mk_p(SYM_R, SYM_A)))
130
131 let removed3: nx_int = nx_sat_backward_subsume(s3, unrelated)
132 print(" 3. backward_subsume({r(a)}) on processed={p(a),q(a)} -> removed=" as *u8); print_i64(removed3); println("" as *u8)
133 if removed3 == 0 {
134 if s3.n_processed == 2 {
135 println(" nothing dropped, both kept PASS" as *u8)
136 } else {
137 println(" n_processed off FAIL" as *u8); fails = fails + 1
138 }
139 } else {
140 println(" spurious removal FAIL" as *u8); fails = fails + 1
141 }
142
143 println("" as *u8)
144 if fails == 0 {
145 println("=== ALL 3 backward-subsumption tests PASS ===" as *u8)
146 return 0
147 }
148 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
149 return 1
150}