nx_hyperres_test.nx source
↩ module page · 161 lines · 7102 B
1// nx_hyperres_test.nx -- N-electron hyperresolution 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_hyperres.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
17
18func mk_p(p_sym: nx_int, c_sym: nx_int) -> *Term {
19 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
20 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
21 return nx_term_app(p_sym, 1, arg)
22}
23
24func mk_p_var(p_sym: nx_int, var_id: nx_int) -> *Term {
25 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
26 arg.kind = NX_TERM_VAR; arg.sym = var_id; arg.n_args = 0; arg.args = 0 as *Term
27 return nx_term_app(p_sym, 1, arg)
28}
29
30func place(arr: *Clause, i: nx_int, src: *Clause) {
31 let dest: *Clause = ((arr as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
32 dest.n_lits = src.n_lits
33 dest.lits = src.lits
34}
35
36func main() -> nx_exit {
37 println("=== N-electron hyperresolution smoke ===" as *u8)
38 var fails: nx_int = 0
39
40 // ---------- Test 1: 2-electron classic case ----------------
41 // Nucleus: {p(a), ~q(a), ~r(a)}
42 // Electrons: E1 = {q(a)}, E2 = {r(a)}
43 // Resolve nucleus[1] with E1[0], nucleus[2] with E2[0]
44 // Expected: {p(a)} (residual nucleus, electrons fully consumed)
45 let nuc: *Clause = nx_clause_new()
46 let _r1a: *NxResult = nx_clause_add(nuc, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
47 let _r1b: *NxResult = nx_clause_add(nuc, nx_lit_make(NX_LIT_NEG, mk_p(SYM_Q, SYM_A)))
48 let _r1c: *NxResult = nx_clause_add(nuc, nx_lit_make(NX_LIT_NEG, mk_p(SYM_R, SYM_A)))
49
50 let elecs: *Clause = (sys_mmap((4 * NX_CLAUSE_BYTES) as i64)) as *Clause
51 let e1: *Clause = nx_clause_new()
52 let _re1: *NxResult = nx_clause_add(e1, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
53 place(elecs, 0, e1)
54 let e2: *Clause = nx_clause_new()
55 let _re2: *NxResult = nx_clause_add(e2, nx_lit_make(NX_LIT_POS, mk_p(SYM_R, SYM_A)))
56 place(elecs, 1, e2)
57
58 let neg_idx: *nx_int = (sys_mmap(16)) as *nx_int
59 neg_idx[0] = 1
60 neg_idx[1] = 2
61 let pos_idx: *nx_int = (sys_mmap(16)) as *nx_int
62 pos_idx[0] = 0
63 pos_idx[1] = 0
64
65 let out1: *Clause = nx_clause_new()
66 let r1: *NxResult = nx_hyperresolve(nuc, neg_idx, 2, elecs, pos_idx, 2, out1)
67 if nx_result_is_err(r1) == 1 {
68 println("1. {p,~q,~r} + {q} + {r} -> ERR FAIL" as *u8); fails = fails + 1
69 } else {
70 if out1.n_lits == 1 {
71 let l: *Literal = nx_clause_lit_at(out1, 0)
72 if l.atom.sym == SYM_P {
73 println("1. 2-electron hyperres -> {p(a)} PASS" as *u8)
74 } else { print("1. wrong head sym=" as *u8); print_i64(l.atom.sym); println(" FAIL" as *u8); fails = fails + 1 }
75 } else { print("1. n_lits=" as *u8); print_i64(out1.n_lits); println(" FAIL" as *u8); fails = fails + 1 }
76 }
77
78 // ---------- Test 2: composed unifier across electrons ------
79 // Nucleus: {p(X), ~q(X), ~r(X)} -- all share X
80 // E1 = {q(a)}, E2 = {r(a)} -- both fix X to a
81 // Unifier composes: X := a from E1, then E2 already has X := a.
82 // Expected: {p(a)}.
83 let nuc2: *Clause = nx_clause_new()
84 let _r2a: *NxResult = nx_clause_add(nuc2, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
85 let _r2b: *NxResult = nx_clause_add(nuc2, nx_lit_make(NX_LIT_NEG, mk_p_var(SYM_Q, VAR_X)))
86 let _r2c: *NxResult = nx_clause_add(nuc2, nx_lit_make(NX_LIT_NEG, mk_p_var(SYM_R, VAR_X)))
87
88 let out2: *Clause = nx_clause_new()
89 let r2: *NxResult = nx_hyperresolve(nuc2, neg_idx, 2, elecs, pos_idx, 2, out2)
90 if nx_result_is_err(r2) == 1 {
91 println("2. {p(X),~q(X),~r(X)} + {q(a)} + {r(a)} -> ERR FAIL" as *u8); fails = fails + 1
92 } else {
93 if out2.n_lits == 1 {
94 let l: *Literal = nx_clause_lit_at(out2, 0)
95 let arg: *Term = nx_term_arg(l.atom, 0)
96 if arg.kind == NX_TERM_CONST {
97 if arg.sym == SYM_A {
98 println("2. composed unifier X:=a -> {p(a)} PASS" as *u8)
99 } else { println("2. arg not a FAIL" as *u8); fails = fails + 1 }
100 } else { println("2. arg not CONST -- subst not applied FAIL" as *u8); fails = fails + 1 }
101 } else { println("2. wrong count FAIL" as *u8); fails = fails + 1 }
102 }
103
104 // ---------- Test 3: incompatible unifier rejects -----------
105 // Nucleus: {~p(X), ~q(X)}
106 // E1 = {p(a)}, E2 = {q(b)}
107 // Composed unifier would bind X to both a and b -> fail.
108 let nuc3: *Clause = nx_clause_new()
109 let _r3a: *NxResult = nx_clause_add(nuc3, nx_lit_make(NX_LIT_NEG, mk_p_var(SYM_P, VAR_X)))
110 let _r3b: *NxResult = nx_clause_add(nuc3, nx_lit_make(NX_LIT_NEG, mk_p_var(SYM_Q, VAR_X)))
111
112 let elecs3: *Clause = (sys_mmap((4 * NX_CLAUSE_BYTES) as i64)) as *Clause
113 let e3a: *Clause = nx_clause_new()
114 let _re3a: *NxResult = nx_clause_add(e3a, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
115 place(elecs3, 0, e3a)
116 let e3b: *Clause = nx_clause_new()
117 let _re3b: *NxResult = nx_clause_add(e3b, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_B)))
118 place(elecs3, 1, e3b)
119
120 let neg3: *nx_int = (sys_mmap(16)) as *nx_int
121 neg3[0] = 0
122 neg3[1] = 1
123 let pos3: *nx_int = (sys_mmap(16)) as *nx_int
124 pos3[0] = 0
125 pos3[1] = 0
126
127 let out3: *Clause = nx_clause_new()
128 let r3: *NxResult = nx_hyperresolve(nuc3, neg3, 2, elecs3, pos3, 2, out3)
129 if nx_result_is_err(r3) == 1 {
130 println("3. {~p(X),~q(X)} + {p(a)} + {q(b)} -> ERR (X binds twice) PASS" as *u8)
131 } else { println("3. expected ERR FAIL" as *u8); fails = fails + 1 }
132
133 // ---------- Test 4: polarity mismatch ----------------------
134 // Nucleus[0] is POS but caller asks to consume it as if NEG.
135 let neg4: *nx_int = (sys_mmap(16)) as *nx_int
136 neg4[0] = 0 // nucleus[0] is the POSITIVE p(a) -- error
137 let pos4: *nx_int = (sys_mmap(16)) as *nx_int
138 pos4[0] = 0
139 let out4: *Clause = nx_clause_new()
140 let r4: *NxResult = nx_hyperresolve(nuc, neg4, 1, elecs, pos4, 1, out4)
141 if nx_result_is_err(r4) == 1 {
142 if nx_result_err_code(r4) == NX_ERR_TAG_MISMATCH {
143 println("4. polarity mismatch -> ERR=TAG_MISMATCH PASS" as *u8)
144 } else { println("4. wrong err code FAIL" as *u8); fails = fails + 1 }
145 } else { println("4. expected ERR FAIL" as *u8); fails = fails + 1 }
146
147 // ---------- Test 5: index count mismatch -------------------
148 // n_neg != n_electrons should reject.
149 let r5: *NxResult = nx_hyperresolve(nuc, neg_idx, 2, elecs, pos_idx, 1, nx_clause_new())
150 if nx_result_is_err(r5) == 1 {
151 println("5. n_neg != n_electrons -> ERR PASS" as *u8)
152 } else { println("5. expected ERR FAIL" as *u8); fails = fails + 1 }
153
154 println("" as *u8)
155 if fails == 0 {
156 println("=== ALL 5 hyperresolution tests PASS ===" as *u8)
157 return 0
158 }
159 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
160 return 1
161}