nx_eq_factor_test.nx source
↩ module page · 144 lines · 6699 B
1// nx_eq_factor_test.nx -- equality factoring 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_eq_factor.nx"
10
11const SYM_A: nx_int = 100
12const SYM_B: nx_int = 101
13const SYM_C: nx_int = 102
14const SYM_F: nx_int = 200
15const SYM_P: nx_int = 300
16const SYM_EQ: nx_int = 50
17const VAR_X: nx_int = 0
18
19func mk_eq_atom(t1: *Term, t2: *Term) -> *Term {
20 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
21 let a0: *Term = args
22 a0.kind = t1.kind; a0.sym = t1.sym; a0.n_args = t1.n_args; a0.args = t1.args
23 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
24 a1.kind = t2.kind; a1.sym = t2.sym; a1.n_args = t2.n_args; a1.args = t2.args
25 return nx_term_app(SYM_EQ, 2, args)
26}
27
28func mk_unary_app(p_sym: nx_int, child: *Term) -> *Term {
29 let buf: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
30 buf.kind = child.kind; buf.sym = child.sym
31 buf.n_args = child.n_args; buf.args = child.args
32 return nx_term_app(p_sym, 1, buf)
33}
34
35func main() -> nx_exit {
36 println("=== Equality factoring smoke ===" as *u8)
37 var fails: nx_int = 0
38
39 // ---------- Test 1: classic 2-literal case ------------------
40 // C = {a = b, a = c}
41 // Factor on i=0, j=1: unify(a, a) = empty σ
42 // Conclusion: {a = b, b ≄ c}
43 let c1: *Clause = nx_clause_new()
44 let _r1a: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS,
45 mk_eq_atom(nx_term_const(SYM_A), nx_term_const(SYM_B))))
46 let _r1b: *NxResult = nx_clause_add(c1, nx_lit_make(NX_LIT_POS,
47 mk_eq_atom(nx_term_const(SYM_A), nx_term_const(SYM_C))))
48
49 let out1: *Clause = nx_clause_new()
50 let r1: *NxResult = nx_eq_factor(c1, 0, 1, SYM_EQ, out1)
51 if nx_result_is_err(r1) == 1 {
52 println("1. {a=b, a=c} factor -> ERR FAIL" as *u8); fails = fails + 1
53 } else {
54 if out1.n_lits == 2 {
55 // First lit kept = a=b; second = b ≄ c (NEG eq)
56 let kept: *Literal = nx_clause_lit_at(out1, 0)
57 let neg: *Literal = nx_clause_lit_at(out1, 1)
58 if kept.sign == NX_LIT_POS {
59 if neg.sign == NX_LIT_NEG {
60 if neg.atom.sym == SYM_EQ {
61 let l: *Term = nx_term_arg(neg.atom, 0)
62 let r: *Term = nx_term_arg(neg.atom, 1)
63 if l.sym == SYM_B {
64 if r.sym == SYM_C {
65 println("1. {a=b, a=c} -> {a=b, b≄c} PASS" as *u8)
66 } else { println("1. RHS not c FAIL" as *u8); fails = fails + 1 }
67 } else { println("1. LHS not b FAIL" as *u8); fails = fails + 1 }
68 } else { println("1. neg head wrong FAIL" as *u8); fails = fails + 1 }
69 } else { println("1. second lit not NEG FAIL" as *u8); fails = fails + 1 }
70 } else { println("1. first lit not POS FAIL" as *u8); fails = fails + 1 }
71 } else { print("1. n_lits=" as *u8); print_i64(out1.n_lits); println(" FAIL" as *u8); fails = fails + 1 }
72 }
73
74 // ---------- Test 2: variable LHS unifies --------------------
75 // C = {f(X) = a, f(b) = c}
76 // Factor on 0, 1: unify(f(X), f(b)) = {X := b}
77 // Conclusion: {f(b) = a, a ≄ c} (X replaced with b)
78 let c2: *Clause = nx_clause_new()
79 let _r2a: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS,
80 mk_eq_atom(mk_unary_app(SYM_F, nx_term_var(VAR_X)), nx_term_const(SYM_A))))
81 let _r2b: *NxResult = nx_clause_add(c2, nx_lit_make(NX_LIT_POS,
82 mk_eq_atom(mk_unary_app(SYM_F, nx_term_const(SYM_B)), nx_term_const(SYM_C))))
83
84 let out2: *Clause = nx_clause_new()
85 let r2: *NxResult = nx_eq_factor(c2, 0, 1, SYM_EQ, out2)
86 if nx_result_is_err(r2) == 1 {
87 println("2. {f(X)=a, f(b)=c} factor -> ERR FAIL" as *u8); fails = fails + 1
88 } else {
89 if out2.n_lits == 2 {
90 let kept: *Literal = nx_clause_lit_at(out2, 0)
91 let f_arg: *Term = nx_term_arg(kept.atom, 0)
92 let inner: *Term = nx_term_arg(f_arg, 0)
93 if inner.sym == SYM_B {
94 println("2. {f(X)=a, f(b)=c} -> {f(b)=a, a≄c} PASS" as *u8)
95 } else { print("2. inner.sym=" as *u8); print_i64(inner.sym); println(" FAIL" as *u8); fails = fails + 1 }
96 } else { println("2. wrong count FAIL" as *u8); fails = fails + 1 }
97 }
98
99 // ---------- Test 3: incompatible LHS rejects ---------------
100 // C = {a = b, c = d} -- a doesn't unify with c.
101 let c3: *Clause = nx_clause_new()
102 let _r3a: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS,
103 mk_eq_atom(nx_term_const(SYM_A), nx_term_const(SYM_B))))
104 let _r3b: *NxResult = nx_clause_add(c3, nx_lit_make(NX_LIT_POS,
105 mk_eq_atom(nx_term_const(SYM_C), nx_term_const(SYM_A)))) // c = a
106
107 let out3: *Clause = nx_clause_new()
108 let r3: *NxResult = nx_eq_factor(c3, 0, 1, SYM_EQ, out3)
109 if nx_result_is_err(r3) == 1 {
110 println("3. {a=b, c=a} factor -> ERR (a/c don't unify) PASS" as *u8)
111 } else { println("3. expected ERR FAIL" as *u8); fails = fails + 1 }
112
113 // ---------- Test 4: non-equality literal rejects ------------
114 // C = {p(a), a = b} -- index 0 isn't an equality.
115 let c4: *Clause = nx_clause_new()
116 let p_atom: *Term = mk_unary_app(SYM_P, nx_term_const(SYM_A))
117 let _r4a: *NxResult = nx_clause_add(c4, nx_lit_make(NX_LIT_POS, p_atom))
118 let _r4b: *NxResult = nx_clause_add(c4, nx_lit_make(NX_LIT_POS,
119 mk_eq_atom(nx_term_const(SYM_A), nx_term_const(SYM_B))))
120
121 let out4: *Clause = nx_clause_new()
122 let r4: *NxResult = nx_eq_factor(c4, 0, 1, SYM_EQ, out4)
123 if nx_result_is_err(r4) == 1 {
124 if nx_result_err_code(r4) == NX_ERR_TAG_MISMATCH {
125 println("4. non-equality at index 0 -> TAG_MISMATCH PASS" as *u8)
126 } else { println("4. wrong err FAIL" as *u8); fails = fails + 1 }
127 } else { println("4. expected ERR FAIL" as *u8); fails = fails + 1 }
128
129 // ---------- Test 5: same-index reject ----------------------
130 let r5: *NxResult = nx_eq_factor(c1, 0, 0, SYM_EQ, nx_clause_new())
131 if nx_result_is_err(r5) == 1 {
132 if nx_result_err_code(r5) == NX_ERR_INVALID_INPUT {
133 println("5. i == j -> INVALID_INPUT PASS" as *u8)
134 } else { println("5. wrong err FAIL" as *u8); fails = fails + 1 }
135 } else { println("5. expected ERR FAIL" as *u8); fails = fails + 1 }
136
137 println("" as *u8)
138 if fails == 0 {
139 println("=== ALL 5 equality-factoring tests PASS ===" as *u8)
140 return 0
141 }
142 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
143 return 1
144}