nx_tptp_emit_test.nx source
↩ module page · 157 lines · 6224 B
1// nx_tptp_emit_test.nx -- emitter smoke + parser round-trip.
2
3import "nx_syscalls.nx"
4import "nx_runtime.nx"
5import "nx_tier.nx"
6import "nx_str.nx"
7import "nx_result.nx"
8import "nx_unify.nx"
9import "nx_resolution.nx"
10import "nx_tptp_symtab.nx"
11import "nx_tptp_term.nx"
12import "nx_tptp_formula.nx"
13import "nx_tptp_emit.nx"
14
15const SYM_EQ: nx_int = 50
16
17// Inline a string into a writable buffer for parsing.
18func mk_input(s: *u8) -> *u8 {
19 let len: nx_int = nx_str_len(s)
20 let buf: *u8 = sys_mmap((len + 1) as i64)
21 var i: nx_int = 0
22 while i < len { buf[i] = s[i]; i = i + 1 }
23 buf[len] = 0
24 return buf
25}
26
27// Round-trip: parse `input`, emit it back, return the emitted string.
28func roundtrip(input: *u8) -> *u8 {
29 let st: *TptpSymtab = nx_tptp_symtab_new()
30 let buf_in: *u8 = mk_input(input)
31 let len: nx_int = nx_str_len(input)
32 let pos: *nx_int = sys_mmap(8) as *nx_int
33 pos[0] = 0
34 nx_tptp_symtab_reset_vars(st)
35 let c: *Clause = nx_tptp_parse_cnf_clause(buf_in, len, pos, st, SYM_EQ)
36 if (c as nx_int) == 0 { return 0 as *u8 }
37
38 let out_buf: *u8 = sys_mmap(512)
39 let out_pos: *nx_int = sys_mmap(8) as *nx_int
40 out_pos[0] = 0
41 let r: nx_int = nx_emit_clause_body(c, st, SYM_EQ, out_buf, out_pos, 512)
42 if r < 0 { return 0 as *u8 }
43 if out_pos[0] < 512 { out_buf[out_pos[0]] = 0 }
44 return out_buf
45}
46
47// Parse `input`, emit, then parse the EMITTED text -- assert n_lits
48// matches. Strong round-trip: the emitter produces text the parser
49// can read back into an equivalent clause.
50func roundtrip_lit_count(input: *u8, expected_n: nx_int) -> nx_int {
51 let st: *TptpSymtab = nx_tptp_symtab_new()
52 let buf_in: *u8 = mk_input(input)
53 let len: nx_int = nx_str_len(input)
54 let pos: *nx_int = sys_mmap(8) as *nx_int
55 pos[0] = 0
56 nx_tptp_symtab_reset_vars(st)
57 let c: *Clause = nx_tptp_parse_cnf_clause(buf_in, len, pos, st, SYM_EQ)
58 if (c as nx_int) == 0 { return 0 - 1 }
59
60 let out_buf: *u8 = sys_mmap(512)
61 let out_pos: *nx_int = sys_mmap(8) as *nx_int
62 out_pos[0] = 0
63 if nx_emit_clause_body(c, st, SYM_EQ, out_buf, out_pos, 512) < 0 { return 0 - 1 }
64 out_buf[out_pos[0]] = 0
65 let emitted_len: nx_int = out_pos[0]
66
67 // Re-parse the emitted text with a fresh symtab.
68 let st2: *TptpSymtab = nx_tptp_symtab_new()
69 let pos2: *nx_int = sys_mmap(8) as *nx_int
70 pos2[0] = 0
71 nx_tptp_symtab_reset_vars(st2)
72 let c2: *Clause = nx_tptp_parse_cnf_clause(out_buf, emitted_len, pos2, st2, SYM_EQ)
73 if (c2 as nx_int) == 0 { return 0 - 1 }
74 if c2.n_lits == expected_n { return 1 }
75 return 0
76}
77
78func main() -> nx_exit {
79 println("=== TPTP CNF emitter smoke ===" as *u8)
80 var fails: nx_int = 0
81
82 // ---------- Test 1: emit a simple atom ----------------------
83 let s1: *u8 = roundtrip("p(a)" as *u8)
84 if (s1 as nx_int) == 0 {
85 println(" 1. roundtrip(p(a)) -> NULL FAIL" as *u8); fails = fails + 1
86 } else {
87 print(" 1. roundtrip(p(a)) -> '" as *u8); print(s1); print("'" as *u8)
88 if nx_str_eq(s1, "p(a)" as *u8) == 1 { println(" PASS" as *u8) }
89 else { println(" text differs FAIL" as *u8); fails = fails + 1 }
90 }
91
92 // ---------- Test 2: negation prefix -------------------------
93 let s2: *u8 = roundtrip("~p(a)" as *u8)
94 if (s2 as nx_int) == 0 {
95 println(" 2. roundtrip(~p(a)) -> NULL FAIL" as *u8); fails = fails + 1
96 } else {
97 print(" 2. roundtrip(~p(a)) -> '" as *u8); print(s2); println("'" as *u8)
98 if nx_str_eq(s2, "~p(a)" as *u8) == 1 { println(" PASS" as *u8) }
99 else { println(" text differs FAIL" as *u8); fails = fails + 1 }
100 }
101
102 // ---------- Test 3: equality emitted as "lhs = rhs" ---------
103 let s3: *u8 = roundtrip("a = b" as *u8)
104 if (s3 as nx_int) == 0 {
105 println(" 3. roundtrip(a=b) -> NULL FAIL" as *u8); fails = fails + 1
106 } else {
107 print(" 3. roundtrip(a=b) -> '" as *u8); print(s3); println("'" as *u8)
108 if nx_str_eq(s3, "a = b" as *u8) == 1 { println(" PASS" as *u8) }
109 else { println(" text differs FAIL" as *u8); fails = fails + 1 }
110 }
111
112 // ---------- Test 4: inequality emitted as "lhs != rhs" ------
113 let s4: *u8 = roundtrip("a != b" as *u8)
114 if (s4 as nx_int) == 0 {
115 println(" 4. roundtrip(a!=b) -> NULL FAIL" as *u8); fails = fails + 1
116 } else {
117 print(" 4. roundtrip(a!=b) -> '" as *u8); print(s4); println("'" as *u8)
118 if nx_str_eq(s4, "a != b" as *u8) == 1 { println(" PASS" as *u8) }
119 else { println(" text differs FAIL" as *u8); fails = fails + 1 }
120 }
121
122 // ---------- Test 5: disjunction -----------------------------
123 let s5: *u8 = roundtrip("p(a) | ~q(b)" as *u8)
124 if (s5 as nx_int) == 0 {
125 println(" 5. roundtrip(p|~q) -> NULL FAIL" as *u8); fails = fails + 1
126 } else {
127 print(" 5. roundtrip(p|~q) -> '" as *u8); print(s5); println("'" as *u8)
128 if nx_str_eq(s5, "p(a) | ~q(b)" as *u8) == 1 { println(" PASS" as *u8) }
129 else { println(" text differs FAIL" as *u8); fails = fails + 1 }
130 }
131
132 // ---------- Test 6: variables preserved --------------------
133 let s6: *u8 = roundtrip("p(X)" as *u8)
134 if (s6 as nx_int) == 0 {
135 println(" 6. roundtrip(p(X)) -> NULL FAIL" as *u8); fails = fails + 1
136 } else {
137 print(" 6. roundtrip(p(X)) -> '" as *u8); print(s6); println("'" as *u8)
138 if nx_str_eq(s6, "p(X)" as *u8) == 1 { println(" PASS" as *u8) }
139 else { println(" text differs FAIL" as *u8); fails = fails + 1 }
140 }
141
142 // ---------- Test 7: full round-trip lit-count check --------
143 // Parse, emit, re-parse -- the result should have the same
144 // number of literals.
145 let r7: nx_int = roundtrip_lit_count("p(X) | q(a) | ~r(b)" as *u8, 3)
146 if r7 == 1 {
147 println(" 7. round-trip lit count match (3 lits) PASS" as *u8)
148 } else { println(" 7. round-trip mismatch FAIL" as *u8); fails = fails + 1 }
149
150 println("" as *u8)
151 if fails == 0 {
152 println("=== ALL 7 emitter tests PASS ===" as *u8)
153 return 0
154 }
155 print("=== " as *u8); print_i64(fails); println(" tests FAILED ===" as *u8)
156 return 1
157}