nx_inst_gen_test.nx source
↩ module page · 132 lines · 6165 B
1// nx_inst_gen_test.nx -- instance generation 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_inst_gen.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 VAR_X: nx_int = 0
16const VAR_Y: nx_int = 1
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 main() -> nx_exit {
31 println("=== Inst-Gen smoke ===" as *u8)
32 var fails: nx_int = 0
33
34 // ---------- Test 1: classic Inst-Gen step -------------------
35 // c1 = {p(X)}, c2 = {~p(a)}
36 // σ = {X := a}
37 // Result: c1_out = {p(a)}, c2_out = {~p(a)}
38 // Note: NEITHER is empty, NEITHER has L removed. They're just
39 // both more specific now.
40 let c1: *Clause = nx_clause_new()
41 let _r1a: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
42 let c2: *Clause = nx_clause_new()
43 let _r1b: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_NEG, mk_p(SYM_P, SYM_A)))
44
45 let c1_out: *Clause = nx_clause_new()
46 let c2_out: *Clause = nx_clause_new()
47 let r1: *NxResult = nx_inst_gen(c1, 0, c2, 0, c1_out, c2_out)
48 if nx_result_is_err(r1) == 1 {
49 println("1. inst_gen({p(X)}, {~p(a)}) -> ERR FAIL" as *u8); fails = fails + 1
50 } else {
51 if c1_out.n_lits == 1 {
52 if c2_out.n_lits == 1 {
53 let l1: *Literal = nx_clause_lit_at(c1_out, 0)
54 let arg1: *Term = nx_term_arg(l1.atom, 0)
55 if arg1.kind == NX_TERM_CONST {
56 if arg1.sym == SYM_A {
57 if l1.sign == NX_LIT_POS {
58 println("1. {p(X)} + {~p(a)} -> {p(a)} + {~p(a)} (both kept, both σ) PASS" as *u8)
59 } else { println("1. c1 sign wrong FAIL" as *u8); fails = fails + 1 }
60 } else { println("1. c1 arg not a FAIL" as *u8); fails = fails + 1 }
61 } else { println("1. c1 arg not CONST -- subst failed FAIL" as *u8); fails = fails + 1 }
62 } else { print("1. c2_out lits=" as *u8); print_i64(c2_out.n_lits); println(" FAIL" as *u8); fails = fails + 1 }
63 } else { print("1. c1_out lits=" as *u8); print_i64(c1_out.n_lits); println(" FAIL" as *u8); fails = fails + 1 }
64 }
65
66 // ---------- Test 2: residual literals carry through ---------
67 // c1 = {p(X), q(X)}, c2 = {~p(a)}
68 // σ = {X := a}
69 // Result: c1_out = {p(a), q(a)} (BOTH literals σ-applied, neither removed)
70 // c2_out = {~p(a)}
71 let c1b: *Clause = nx_clause_new()
72 let _r2a: *NxResult = nx_clause_add(c1b, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_P, VAR_X)))
73 let _r2b: *NxResult = nx_clause_add(c1b, nx_lit_make(NX_LIT_POS, mk_p_var(SYM_Q, VAR_X)))
74
75 let c1b_out: *Clause = nx_clause_new()
76 let c2b_out: *Clause = nx_clause_new()
77 let r2: *NxResult = nx_inst_gen(c1b, 0, c2, 0, c1b_out, c2b_out)
78 if nx_result_is_err(r2) == 1 {
79 println("2. residual carry -> ERR FAIL" as *u8); fails = fails + 1
80 } else {
81 if c1b_out.n_lits == 2 {
82 // Verify q(X) became q(a) under σ.
83 let q_lit: *Literal = nx_clause_lit_at(c1b_out, 1)
84 let q_arg: *Term = nx_term_arg(q_lit.atom, 0)
85 if q_arg.sym == SYM_A {
86 println("2. {p(X),q(X)} + {~p(a)} -> {p(a),q(a)} + {~p(a)} PASS" as *u8)
87 } else { println("2. q arg not σ-applied FAIL" as *u8); fails = fails + 1 }
88 } else { print("2. c1b_out lits=" as *u8); print_i64(c1b_out.n_lits); println(" FAIL" as *u8); fails = fails + 1 }
89 }
90
91 // ---------- Test 3: same-polarity rejects ------------------
92 // Both POS at chosen indices -- not complementary.
93 let c3a: *Clause = nx_clause_new()
94 let _r3a: *NxResult = nx_clause_add(c3a, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
95 let c3b: *Clause = nx_clause_new()
96 let _r3b: *NxResult = nx_clause_add(c3b, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
97
98 let r3: *NxResult = nx_inst_gen(c3a, 0, c3b, 0, nx_clause_new(), nx_clause_new())
99 if nx_result_is_err(r3) == 1 {
100 if nx_result_err_code(r3) == NX_ERR_TAG_MISMATCH {
101 println("3. same-polarity -> TAG_MISMATCH PASS" as *u8)
102 } else { println("3. wrong err code FAIL" as *u8); fails = fails + 1 }
103 } else { println("3. expected ERR FAIL" as *u8); fails = fails + 1 }
104
105 // ---------- Test 4: non-unifiable atoms reject --------------
106 // c1 = {p(a)}, c2 = {~p(b)} -- a doesn't unify with b.
107 let c4a: *Clause = nx_clause_new()
108 let _r4a: *NxResult = nx_clause_add(c4a, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
109 let c4b: *Clause = nx_clause_new()
110 let _r4b: *NxResult = nx_clause_add(c4b, nx_lit_make(NX_LIT_NEG, mk_p(SYM_P, SYM_B)))
111
112 let r4: *NxResult = nx_inst_gen(c4a, 0, c4b, 0, nx_clause_new(), nx_clause_new())
113 if nx_result_is_err(r4) == 1 {
114 println("4. non-unifiable atoms -> ERR PASS" as *u8)
115 } else { println("4. expected ERR FAIL" as *u8); fails = fails + 1 }
116
117 // ---------- Test 5: bad index rejects -----------------------
118 let r5: *NxResult = nx_inst_gen(c1, 5, c2, 0, nx_clause_new(), nx_clause_new())
119 if nx_result_is_err(r5) == 1 {
120 if nx_result_err_code(r5) == NX_ERR_OUT_OF_RANGE {
121 println("5. bad index -> OUT_OF_RANGE PASS" as *u8)
122 } else { println("5. wrong err FAIL" as *u8); fails = fails + 1 }
123 } else { println("5. expected ERR FAIL" as *u8); fails = fails + 1 }
124
125 println("" as *u8)
126 if fails == 0 {
127 println("=== ALL 5 inst-gen tests PASS ===" as *u8)
128 return 0
129 }
130 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
131 return 1
132}