nx_subsumption_test.nx source
↩ module page · 108 lines · 5726 B
1// nx_subsumption_test.nx -- forward subsumption 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"
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
15
16const VAR_X: nx_int = 1
17
18// ---------- helpers ------------------------------------------------
19func mk_atom1(sym: nx_int, child: *Term) -> *Term {
20 let a: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
21 a.kind = child.kind; a.sym = child.sym
22 a.n_args = child.n_args; a.args = child.args
23 return nx_term_app(sym, 1, a)
24}
25
26func report(name: *u8, expected: nx_int, actual: nx_int) -> nx_int {
27 print(" " as *u8); print(name); print(" -> " as *u8)
28 print(nx_subsumes_verdict_name(actual))
29 if actual == expected { println(" PASS" as *u8); return 0 }
30 print(" (expected " as *u8); print(nx_subsumes_verdict_name(expected)); println(") FAIL" as *u8)
31 return 1
32}
33
34func main() -> nx_exit {
35 println("=== Forward subsumption smoke ===" as *u8)
36
37 var fails: nx_int = 0
38
39 // ---------- Test 1: trivial subset ---------------------------
40 // C = {p(a)}, D = {p(a), q(b)} -> SUBSUMES (sigma = empty)
41 let c1: *Clause = nx_clause_new()
42 let _r1: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_P, nx_term_const(SYM_A))))
43 let d1: *Clause = nx_clause_new()
44 let _r2: *NxResult = nx_clause_add(d1, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_P, nx_term_const(SYM_A))))
45 let _r3: *NxResult = nx_clause_add(d1, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_Q, nx_term_const(SYM_B))))
46 fails = fails + report("1. {p(a)} vs {p(a), q(b)}" as *u8, NX_SUBSUMES_YES, nx_subsumes(c1, d1))
47
48 // ---------- Test 2: variable instantiation -------------------
49 // C = {p(x)}, D = {p(a)} -> SUBSUMES via {x -> a}
50 let c2: *Clause = nx_clause_new()
51 let _r4: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_P, nx_term_var(VAR_X))))
52 let d2: *Clause = nx_clause_new()
53 let _r5: *NxResult = nx_clause_add(d2, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_P, nx_term_const(SYM_A))))
54 fails = fails + report("2. {p(x)} vs {p(a)}" as *u8, NX_SUBSUMES_YES, nx_subsumes(c2, d2))
55
56 // ---------- Test 3a: shared var, consistent ------------------
57 // C = {p(x), q(x)}, D = {p(a), q(a)} -> SUBSUMES via {x -> a}
58 let c3: *Clause = nx_clause_new()
59 let _r6: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_P, nx_term_var(VAR_X))))
60 let _r7: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_Q, nx_term_var(VAR_X))))
61 let d3: *Clause = nx_clause_new()
62 let _r8: *NxResult = nx_clause_add(d3, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_P, nx_term_const(SYM_A))))
63 let _r9: *NxResult = nx_clause_add(d3, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_Q, nx_term_const(SYM_A))))
64 fails = fails + report("3a. {p(x),q(x)} vs {p(a),q(a)}" as *u8, NX_SUBSUMES_YES, nx_subsumes(c3, d3))
65
66 // ---------- Test 3b: shared var, INCONSISTENT ----------------
67 // C = {p(x), q(x)}, D = {p(a), q(b)} -> NOT_SUBSUMES
68 // (must bind x to both a and b -- backtracking exhausted)
69 let d3b: *Clause = nx_clause_new()
70 let _ra: *NxResult = nx_clause_add(d3b, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_P, nx_term_const(SYM_A))))
71 let _rb: *NxResult = nx_clause_add(d3b, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_Q, nx_term_const(SYM_B))))
72 fails = fails + report("3b. {p(x),q(x)} vs {p(a),q(b)}" as *u8, NX_SUBSUMES_NO, nx_subsumes(c3, d3b))
73
74 // ---------- Test 4: polarity must match ----------------------
75 // C = {p(x)}, D = {~p(a)} -> NOT_SUBSUMES
76 let d4: *Clause = nx_clause_new()
77 let _rc: *NxResult = nx_clause_add(d4, nx_lit_make(NX_LIT_NEG, mk_atom1(SYM_P, nx_term_const(SYM_A))))
78 fails = fails + report("4. {p(x)} vs {~p(a)}" as *u8, NX_SUBSUMES_NO, nx_subsumes(c2, d4))
79
80 // ---------- Test 5: bigger cannot subsume smaller ------------
81 // C = {p(a), q(a)}, D = {p(a)} -> NOT_SUBSUMES (size guard)
82 let c5: *Clause = nx_clause_new()
83 let _rd: *NxResult = nx_clause_add(c5, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_P, nx_term_const(SYM_A))))
84 let _re: *NxResult = nx_clause_add(c5, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_Q, nx_term_const(SYM_A))))
85 let d5: *Clause = nx_clause_new()
86 let _rf: *NxResult = nx_clause_add(d5, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_P, nx_term_const(SYM_A))))
87 fails = fails + report("5. {p(a),q(a)} vs {p(a)}" as *u8, NX_SUBSUMES_NO, nx_subsumes(c5, d5))
88
89 // ---------- Test 6: backtracking finds a solution ------------
90 // C = {p(x), q(x)}, D = {p(b), q(a), p(a), q(b)}
91 // First match tries (p(x) -> p(b))(x:=b); then q(x)=q(b) -> match D[3]; SUCCEED.
92 // (Either {x:=a} or {x:=b} works; ensures search explores beyond
93 // the first candidate.)
94 let d6: *Clause = nx_clause_new()
95 let _rg: *NxResult = nx_clause_add(d6, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_P, nx_term_const(SYM_B))))
96 let _rh: *NxResult = nx_clause_add(d6, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_Q, nx_term_const(SYM_A))))
97 let _ri: *NxResult = nx_clause_add(d6, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_P, nx_term_const(SYM_A))))
98 let _rj: *NxResult = nx_clause_add(d6, nx_lit_make(NX_LIT_POS, mk_atom1(SYM_Q, nx_term_const(SYM_B))))
99 fails = fails + report("6. {p(x),q(x)} vs {p(b),q(a),p(a),q(b)} (backtrack)" as *u8, NX_SUBSUMES_YES, nx_subsumes(c3, d6))
100
101 println("" as *u8)
102 if fails == 0 {
103 println("=== ALL 6 subsumption tests PASS ===" as *u8)
104 return 0
105 }
106 print("=== " as *u8); print_i64(fails); println(" subsumption tests FAILED ===" as *u8)
107 return 1
108}