nx_pre_sat_test.nx source
↩ module page · 130 lines · 5350 B
1// nx_pre_sat_test.nx -- pre-saturation simplification 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_subsumption.nx"
10import "nx_tautology.nx"
11import "nx_pre_sat.nx"
12
13const SYM_A: nx_int = 100
14const SYM_P: nx_int = 200
15const SYM_Q: nx_int = 201
16const SYM_EQ: nx_int = 50
17const VAR_X: nx_int = 0
18
19func mk_p(p_sym: nx_int, c_sym: nx_int) -> *Term {
20 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
21 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
22 return nx_term_app(p_sym, 1, arg)
23}
24
25func mk_p_var(p_sym: nx_int, var_id: nx_int) -> *Term {
26 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
27 arg.kind = NX_TERM_VAR; arg.sym = var_id; arg.n_args = 0; arg.args = 0 as *Term
28 return nx_term_app(p_sym, 1, arg)
29}
30
31func mk_unit_pos(atom: *Term) -> *Clause {
32 let c: *Clause = nx_clause_new()
33 let _r: *NxResult = nx_clause_add(c, nx_lit_make(NX_LIT_POS, atom))
34 return c
35}
36
37func place(arr: *Clause, i: nx_int, src: *Clause) {
38 let dest: *Clause = ((arr as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
39 dest.n_lits = src.n_lits
40 dest.lits = src.lits
41}
42
43func main() -> nx_exit {
44 println("=== Pre-saturation simplification smoke ===" as *u8)
45 var fails: nx_int = 0
46
47 // ---------- Test 1: drop tautology --------------------------
48 // Input: {p(a)}, {p(a) | ~p(a)}, {q(a)}
49 // Expected: 2 kept (tautology removed)
50 let in1: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
51 place(in1, 0, mk_unit_pos(mk_p(SYM_P, SYM_A)))
52
53 let taut: *Clause = nx_clause_new()
54 let _ra: *NxResult = nx_clause_add(taut, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
55 let _rb: *NxResult = nx_clause_add(taut, nx_lit_make(NX_LIT_NEG, mk_p(SYM_P, SYM_A)))
56 place(in1, 1, taut)
57
58 place(in1, 2, mk_unit_pos(mk_p(SYM_Q, SYM_A)))
59
60 let out1: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
61 let n1: nx_int = nx_pre_sat_simplify(in1, 3, SYM_EQ, out1)
62 print(" 1. tautology drop -> kept=" as *u8); print_i64(n1); println("" as *u8)
63 if n1 == 2 {
64 println(" dropped tautology PASS" as *u8)
65 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
66
67 // ---------- Test 2: forward subsumption ---------------------
68 // Input: {p(X)}, {p(a), q(a)}, {q(a)}
69 // {p(a), q(a)} is subsumed by {p(X)}. -> kept = {p(X), q(a)}.
70 let in2: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
71 place(in2, 0, mk_unit_pos(mk_p_var(SYM_P, VAR_X)))
72
73 let pq: *Clause = nx_clause_new()
74 let _r2a: *NxResult = nx_clause_add(pq, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
75 let _r2b: *NxResult = nx_clause_add(pq, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
76 place(in2, 1, pq)
77
78 place(in2, 2, mk_unit_pos(mk_p(SYM_Q, SYM_A)))
79
80 let out2: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
81 let n2: nx_int = nx_pre_sat_simplify(in2, 3, SYM_EQ, out2)
82 print(" 2. forward-subsumption -> kept=" as *u8); print_i64(n2); println("" as *u8)
83 if n2 == 2 {
84 println(" {p(a),q(a)} subsumed, dropped PASS" as *u8)
85 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
86
87 // ---------- Test 3: backward subsumption --------------------
88 // Input: {p(a), q(a)}, {p(X)}
89 // First {p(a), q(a)} kept (no prior). Then {p(X)} arrives -- it
90 // subsumes the previously-kept clause; backward simplification
91 // drops {p(a), q(a)}. -> kept = {p(X)}.
92 let in3: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
93
94 let pq2: *Clause = nx_clause_new()
95 let _r3a: *NxResult = nx_clause_add(pq2, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
96 let _r3b: *NxResult = nx_clause_add(pq2, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
97 place(in3, 0, pq2)
98
99 place(in3, 1, mk_unit_pos(mk_p_var(SYM_P, VAR_X)))
100
101 let out3: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
102 let n3: nx_int = nx_pre_sat_simplify(in3, 2, SYM_EQ, out3)
103 print(" 3. backward-simp -> kept=" as *u8); print_i64(n3); println("" as *u8)
104 if n3 == 1 {
105 println(" general clause supplanted specific PASS" as *u8)
106 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
107
108 // ---------- Test 4: nothing to drop -------------------------
109 // Input: {p(a)}, {q(a)}, {r(a)} -- all distinct, no overlap.
110 let SYM_R: nx_int = 202
111 let in4: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
112 place(in4, 0, mk_unit_pos(mk_p(SYM_P, SYM_A)))
113 place(in4, 1, mk_unit_pos(mk_p(SYM_Q, SYM_A)))
114 place(in4, 2, mk_unit_pos(mk_p(SYM_R, SYM_A)))
115
116 let out4: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
117 let n4: nx_int = nx_pre_sat_simplify(in4, 3, SYM_EQ, out4)
118 print(" 4. no-op pass -> kept=" as *u8); print_i64(n4); println("" as *u8)
119 if n4 == 3 {
120 println(" all preserved PASS" as *u8)
121 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
122
123 println("" as *u8)
124 if fails == 0 {
125 println("=== ALL 4 pre-saturation tests PASS ===" as *u8)
126 return 0
127 }
128 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
129 return 1
130}