nx_selection_test.nx source
↩ module page · 105 lines · 4634 B
1// nx_selection_test.nx -- selection function 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_term_order.nx"
10import "nx_selection.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_F: nx_int = 250
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_unary_app(p_sym: nx_int, child: *Term) -> *Term {
25 let buf: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
26 buf.kind = child.kind; buf.sym = child.sym
27 buf.n_args = child.n_args; buf.args = child.args
28 return nx_term_app(p_sym, 1, buf)
29}
30
31func main() -> nx_exit {
32 println("=== Literal selection smoke ===" as *u8)
33 var fails: nx_int = 0
34
35 // Build a clause: {p(a), ~q(a), p(b)}
36 let c: *Clause = nx_clause_new()
37 let _r1: *NxResult = nx_clause_add(c, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
38 let _r2: *NxResult = nx_clause_add(c, nx_lit_make(NX_LIT_NEG, mk_p(SYM_Q, SYM_A)))
39 let _r3: *NxResult = nx_clause_add(c, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_B)))
40
41 // ---------- Test 1: first negative -> idx 1 ------------------
42 let neg_idx: nx_int = nx_select_first_negative(c)
43 print(" 1. first_negative({p(a),~q(a),p(b)}) -> idx=" as *u8); print_i64(neg_idx); println("" as *u8)
44 if neg_idx == 1 { println(" PASS" as *u8) }
45 else { println(" FAIL" as *u8); fails = fails + 1 }
46
47 // ---------- Test 2: first positive -> idx 0 ------------------
48 let pos_idx: nx_int = nx_select_first_positive(c)
49 print(" 2. first_positive(...) -> idx=" as *u8); print_i64(pos_idx); println("" as *u8)
50 if pos_idx == 0 { println(" PASS" as *u8) }
51 else { println(" FAIL" as *u8); fails = fails + 1 }
52
53 // ---------- Test 3: last -> idx 2 ----------------------------
54 let last_idx: nx_int = nx_select_last(c)
55 print(" 3. last(...) -> idx=" as *u8); print_i64(last_idx); println("" as *u8)
56 if last_idx == 2 { println(" PASS" as *u8) }
57 else { println(" FAIL" as *u8); fails = fails + 1 }
58
59 // ---------- Test 4: empty clause selectors return -1 ---------
60 let empty: *Clause = nx_clause_new()
61 let neg_e: nx_int = nx_select_first_negative(empty)
62 let last_e: nx_int = nx_select_last(empty)
63 if neg_e == 0 - 1 {
64 if last_e == 0 - 1 {
65 println(" 4. empty clause -> -1 / -1 PASS" as *u8)
66 } else { println(" 4. last on empty wrong FAIL" as *u8); fails = fails + 1 }
67 } else { println(" 4. neg on empty wrong FAIL" as *u8); fails = fails + 1 }
68
69 // ---------- Test 5: all-positive -> first_negative = -1 ------
70 let all_pos: *Clause = nx_clause_new()
71 let _ra: *NxResult = nx_clause_add(all_pos, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
72 let _rb: *NxResult = nx_clause_add(all_pos, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
73 let no_neg: nx_int = nx_select_first_negative(all_pos)
74 if no_neg == 0 - 1 {
75 println(" 5. all-positive clause -> first_neg = -1 PASS" as *u8)
76 } else { println(" 5. spurious neg index FAIL" as *u8); fails = fails + 1 }
77
78 // ---------- Test 6: KBO maximal ------------------------------
79 // Clause: {p(a), p(f(a))}. Atoms p(a) and p(f(a)).
80 // f(a) > a in KBO (weight 2 vs 1), so p(f(a)) > p(a) by lex.
81 // Expected: select_kbo_maximal -> idx 1.
82 let st: *KboState = nx_kbo_new(1)
83 let _rs1: *NxResult = nx_kbo_register(st, SYM_A, 1, 10, 0)
84 let _rs2: *NxResult = nx_kbo_register(st, SYM_F, 1, 20, 1)
85 let _rs3: *NxResult = nx_kbo_register(st, SYM_P, 1, 5, 1)
86
87 let kclause: *Clause = nx_clause_new()
88 let _rk1: *NxResult = nx_clause_add(kclause, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
89 let _rk2: *NxResult = nx_clause_add(kclause, nx_lit_make(NX_LIT_POS,
90 mk_unary_app(SYM_P, mk_unary_app(SYM_F, nx_term_const(SYM_A)))))
91
92 let kmax: nx_int = nx_select_kbo_maximal(st, kclause, 4)
93 print(" 6. kbo_maximal({p(a), p(f(a))}) -> idx=" as *u8); print_i64(kmax); println("" as *u8)
94 if kmax == 1 {
95 println(" p(f(a)) is bigger PASS" as *u8)
96 } else { println(" wrong index FAIL" as *u8); fails = fails + 1 }
97
98 println("" as *u8)
99 if fails == 0 {
100 println("=== ALL 6 selection tests PASS ===" as *u8)
101 return 0
102 }
103 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
104 return 1
105}