nx_clause_weight_test.nx source
↩ module page · 118 lines · 5047 B
1// nx_clause_weight_test.nx -- clause weight + best-first pick 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_subsumption.nx"
10import "nx_tautology.nx"
11import "nx_saturation.nx"
12
13const SYM_A: nx_int = 100
14const SYM_P: nx_int = 200
15const SYM_Q: nx_int = 201
16const SYM_F: nx_int = 250
17const VAR_X: nx_int = 0
18
19func mk_p(p_sym: nx_int, c_sym: nx_int) -> *Term {
20 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
21 arg.kind = NX_TERM_CONST; arg.sym = c_sym; arg.n_args = 0; arg.args = 0 as *Term
22 return nx_term_app(p_sym, 1, arg)
23}
24
25func mk_p_app(p_sym: nx_int, inner: *Term) -> *Term {
26 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
27 arg.kind = inner.kind; arg.sym = inner.sym
28 arg.n_args = inner.n_args; arg.args = inner.args
29 return nx_term_app(p_sym, 1, arg)
30}
31
32func mk_unit(atom: *Term) -> *Clause {
33 let c: *Clause = nx_clause_new()
34 let _r: *NxResult = nx_clause_add(c, nx_lit_make(NX_LIT_POS, atom))
35 return c
36}
37
38func main() -> nx_exit {
39 println("=== Clause weight + best-first pick smoke ===" as *u8)
40 var fails: nx_int = 0
41
42 // ---------- Test 1: clause weight ---------------------------
43 // p(a) -- weight 2 (p + a)
44 let c1: *Clause = mk_unit(mk_p(SYM_P, SYM_A))
45 let w1: nx_int = nx_clause_weight(c1)
46 print(" 1. weight(p(a)) = " as *u8); print_i64(w1); println("" as *u8)
47 if w1 == 2 { println(" PASS" as *u8) }
48 else { println(" FAIL" as *u8); fails = fails + 1 }
49
50 // ---------- Test 2: deeper term weights more -----------------
51 // p(f(a)) -- weight 3 (p + f + a)
52 let c2: *Clause = mk_unit(mk_p_app(SYM_P, mk_p(SYM_F, SYM_A)))
53 let w2: nx_int = nx_clause_weight(c2)
54 print(" 2. weight(p(f(a))) = " as *u8); print_i64(w2); println("" as *u8)
55 if w2 == 3 { println(" PASS" as *u8) }
56 else { println(" FAIL" as *u8); fails = fails + 1 }
57
58 // ---------- Test 3: multi-literal clause sum ----------------
59 // {p(a), q(a)} -- weight 4 (2 + 2)
60 let c3: *Clause = nx_clause_new()
61 let _r3a: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p(SYM_P, SYM_A)))
62 let _r3b: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_p(SYM_Q, SYM_A)))
63 let w3: nx_int = nx_clause_weight(c3)
64 print(" 3. weight({p(a),q(a)}) = " as *u8); print_i64(w3); println("" as *u8)
65 if w3 == 4 { println(" PASS" as *u8) }
66 else { println(" FAIL" as *u8); fails = fails + 1 }
67
68 // ---------- Test 4: variable counts as 1 --------------------
69 // p(X) -- weight 2 (p + X)
70 let var_atom: *Term = nx_term_var(VAR_X)
71 let c4: *Clause = mk_unit(mk_p_app(SYM_P, var_atom))
72 let w4: nx_int = nx_clause_weight(c4)
73 print(" 4. weight(p(X)) = " as *u8); print_i64(w4); println("" as *u8)
74 if w4 == 2 { println(" PASS" as *u8) }
75 else { println(" FAIL" as *u8); fails = fails + 1 }
76
77 // ---------- Test 5: best-first picks lightest first ---------
78 // Queue (in insertion order): {p(f(a))} (w=3), {p(a)} (w=2), {q(a)} (w=2)
79 // Best-first should pick {p(a)} (or {q(a)}) first (lightest), not
80 // {p(f(a))}.
81 let s: *Saturation = nx_saturation_new(50)
82 let _u1: *NxResult = nx_sat_add_unproc(s, mk_unit(mk_p_app(SYM_P, mk_p(SYM_F, SYM_A)))) // w=3
83 let _u2: *NxResult = nx_sat_add_unproc(s, mk_unit(mk_p(SYM_P, SYM_A))) // w=2
84 let _u3: *NxResult = nx_sat_add_unproc(s, mk_unit(mk_p(SYM_Q, SYM_A))) // w=2
85
86 let pick1: *Clause = nx_sat_pick_given_best_first(s)
87 let pw1: nx_int = nx_clause_weight(pick1)
88 print(" 5. first pick weight = " as *u8); print_i64(pw1); println("" as *u8)
89 if pw1 == 2 {
90 println(" lightest picked first PASS" as *u8)
91 } else { println(" wrong weight FAIL" as *u8); fails = fails + 1 }
92
93 // ---------- Test 6: subsequent picks see remaining lights ----
94 let pick2: *Clause = nx_sat_pick_given_best_first(s)
95 let pw2: nx_int = nx_clause_weight(pick2)
96 print(" 6. second pick weight = " as *u8); print_i64(pw2); println("" as *u8)
97 if pw2 == 2 { println(" other w=2 picked next PASS" as *u8) }
98 else { println(" FAIL" as *u8); fails = fails + 1 }
99
100 let pick3: *Clause = nx_sat_pick_given_best_first(s)
101 let pw3: nx_int = nx_clause_weight(pick3)
102 print(" 7. third pick weight = " as *u8); print_i64(pw3); println("" as *u8)
103 if pw3 == 3 { println(" heaviest last PASS" as *u8) }
104 else { println(" FAIL" as *u8); fails = fails + 1 }
105
106 let pick4: *Clause = nx_sat_pick_given_best_first(s)
107 if (pick4 as nx_int) == 0 {
108 println(" 8. queue exhausted -> null PASS" as *u8)
109 } else { println(" 8. expected null FAIL" as *u8); fails = fails + 1 }
110
111 println("" as *u8)
112 if fails == 0 {
113 println("=== ALL 8 weight + best-first tests PASS ===" as *u8)
114 return 0
115 }
116 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
117 return 1
118}