nx_tptp_load.nx source
↩ module page · 210 lines · 8191 B
1// nx_tptp_load.nx -- end-to-end TPTP CNF file loader.
2//
3// Per user directive 2026-05-15: all functionality native to NishiLang,
4// no shell preprocessing or Python. Reads a TPTP file via the native
5// sys_read_file primitive, walks the buffer parsing each cnf(name,
6// role, FORMULA). statement, returns an array of *Clause ready for the
7// saturation loop.
8//
9// Phase 1.6 closure: this is what flips the vs-Vampire CASC bench
10// status from BLOCKED_ON_TPTP_FORMULA_PARSER to UNBLOCKED_FOR_CNF.
11// (FOF formulas still queued for Phase 2; CASC FOF division entries
12// must be CNF-converted before the substrate can solve them today.)
13//
14// Result-typed throughout (per cardinal: no null-as-error sentinels).
15// Caller unwraps via nx_result_unwrap; on error inspects err_code
16// (NX_ERR_FILE_NOT_FOUND / NX_ERR_PARSE_FAILED / NX_ERR_OVERFLOW).
17
18// nx_safety_envelope:
19// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
20// sil_target: SIL1
21// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
22// verdict: NOT_YET_EVALUATED
23
24import "nx_syscalls.nx"
25import "nx_runtime.nx"
26import "nx_tier.nx"
27import "nx_str.nx"
28import "nx_result.nx"
29import "nx_file_result.nx"
30import "nx_unify.nx"
31import "nx_resolution.nx"
32import "nx_tptp_symtab.nx"
33import "nx_tptp_term.nx"
34import "nx_tptp_formula.nx"
35
36const NX_TPTP_LOAD_MAX_CLAUSES: nx_int = 256
37
38struct TptpLoaded {
39 clauses: *Clause, // flat array of NX_TPTP_LOAD_MAX_CLAUSES
40 n: nx_int,
41 symtab: *TptpSymtab, // returned to caller for downstream use
42}
43
44const NX_TPTP_LOADED_BYTES: nx_int = 24
45
46// Skip whitespace + line comments (% ...). Iterative -- no recursion
47// (recursion here was a relic of the codegen-bug-era loader; the bug
48// was fixed in nxc2 riscv.c emit_call so this can stay flat).
49func nx_tptp_load_skip(buf: *u8, n: nx_int, pos: *nx_int) {
50 var p: nx_int = pos[0]
51 while p < n {
52 let c: nx_int = buf[p] as nx_int
53 if c == 32 { p = p + 1 }
54 if c == 9 { p = p + 1 }
55 if c == 10 { p = p + 1 }
56 if c == 13 { p = p + 1 }
57 if c == 37 {
58 // '%' line comment -- consume to newline (or EOF).
59 while p < n {
60 let cc: nx_int = buf[p] as nx_int
61 p = p + 1
62 if cc == 10 { p = p - 0 } // exit-via-loop-condition idiom
63 if cc == 10 {
64 // jump to outer loop continuation
65 pos[0] = p
66 nx_tptp_load_skip(buf, n, pos)
67 return
68 }
69 }
70 }
71 if c != 32 {
72 if c != 9 {
73 if c != 10 {
74 if c != 13 {
75 if c != 37 { pos[0] = p; return }
76 }
77 }
78 }
79 }
80 }
81 pos[0] = p
82}
83
84// Read identifier into out_buf; returns length. Local copy of the
85// term reader's helper -- kept distinct so the loader compiles even
86// if the term parser gains a different ident grammar later.
87func nx_tptp_load_read_ident(buf: *u8, n: nx_int, pos: *nx_int, out_buf: *u8) -> nx_int {
88 var p: nx_int = pos[0]
89 var len: nx_int = 0
90 while p < n {
91 let c: nx_int = buf[p] as nx_int
92 var is_id: nx_int = 0
93 if c >= 65 { if c <= 90 { is_id = 1 } }
94 if c >= 97 { if c <= 122 { is_id = 1 } }
95 if c >= 48 { if c <= 57 { is_id = 1 } }
96 if c == 95 { is_id = 1 }
97 if is_id == 0 {
98 out_buf[len] = 0
99 pos[0] = p
100 return len
101 }
102 if len < (NX_TPTP_SYM_NAME_MAX - 1) {
103 out_buf[len] = buf[p]
104 len = len + 1
105 }
106 p = p + 1
107 }
108 out_buf[len] = 0
109 pos[0] = p
110 return len
111}
112
113// Load a TPTP CNF file from `path`. Returns Result<*TptpLoaded as nx_int,
114// NX_ERR_*>. Possible errors:
115// NX_ERR_FILE_NOT_FOUND -- sys_read_file failed
116// NX_ERR_PARSE_FAILED -- malformed TPTP statement
117// NX_ERR_OVERFLOW -- file has more than NX_TPTP_LOAD_MAX_CLAUSES
118//
119// eq_sym: caller-supplied id reserved for equality predicate. Must be
120// outside the [NX_TPTP_SYM_BASE, NX_TPTP_SYM_BASE + NX_TPTP_SYM_MAX)
121// range so it doesn't collide with parser-allocated ids. 50 works.
122func nx_tptp_load_cnf_file(path: *u8, eq_sym: nx_int) -> *NxResult {
123 let len_p: *i64 = (sys_mmap(8)) as *i64
124 len_p[0] = 0
125 let r_read: *NxResult = nx_read_file_result(path, len_p)
126 if nx_result_is_err(r_read) == 1 { return r_read }
127 let buf: *u8 = nx_result_unwrap(r_read) as *u8
128 let n: nx_int = len_p[0]
129
130 let loaded: *TptpLoaded = (sys_mmap(NX_TPTP_LOADED_BYTES as i64)) as *TptpLoaded
131 loaded.clauses = (sys_mmap((NX_TPTP_LOAD_MAX_CLAUSES * NX_CLAUSE_BYTES) as i64)) as *Clause
132 loaded.n = 0
133 loaded.symtab = nx_tptp_symtab_new()
134
135 let pos: *nx_int = (sys_mmap(8)) as *nx_int
136 pos[0] = 0
137 let kind_buf: *u8 = sys_mmap(16)
138 let role_buf: *u8 = sys_mmap(64)
139 let name_buf: *u8 = sys_mmap(NX_TPTP_SYM_NAME_MAX as i64)
140
141 var done: nx_int = 0
142 while done == 0 {
143 nx_tptp_load_skip(buf, n, pos)
144 if pos[0] >= n { done = 1 }
145 if done == 0 {
146 // Read kind ("cnf" / "fof" / etc.; only "cnf" supported here).
147 let klen: nx_int = nx_tptp_load_read_ident(buf, n, pos, kind_buf)
148 if klen == 0 { done = 1 }
149 if done == 0 {
150 if nx_str_eq(kind_buf, "cnf" as *u8) != 1 { return nx_result_err(NX_ERR_PARSE_FAILED) }
151
152 // Expect '('
153 nx_tptp_load_skip(buf, n, pos)
154 if pos[0] >= n { return nx_result_err(NX_ERR_PARSE_FAILED) }
155 if buf[pos[0]] != 40 { return nx_result_err(NX_ERR_PARSE_FAILED) }
156 pos[0] = pos[0] + 1
157
158 // Read name
159 nx_tptp_load_skip(buf, n, pos)
160 let _nlen: nx_int = nx_tptp_load_read_ident(buf, n, pos, name_buf)
161
162 // Expect ','
163 nx_tptp_load_skip(buf, n, pos)
164 if pos[0] >= n { return nx_result_err(NX_ERR_PARSE_FAILED) }
165 if buf[pos[0]] != 44 { return nx_result_err(NX_ERR_PARSE_FAILED) }
166 pos[0] = pos[0] + 1
167
168 // Read role
169 nx_tptp_load_skip(buf, n, pos)
170 let _rlen: nx_int = nx_tptp_load_read_ident(buf, n, pos, role_buf)
171
172 // Expect ','
173 nx_tptp_load_skip(buf, n, pos)
174 if pos[0] >= n { return nx_result_err(NX_ERR_PARSE_FAILED) }
175 if buf[pos[0]] != 44 { return nx_result_err(NX_ERR_PARSE_FAILED) }
176 pos[0] = pos[0] + 1
177
178 // Parse formula body -- variables clause-local.
179 nx_tptp_symtab_reset_vars(loaded.symtab)
180 let c: *Clause = nx_tptp_parse_cnf_clause(buf, n, pos, loaded.symtab, eq_sym)
181 if (c as nx_int) == 0 { return nx_result_err(NX_ERR_PARSE_FAILED) }
182
183 // Store into output array.
184 if loaded.n >= NX_TPTP_LOAD_MAX_CLAUSES { return nx_result_err(NX_ERR_OVERFLOW) }
185 let dest: *Clause = ((loaded.clauses as nx_int) + (loaded.n * NX_CLAUSE_BYTES)) as *Clause
186 dest.n_lits = c.n_lits
187 dest.lits = c.lits
188 loaded.n = loaded.n + 1
189
190 // Expect ')' then '.'
191 nx_tptp_load_skip(buf, n, pos)
192 if pos[0] >= n { return nx_result_err(NX_ERR_PARSE_FAILED) }
193 if buf[pos[0]] != 41 { return nx_result_err(NX_ERR_PARSE_FAILED) }
194 pos[0] = pos[0] + 1
195 nx_tptp_load_skip(buf, n, pos)
196 if pos[0] >= n { return nx_result_err(NX_ERR_PARSE_FAILED) }
197 if buf[pos[0]] != 46 { return nx_result_err(NX_ERR_PARSE_FAILED) }
198 pos[0] = pos[0] + 1
199 }
200 }
201 }
202 return nx_result_ok(loaded as nx_int)
203}
204
205// Accessor: get the i-th loaded clause.
206func nx_tptp_loaded_at(l: *TptpLoaded, i: nx_int) -> *Clause {
207 if i < 0 { return 0 as *Clause }
208 if i >= l.n { return 0 as *Clause }
209 return ((l.clauses as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
210}