nx_paramodulation_test.nx source
↩ module page · 175 lines · 7923 B
1// nx_paramodulation_test.nx -- paramodulation 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_paramodulation.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_G: nx_int = 201
16const SYM_P: nx_int = 300
17const SYM_EQ: nx_int = 50
18
19const VAR_X: nx_int = 0
20
21// helpers ---------------------------------------------------------
22func mk_eq(t1: *Term, t2: *Term) -> *Term {
23 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
24 let a0: *Term = args
25 a0.kind = t1.kind; a0.sym = t1.sym; a0.n_args = t1.n_args; a0.args = t1.args
26 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
27 a1.kind = t2.kind; a1.sym = t2.sym; a1.n_args = t2.n_args; a1.args = t2.args
28 return nx_term_app(SYM_EQ, 2, args)
29}
30
31func mk_p(c: *Term) -> *Term {
32 let buf: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
33 buf.kind = c.kind; buf.sym = c.sym
34 buf.n_args = c.n_args; buf.args = c.args
35 return nx_term_app(SYM_P, 1, buf)
36}
37
38func mk_f(c: *Term) -> *Term {
39 let buf: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
40 buf.kind = c.kind; buf.sym = c.sym
41 buf.n_args = c.n_args; buf.args = c.args
42 return nx_term_app(SYM_F, 1, buf)
43}
44
45func mk_g(c: *Term) -> *Term {
46 let buf: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
47 buf.kind = c.kind; buf.sym = c.sym
48 buf.n_args = c.n_args; buf.args = c.args
49 return nx_term_app(SYM_G, 1, buf)
50}
51
52func main() -> nx_exit {
53 println("=== Paramodulation smoke ===" as *u8)
54 var fails: nx_int = 0
55
56 // ---------- Test 1: simple paramod ---------------------------
57 // Equation: {a = b}
58 // Target: {p(a)}
59 // Expected: {p(b)}
60 let eq1: *Clause = nx_clause_new()
61 let _r1a: *NxResult = nx_clause_add(eq1, nx_lit_make(NX_LIT_POS,
62 mk_eq(nx_term_const(SYM_A), nx_term_const(SYM_B))))
63 let tg1: *Clause = nx_clause_new()
64 let _r1b: *NxResult = nx_clause_add(tg1, nx_lit_make(NX_LIT_POS,
65 mk_p(nx_term_const(SYM_A))))
66 let out1: *Clause = nx_clause_new()
67 let r1: *NxResult = nx_paramodulate(eq1, 0, tg1, 0, SYM_EQ, out1)
68 if nx_result_is_err(r1) == 1 {
69 println("1. paramod {a=b} into {p(a)} -> ERR FAIL" as *u8); fails = fails + 1
70 } else {
71 if out1.n_lits == 1 {
72 let l: *Literal = nx_clause_lit_at(out1, 0)
73 let inner: *Term = nx_term_arg(l.atom, 0)
74 if l.atom.sym == SYM_P {
75 if inner.sym == SYM_B {
76 println("1. paramod {a=b} into {p(a)} -> {p(b)} PASS" as *u8)
77 } else { print("1. inner.sym=" as *u8); print_i64(inner.sym); println(" FAIL" as *u8); fails = fails + 1 }
78 } else { println("1. wrong head FAIL" as *u8); fails = fails + 1 }
79 } else { print("1. n_lits=" as *u8); print_i64(out1.n_lits); println(" FAIL" as *u8); fails = fails + 1 }
80 }
81
82 // ---------- Test 2: paramod with variable -- f(X)=g(X) into p(f(c))
83 // Equation: {f(X) = g(X)}
84 // Target: {p(f(c))}
85 // Expected: {p(g(c))} -- unify f(X) with f(c), σ={X->c}, replace
86 // f(c) (the subterm of p) with g(c).
87 let eq2: *Clause = nx_clause_new()
88 let _r2a: *NxResult = nx_clause_add(eq2, nx_lit_make(NX_LIT_POS,
89 mk_eq(mk_f(nx_term_var(VAR_X)), mk_g(nx_term_var(VAR_X)))))
90 let tg2: *Clause = nx_clause_new()
91 let _r2b: *NxResult = nx_clause_add(tg2, nx_lit_make(NX_LIT_POS,
92 mk_p(mk_f(nx_term_const(SYM_C)))))
93 let out2: *Clause = nx_clause_new()
94 let r2: *NxResult = nx_paramodulate(eq2, 0, tg2, 0, SYM_EQ, out2)
95 if nx_result_is_err(r2) == 1 {
96 println("2. paramod {f(X)=g(X)} into {p(f(c))} -> ERR FAIL" as *u8); fails = fails + 1
97 } else {
98 if out2.n_lits == 1 {
99 let l: *Literal = nx_clause_lit_at(out2, 0)
100 let inner: *Term = nx_term_arg(l.atom, 0)
101 if inner.sym == SYM_G {
102 let inner_arg: *Term = nx_term_arg(inner, 0)
103 if inner_arg.sym == SYM_C {
104 println("2. paramod {f(X)=g(X)} into {p(f(c))} -> {p(g(c))} PASS" as *u8)
105 } else { print("2. inner_arg.sym=" as *u8); print_i64(inner_arg.sym); println(" FAIL" as *u8); fails = fails + 1 }
106 } else { print("2. inner.sym=" as *u8); print_i64(inner.sym); println(" FAIL" as *u8); fails = fails + 1 }
107 } else { print("2. n_lits=" as *u8); print_i64(out2.n_lits); println(" FAIL" as *u8); fails = fails + 1 }
108 }
109
110 // ---------- Test 3: no unification possible ------------------
111 // Equation: {a = b}
112 // Target: {p(c)} -- c doesn't unify with a
113 // Expected: ERR=NOT_FOUND
114 let tg3: *Clause = nx_clause_new()
115 let _r3: *NxResult = nx_clause_add(tg3, nx_lit_make(NX_LIT_POS,
116 mk_p(nx_term_const(SYM_C))))
117 let out3: *Clause = nx_clause_new()
118 let r3: *NxResult = nx_paramodulate(eq1, 0, tg3, 0, SYM_EQ, out3)
119 if nx_result_is_err(r3) == 1 {
120 if nx_result_err_code(r3) == NX_ERR_NOT_FOUND {
121 println("3. paramod {a=b} into {p(c)} -> NOT_FOUND PASS" as *u8)
122 } else { print("3. err_code=" as *u8); print_i64(nx_result_err_code(r3)); println(" FAIL" as *u8); fails = fails + 1 }
123 } else { println("3. expected ERR FAIL" as *u8); fails = fails + 1 }
124
125 // ---------- Test 4: symmetric direction ----------------------
126 // Equation: {b = a} (RHS of equation is what matches; flip)
127 // Target: {p(a)}
128 // Expected: {p(b)}
129 let eq4: *Clause = nx_clause_new()
130 let _r4a: *NxResult = nx_clause_add(eq4, nx_lit_make(NX_LIT_POS,
131 mk_eq(nx_term_const(SYM_B), nx_term_const(SYM_A))))
132 let out4: *Clause = nx_clause_new()
133 let r4: *NxResult = nx_paramodulate(eq4, 0, tg1, 0, SYM_EQ, out4)
134 if nx_result_is_err(r4) == 1 {
135 println("4. paramod {b=a} into {p(a)} -> ERR FAIL" as *u8); fails = fails + 1
136 } else {
137 if out4.n_lits == 1 {
138 let l: *Literal = nx_clause_lit_at(out4, 0)
139 let inner: *Term = nx_term_arg(l.atom, 0)
140 if inner.sym == SYM_B {
141 println("4. paramod {b=a} into {p(a)} -> {p(b)} (symmetric) PASS" as *u8)
142 } else { print("4. inner.sym=" as *u8); print_i64(inner.sym); println(" FAIL" as *u8); fails = fails + 1 }
143 } else { println("4. n_lits wrong FAIL" as *u8); fails = fails + 1 }
144 }
145
146 // ---------- Test 5: extra literals carry through -------------
147 // Equation: {a = b, q(c)} -- two-literal equational clause
148 // Target: {p(a)}
149 // Expected: {p(b), q(c)} -- residual q(c) carries through
150 let SYM_Q: nx_int = 301
151 let eq5: *Clause = nx_clause_new()
152 let _r5a: *NxResult = nx_clause_add(eq5, nx_lit_make(NX_LIT_POS,
153 mk_eq(nx_term_const(SYM_A), nx_term_const(SYM_B))))
154 let q_atom: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
155 q_atom.kind = NX_TERM_CONST; q_atom.sym = SYM_C; q_atom.n_args = 0; q_atom.args = 0 as *Term
156 let q_app: *Term = nx_term_app(SYM_Q, 1, q_atom)
157 let _r5b: *NxResult = nx_clause_add(eq5, nx_lit_make(NX_LIT_POS, q_app))
158 let out5: *Clause = nx_clause_new()
159 let r5: *NxResult = nx_paramodulate(eq5, 0, tg1, 0, SYM_EQ, out5)
160 if nx_result_is_err(r5) == 1 {
161 println("5. paramod with residual -> ERR FAIL" as *u8); fails = fails + 1
162 } else {
163 if out5.n_lits == 2 {
164 println("5. paramod {a=b,q(c)} into {p(a)} -> 2 literals (p(b)+q(c)) PASS" as *u8)
165 } else { print("5. n_lits=" as *u8); print_i64(out5.n_lits); println(" FAIL" as *u8); fails = fails + 1 }
166 }
167
168 println("" as *u8)
169 if fails == 0 {
170 println("=== ALL 5 paramodulation tests PASS ===" as *u8)
171 return 0
172 }
173 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
174 return 1
175}