nx_avatar_split_test.nx source
↩ module page · 133 lines · 6357 B
1// nx_avatar_split_test.nx -- AVATAR splitting 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_clause_components.nx"
10import "nx_avatar_split.nx"
11
12const SYM_A: nx_int = 100
13const SYM_B: nx_int = 101
14const SYM_P: nx_int = 200
15const SYM_Q: nx_int = 201
16const SYM_R: nx_int = 202
17const VAR_X: nx_int = 0
18const VAR_Y: nx_int = 1
19
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
26func mk_p_var(p_sym: nx_int, var_id: nx_int) -> *Term {
27 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
28 arg.kind = NX_TERM_VAR; arg.sym = var_id; arg.n_args = 0; arg.args = 0 as *Term
29 return nx_term_app(p_sym, 1, arg)
30}
31
32func place(arr: *Clause, i: nx_int, src: *Clause) {
33 let dest: *Clause = ((arr as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
34 dest.n_lits = src.n_lits
35 dest.lits = src.lits
36}
37
38func main() -> nx_exit {
39 println("=== AVATAR splitting smoke ===" as *u8)
40 var fails: nx_int = 0
41
42 let out: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
43
44 // ---------- Test 1: single-component passes through --------
45 // {p(X), q(X)} -- shared X, single component. Output: 1 clause.
46 let c1: *Clause = nx_clause_new()
47 let _r1a: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
48 let _r1b: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_Q, VAR_X)))
49 let n1: nx_int = nx_avatar_split_clause(c1, out, 10)
50 print(" 1. {p(X),q(X)} (1 comp) -> emitted=" as *u8); print_i64(n1); println("" as *u8)
51 if n1 == 1 {
52 let dest: *Clause = out
53 if dest.n_lits == 2 { println(" pass-through with 2 lits PASS" as *u8) }
54 else { println(" wrong n_lits FAIL" as *u8); fails = fails + 1 }
55 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
56
57 // ---------- Test 2: 2-component split ---------------------
58 // {p(X), q(Y)} -- X and Y disjoint, 2 components.
59 // Expected: 2 clauses {p(X)} and {q(Y)}.
60 let c2: *Clause = nx_clause_new()
61 let _r2a: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
62 let _r2b: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_Q, VAR_Y)))
63 let n2: nx_int = nx_avatar_split_clause(c2, out, 10)
64 print(" 2. {p(X), q(Y)} (2 comp) -> emitted=" as *u8); print_i64(n2); println("" as *u8)
65 if n2 == 2 {
66 let d0: *Clause = out
67 let d1: *Clause = ((out as nx_int) + NX_CLAUSE_BYTES) as *Clause
68 if d0.n_lits == 1 {
69 if d1.n_lits == 1 {
70 println(" 2 single-lit subclauses PASS" as *u8)
71 } else { println(" d1 wrong FAIL" as *u8); fails = fails + 1 }
72 } else { println(" d0 wrong FAIL" as *u8); fails = fails + 1 }
73 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
74
75 // ---------- Test 3: ground multi-comp split ----------------
76 // {p(a), q(b)} -- ground, no var sharing -> 2 components.
77 let c3: *Clause = nx_clause_new()
78 let _r3a: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
79 let _r3b: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_B)))
80 let n3: nx_int = nx_avatar_split_clause(c3, out, 10)
81 print(" 3. {p(a), q(b)} ground -> emitted=" as *u8); print_i64(n3); println("" as *u8)
82 if n3 == 2 { println(" ground split PASS" as *u8) }
83 else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
84
85 // ---------- Test 4: split_all over a clause set ------------
86 // Inputs: {p(X), q(X)} (1 comp), {p(a), q(b)} (2 comp).
87 // Expected: 1 + 2 = 3 output clauses.
88 let in4: *Clause = (sys_mmap((10 * NX_CLAUSE_BYTES) as i64)) as *Clause
89 place(in4, 0, c1)
90 place(in4, 1, c3)
91 let n4: nx_int = nx_avatar_split_all(in4, 2, out, 10)
92 print(" 4. split_all of 2 input clauses -> total=" as *u8); print_i64(n4); println("" as *u8)
93 if n4 == 3 { println(" 1 + 2 = 3 outputs PASS" as *u8) }
94 else { println(" wrong total FAIL" as *u8); fails = fails + 1 }
95
96 // ---------- Test 5: multi-comp with shared chain -----------
97 // {p(X), q(X), r(Y)} -- X-pair + Y-singleton -> 2 components.
98 // Expected first comp: {p(X), q(X)}, second: {r(Y)}.
99 let c5: *Clause = nx_clause_new()
100 let _r5a: *NxResult = nx_clause_add(c5, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
101 let _r5b: *NxResult = nx_clause_add(c5, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_Q, VAR_X)))
102 let _r5c: *NxResult = nx_clause_add(c5, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_R, VAR_Y)))
103 let n5: nx_int = nx_avatar_split_clause(c5, out, 10)
104 print(" 5. {p(X),q(X),r(Y)} -> emitted=" as *u8); print_i64(n5); println("" as *u8)
105 if n5 == 2 {
106 let d0: *Clause = out
107 let d1: *Clause = ((out as nx_int) + NX_CLAUSE_BYTES) as *Clause
108 // First component (X-pair) should have 2 lits, second (Y-only) 1 lit.
109 if d0.n_lits == 2 {
110 if d1.n_lits == 1 {
111 println(" {p,q} + {r} PASS" as *u8)
112 } else { print(" d1 lits=" as *u8); print_i64(d1.n_lits); println(" FAIL" as *u8); fails = fails + 1 }
113 } else { print(" d0 lits=" as *u8); print_i64(d0.n_lits); println(" FAIL" as *u8); fails = fails + 1 }
114 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
115
116 // ---------- Test 6: empty clause passes through ------------
117 let empty: *Clause = nx_clause_new()
118 let n6: nx_int = nx_avatar_split_clause(empty, out, 10)
119 print(" 6. empty clause -> emitted=" as *u8); print_i64(n6); println("" as *u8)
120 if n6 == 1 {
121 let d: *Clause = out
122 if d.n_lits == 0 { println(" empty preserved PASS" as *u8) }
123 else { println(" not empty FAIL" as *u8); fails = fails + 1 }
124 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
125
126 println("" as *u8)
127 if fails == 0 {
128 println("=== ALL 6 AVATAR-split tests PASS ===" as *u8)
129 return 0
130 }
131 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
132 return 1
133}