nx_resolution_test.nx source
↩ module page · 108 lines · 4480 B
1// nx_resolution_test.nx -- binary resolution 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"
9
10const SYM_P: nx_int = 200
11const SYM_Q: nx_int = 201
12const SYM_A: nx_int = 100
13const SYM_B: nx_int = 101
14const VAR_X: nx_int = 1
15
16func main() -> nx_exit {
17 println("=== Binary resolution smoke ===" as *u8)
18
19 // Test 1: Resolve {p(x), q(x)} with {~p(a)} on p
20 // -> resolvent: {q(a)}
21 let p_x_args: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
22 p_x_args.kind = NX_TERM_VAR; p_x_args.sym = VAR_X
23 p_x_args.n_args = 0; p_x_args.args = 0 as *Term
24 let atom_p_x: *Term = nx_term_app(SYM_P, 1, p_x_args)
25
26 let q_x_args: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
27 q_x_args.kind = NX_TERM_VAR; q_x_args.sym = VAR_X
28 q_x_args.n_args = 0; q_x_args.args = 0 as *Term
29 let atom_q_x: *Term = nx_term_app(SYM_Q, 1, q_x_args)
30
31 let c1: *Clause = nx_clause_new()
32 let lit1a: *Literal = nx_lit_make(NX_LIT_POS, atom_p_x)
33 let lit1b: *Literal = nx_lit_make(NX_LIT_POS, atom_q_x)
34 let _r1a: *NxResult = nx_clause_add(c1, lit1a)
35 let _r1b: *NxResult = nx_clause_add(c1, lit1b)
36
37 let p_a_args: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
38 p_a_args.kind = NX_TERM_CONST; p_a_args.sym = SYM_A
39 p_a_args.n_args = 0; p_a_args.args = 0 as *Term
40 let atom_p_a: *Term = nx_term_app(SYM_P, 1, p_a_args)
41
42 let c2: *Clause = nx_clause_new()
43 let lit2a: *Literal = nx_lit_make(NX_LIT_NEG, atom_p_a)
44 let _r2: *NxResult = nx_clause_add(c2, lit2a)
45
46 let c_out: *Clause = nx_clause_new()
47 let r_res: *NxResult = nx_resolve(c1, 0, c2, 0, c_out)
48 if nx_result_is_err(r_res) == 1 {
49 print("FAIL: resolve t1 expected OK got err=" as *u8)
50 print(nx_err_name(nx_result_err_code(r_res))); println("" as *u8)
51 return 1
52 }
53 if c_out.n_lits != 1 { return 2 }
54 let resolvent_lit: *Literal = nx_clause_lit_at(c_out, 0)
55 if resolvent_lit.atom.sym != SYM_Q { return 3 }
56 print(" Test 1 resolve {p(x), q(x)} with {~p(a)} -> {q(" as *u8)
57 if resolvent_lit.atom.n_args > 0 {
58 let arg0: *Term = nx_term_arg(resolvent_lit.atom, 0)
59 if arg0.kind == NX_TERM_CONST {
60 if arg0.sym == SYM_A { print("a" as *u8) }
61 }
62 }
63 println(")} PASS" as *u8)
64
65 // Test 2: Resolve {p(a)} with {~p(b)} -> ERR (atoms don't unify)
66 let p_b_args: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
67 p_b_args.kind = NX_TERM_CONST; p_b_args.sym = SYM_B
68 p_b_args.n_args = 0; p_b_args.args = 0 as *Term
69 let atom_p_b: *Term = nx_term_app(SYM_P, 1, p_b_args)
70
71 let c3: *Clause = nx_clause_new()
72 let _r3: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, atom_p_a))
73
74 let c4: *Clause = nx_clause_new()
75 let _r4: *NxResult = nx_clause_add(c4, nx_lit_make(NX_LIT_NEG, atom_p_b))
76
77 let c_out2: *Clause = nx_clause_new()
78 let r2: *NxResult = nx_resolve(c3, 0, c4, 0, c_out2)
79 if nx_result_is_err(r2) == 0 { return 10 }
80 print(" Test 2 resolve {p(a)} with {~p(b)} -> ERR=" as *u8)
81 print(nx_err_name(nx_result_err_code(r2))); println(" PASS" as *u8)
82
83 // Test 3: Empty-clause contradiction: resolve {p(a)} with {~p(a)} -> {}
84 let c5: *Clause = nx_clause_new()
85 let _r5: *NxResult = nx_clause_add(c5, nx_lit_make(NX_LIT_POS, atom_p_a))
86 let c6: *Clause = nx_clause_new()
87 let _r6: *NxResult = nx_clause_add(c6, nx_lit_make(NX_LIT_NEG, atom_p_a))
88 let c_empty: *Clause = nx_clause_new()
89 let r3: *NxResult = nx_resolve(c5, 0, c6, 0, c_empty)
90 if nx_result_is_err(r3) == 1 { return 20 }
91 if nx_clause_is_empty(c_empty) != 1 { return 21 }
92 println(" Test 3 resolve {p(a)} with {~p(a)} -> {} (empty = contradiction) PASS" as *u8)
93
94 // Test 4: Same-sign literals -> not complementary -> ERR
95 let c7: *Clause = nx_clause_new()
96 let _r7: *NxResult = nx_clause_add(c7, nx_lit_make(NX_LIT_POS, atom_p_a))
97 let c8: *Clause = nx_clause_new()
98 let _r8: *NxResult = nx_clause_add(c8, nx_lit_make(NX_LIT_POS, atom_p_a)) // also positive
99 let c_out4: *Clause = nx_clause_new()
100 let r4: *NxResult = nx_resolve(c7, 0, c8, 0, c_out4)
101 if nx_result_is_err(r4) == 0 { return 30 }
102 print(" Test 4 same-sign literals -> ERR=" as *u8)
103 print(nx_err_name(nx_result_err_code(r4))); println(" PASS" as *u8)
104
105 println("" as *u8)
106 println("=== ALL 4 binary resolution tests PASS ===" as *u8)
107 return 0
108}