nx_pure_lit_test.nx source
↩ module page · 122 lines · 5603 B
1// nx_pure_lit_test.nx -- pure-literal elimination 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_pure_lit.nx"
10
11const SYM_A: nx_int = 100
12const SYM_P: nx_int = 200
13const SYM_Q: nx_int = 201
14const SYM_R: nx_int = 202
15
16func mk_p(p_sym: nx_int, c_sym: nx_int) -> *Term {
17 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
18 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
19 return nx_term_app(p_sym, 1, arg)
20}
21
22func mk_unit(sign: nx_int, atom: *Term) -> *Clause {
23 let c: *Clause = nx_clause_new()
24 let _r: *NxResult = nx_clause_add(c, nx_lit_make(sign, atom))
25 return c
26}
27
28func place(arr: *Clause, i: nx_int, src: *Clause) {
29 let dest: *Clause = ((arr as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
30 dest.n_lits = src.n_lits
31 dest.lits = src.lits
32}
33
34func main() -> nx_exit {
35 println("=== Pure-literal elimination smoke ===" as *u8)
36 var fails: nx_int = 0
37
38 // ---------- Test 1: pure positive p, drop {p(a)} ------------
39 // Input: {p(a)}, {q(a), ~q(a)} -- p only positive, q both.
40 // q tautology stays (we don't drop tautologies here -- that's
41 // nx_tautology's job). p is pure positive -> drop {p(a)}.
42 let in1: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
43 place(in1, 0, mk_unit(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
44
45 let qq: *Clause = nx_clause_new()
46 let _ra: *NxResult = nx_clause_add(qq, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
47 let _rb: *NxResult = nx_clause_add(qq, nx_lit_make(NX_LIT_NEG, mk_p(SYM_Q, SYM_A)))
48 place(in1, 1, qq)
49
50 let out1: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
51 let n1_p: *nx_int = sys_mmap(8) as *nx_int
52 let n1: nx_int = nx_pure_lit_eliminate(in1, 2, out1, n1_p)
53 print(" 1. {p(a)}, {q,~q} -> kept=" as *u8); print_i64(n1); println("" as *u8)
54 if n1 == 1 { println(" pure-positive p dropped PASS" as *u8) }
55 else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
56
57 // ---------- Test 2: pure negative r, drop {~r(a)} -----------
58 // Input: {~r(a)}, {p(a), ~p(a)} -- r only negative.
59 let in2: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
60 place(in2, 0, mk_unit(NX_LIT_NEG, mk_p(SYM_R, SYM_A)))
61
62 let pp: *Clause = nx_clause_new()
63 let _r2a: *NxResult = nx_clause_add(pp, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
64 let _r2b: *NxResult = nx_clause_add(pp, nx_lit_make(NX_LIT_NEG, mk_p(SYM_P, SYM_A)))
65 place(in2, 1, pp)
66
67 let out2: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
68 let n2_p: *nx_int = sys_mmap(8) as *nx_int
69 let n2: nx_int = nx_pure_lit_eliminate(in2, 2, out2, n2_p)
70 print(" 2. {~r(a)}, {p,~p} -> kept=" as *u8); print_i64(n2); println("" as *u8)
71 if n2 == 1 { println(" pure-negative r dropped PASS" as *u8) }
72 else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
73
74 // ---------- Test 3: nothing pure, all kept ------------------
75 // Input: {p(a)}, {~p(a)}, {q(a)}, {~q(a)} -- p and q both polarities.
76 let in3: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
77 place(in3, 0, mk_unit(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
78 place(in3, 1, mk_unit(NX_LIT_NEG, mk_p(SYM_P, SYM_A)))
79 place(in3, 2, mk_unit(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
80 place(in3, 3, mk_unit(NX_LIT_NEG, mk_p(SYM_Q, SYM_A)))
81
82 let out3: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
83 let n3_p: *nx_int = sys_mmap(8) as *nx_int
84 let n3: nx_int = nx_pure_lit_eliminate(in3, 4, out3, n3_p)
85 print(" 3. all bipolar -> kept=" as *u8); print_i64(n3); println("" as *u8)
86 if n3 == 4 { println(" all preserved PASS" as *u8) }
87 else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
88
89 // ---------- Test 4: pure literal in multi-lit clause ---------
90 // Input: {p(a), q(a)}, {~q(a)} -- p only positive (in first
91 // clause), q both polarities. First clause has pure-pos p ->
92 // dropped. Result: {~q(a)}.
93 let in4: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
94 let pq: *Clause = nx_clause_new()
95 let _r4a: *NxResult = nx_clause_add(pq, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
96 let _r4b: *NxResult = nx_clause_add(pq, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
97 place(in4, 0, pq)
98 place(in4, 1, mk_unit(NX_LIT_NEG, mk_p(SYM_Q, SYM_A)))
99
100 let out4: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
101 let n4_p: *nx_int = sys_mmap(8) as *nx_int
102 let n4: nx_int = nx_pure_lit_eliminate(in4, 2, out4, n4_p)
103 print(" 4. {p,q}, {~q}, p pure-pos -> kept=" as *u8); print_i64(n4); println("" as *u8)
104 if n4 == 1 { println(" {p,q} dropped via pure p PASS" as *u8) }
105 else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
106
107 // ---------- Test 5: empty input -----------------------------
108 let out5: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
109 let n5_p: *nx_int = sys_mmap(8) as *nx_int
110 let n5: nx_int = nx_pure_lit_eliminate(in1, 0, out5, n5_p)
111 print(" 5. empty input -> kept=" as *u8); print_i64(n5); println("" as *u8)
112 if n5 == 0 { println(" handles empty PASS" as *u8) }
113 else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
114
115 println("" as *u8)
116 if fails == 0 {
117 println("=== ALL 5 pure-lit tests PASS ===" as *u8)
118 return 0
119 }
120 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
121 return 1
122}