nx_clause_components_test.nx source
↩ module page · 117 lines · 5934 B
1// nx_clause_components_test.nx -- AVATAR-style component analysis 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"
10
11const SYM_A: nx_int = 100
12const SYM_B: nx_int = 101
13const SYM_P: nx_int = 200
14const SYM_Q: nx_int = 201
15const SYM_R: nx_int = 202
16const VAR_X: nx_int = 0
17const VAR_Y: nx_int = 1
18const VAR_Z: nx_int = 2
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 main() -> nx_exit {
33 println("=== Clause component analysis smoke ===" as *u8)
34 var fails: nx_int = 0
35
36 // ---------- Test 1: single literal => 1 component ----------
37 let c1: *Clause = nx_clause_new()
38 let _r1: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
39 let n1: nx_int = nx_clause_n_components(c1)
40 print(" 1. {p(a)} -> n_comp=" as *u8); print_i64(n1); println("" as *u8)
41 if n1 == 1 { println(" PASS" as *u8) }
42 else { println(" FAIL" as *u8); fails = fails + 1 }
43
44 // ---------- Test 2: ground clause, 2 lits, no shared vars --
45 // {p(a), q(b)} -- two ground literals, no variables -> still 2
46 // independent components (no var sharing).
47 let c2: *Clause = nx_clause_new()
48 let _r2a: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
49 let _r2b: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_B)))
50 let n2: nx_int = nx_clause_n_components(c2)
51 print(" 2. {p(a), q(b)} -> n_comp=" as *u8); print_i64(n2); println("" as *u8)
52 if n2 == 2 { println(" 2 independent ground literals PASS" as *u8) }
53 else { println(" FAIL" as *u8); fails = fails + 1 }
54
55 // ---------- Test 3: shared variable -> single component ----
56 // {p(X), q(X)} -- both share X
57 let c3: *Clause = nx_clause_new()
58 let _r3a: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
59 let _r3b: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_Q, VAR_X)))
60 let n3: nx_int = nx_clause_n_components(c3)
61 print(" 3. {p(X), q(X)} -> n_comp=" as *u8); print_i64(n3); println("" as *u8)
62 if n3 == 1 { println(" shared X merges PASS" as *u8) }
63 else { println(" FAIL" as *u8); fails = fails + 1 }
64
65 // ---------- Test 4: chain via shared vars ------------------
66 // {p(X), q(X, Y), r(Y)} -- p+q share X, q+r share Y, all merge
67 // (We need a binary q for this -- skip and use a different shape.)
68 // Let's use {p(X), q(X), q(Y), r(Y)} -- two pairs share X, two
69 // share Y, but the X-pair and Y-pair are disjoint -> 2 components.
70 let c4: *Clause = nx_clause_new()
71 let _r4a: *NxResult = nx_clause_add(c4, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
72 let _r4b: *NxResult = nx_clause_add(c4, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_Q, VAR_X)))
73 let _r4c: *NxResult = nx_clause_add(c4, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_Q, VAR_Y)))
74 let _r4d: *NxResult = nx_clause_add(c4, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_R, VAR_Y)))
75 let n4: nx_int = nx_clause_n_components(c4)
76 print(" 4. {p(X),q(X),q(Y),r(Y)} -> n_comp=" as *u8); print_i64(n4); println("" as *u8)
77 if n4 == 2 { println(" two var-disjoint pairs PASS" as *u8) }
78 else { println(" FAIL" as *u8); fails = fails + 1 }
79
80 // ---------- Test 5: ground + var literal independent -------
81 // {p(a), q(X)} -- p(a) has no vars, q(X) has X. Vars-share=false
82 // for the pair -> 2 components.
83 let c5: *Clause = nx_clause_new()
84 let _r5a: *NxResult = nx_clause_add(c5, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
85 let _r5b: *NxResult = nx_clause_add(c5, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_Q, VAR_X)))
86 let n5: nx_int = nx_clause_n_components(c5)
87 print(" 5. {p(a), q(X)} -> n_comp=" as *u8); print_i64(n5); println("" as *u8)
88 if n5 == 2 { println(" ground + var literal independent PASS" as *u8) }
89 else { println(" FAIL" as *u8); fails = fails + 1 }
90
91 // ---------- Test 6: out_ids classification -----------------
92 // {p(X), q(X), r(Y)} -- comps {0,1} share root, {2} alone.
93 // out_ids should reflect: ids[0] == ids[1] != ids[2]
94 let c6: *Clause = nx_clause_new()
95 let _r6a: *NxResult = nx_clause_add(c6, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
96 let _r6b: *NxResult = nx_clause_add(c6, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_Q, VAR_X)))
97 let _r6c: *NxResult = nx_clause_add(c6, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_R, VAR_Y)))
98 let ids: *nx_int = (sys_mmap((c6.n_lits * 8) as i64)) as *nx_int
99 let n6: nx_int = nx_clause_components_classify(c6, ids)
100 print(" 6. classify {p(X),q(X),r(Y)} -> n=" as *u8); print_i64(n6)
101 print(" ids=[" as *u8); print_i64(ids[0]); print("," as *u8); print_i64(ids[1]); print("," as *u8); print_i64(ids[2]); println("]" as *u8)
102 if n6 == 2 {
103 if ids[0] == ids[1] {
104 if ids[0] != ids[2] {
105 println(" ids[0]==ids[1] != ids[2] PASS" as *u8)
106 } else { println(" wrong partition FAIL" as *u8); fails = fails + 1 }
107 } else { println(" wrong partition FAIL" as *u8); fails = fails + 1 }
108 } else { println(" wrong count FAIL" as *u8); fails = fails + 1 }
109
110 println("" as *u8)
111 if fails == 0 {
112 println("=== ALL 6 component-analysis tests PASS ===" as *u8)
113 return 0
114 }
115 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
116 return 1
117}