nx_tptp_load_any.nx source
↩ module page · 207 lines · 9412 B
1// nx_tptp_load_any.nx -- TPTP loader handling both cnf(...) and fof(...).
2//
3// The original nx_tptp_load_cnf_file only handles CNF statements --
4// adequate for hand-written test files but not for real CASC TPTP-Easy
5// problems which are typically in FOF format. This loader auto-detects
6// per statement and routes:
7// cnf(...) -> nx_tptp_parse_cnf_clause (existing path)
8// fof(...) -> nx_fof_parse + nx_fof_to_cnf, expand into CNF clauses
9//
10// Role handling for FOF:
11// axiom / hypothesis / negated_conjecture / lemma / definition / plain
12// -> assert as-is (CNF-convert and append)
13// conjecture
14// -> NEGATE before CNF-converting (standard TPTP convention:
15// prove UNSAT of {axioms ∪ ¬conjecture})
16//
17// All native NishiLang.
18
19// nx_safety_envelope:
20// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
21// sil_target: SIL1
22// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
23// verdict: NOT_YET_EVALUATED
24
25import "nx_syscalls.nx"
26import "nx_runtime.nx"
27import "nx_tier.nx"
28import "nx_str.nx"
29import "nx_result.nx"
30import "nx_file_result.nx"
31import "nx_unify.nx"
32import "nx_resolution.nx"
33import "nx_tptp_symtab.nx"
34import "nx_tptp_term.nx"
35import "nx_tptp_formula.nx"
36import "nx_tptp_load.nx"
37import "nx_fof.nx"
38import "nx_fof_parse.nx"
39import "nx_fof_cnf.nx"
40import "nx_fof_tseitin.nx"
41
42const NX_LOAD_ANY_MAX_CLAUSES: nx_int = 256
43const NX_LOAD_ANY_FOF_CLAUSE_CAP: nx_int = 256
44
45// Build a new clause with duplicate literals removed. Required after
46// FOF->CNF distribution, which can produce {p, p} or {p, ~p} shapes
47// from constructs like (p|p) that arose from naive distribution of
48// nested ANDs. Without dedup, resolution can't reduce {p, p} to {p}
49// (factoring isn't wired into the discount loop's main path), so
50// trivial propositional cases get stuck. Dedup is a clean preprocessing
51// alternative.
52func nx_clause_dedup_lits(c: *Clause) -> *Clause {
53 let out: *Clause = nx_clause_new()
54 var i: nx_int = 0
55 while i < c.n_lits {
56 let li: *Literal = nx_clause_lit_at(c, i)
57 // Have we already added an identical literal?
58 var dup: nx_int = 0
59 var j: nx_int = 0
60 while j < out.n_lits {
61 let lj: *Literal = nx_clause_lit_at(out, j)
62 if li.sign == lj.sign {
63 if nx_term_eq(li.atom, lj.atom) == 1 { dup = 1 }
64 }
65 j = j + 1
66 }
67 if dup == 0 {
68 let _r: *NxResult = nx_clause_add(out, li)
69 }
70 i = i + 1
71 }
72 return out
73}
74
75func nx_tptp_load_any_file(path: *u8, eq_sym: nx_int) -> *NxResult {
76 let len_p: *i64 = (sys_mmap(8)) as *i64
77 len_p[0] = 0
78 let r_read: *NxResult = nx_read_file_result(path, len_p)
79 if nx_result_is_err(r_read) == 1 { return r_read }
80 let buf: *u8 = nx_result_unwrap(r_read) as *u8
81 let n: nx_int = len_p[0]
82
83 let loaded: *TptpLoaded = (sys_mmap(NX_TPTP_LOADED_BYTES as i64)) as *TptpLoaded
84 loaded.clauses = (sys_mmap((NX_LOAD_ANY_MAX_CLAUSES * NX_CLAUSE_BYTES) as i64)) as *Clause
85 loaded.n = 0
86 loaded.symtab = nx_tptp_symtab_new()
87
88 let pos: *nx_int = (sys_mmap(8)) as *nx_int
89 pos[0] = 0
90 let kind_buf: *u8 = sys_mmap(16)
91 let role_buf: *u8 = sys_mmap(64)
92 let name_buf: *u8 = sys_mmap(NX_TPTP_SYM_NAME_MAX as i64)
93
94 var done: nx_int = 0
95 while done == 0 {
96 nx_tptp_load_skip(buf, n, pos)
97 let p_after_skip: nx_int = pos[0]
98 if p_after_skip >= n { done = 1 }
99 if done == 0 {
100 let klen: nx_int = nx_tptp_load_read_ident(buf, n, pos, kind_buf)
101 if klen == 0 { done = 1 }
102 if done == 0 {
103 let is_cnf: nx_int = nx_str_eq(kind_buf, "cnf" as *u8)
104 let is_fof: nx_int = nx_str_eq(kind_buf, "fof" as *u8)
105 if is_cnf == 0 {
106 if is_fof == 0 { return nx_result_err(NX_ERR_PARSE_FAILED) }
107 }
108
109 // Expect '('
110 nx_tptp_load_skip(buf, n, pos)
111 if pos[0] >= n { return nx_result_err(NX_ERR_PARSE_FAILED) }
112 if buf[pos[0]] != 40 { return nx_result_err(NX_ERR_PARSE_FAILED) }
113 pos[0] = pos[0] + 1
114
115 // Read name
116 nx_tptp_load_skip(buf, n, pos)
117 let _nlen: nx_int = nx_tptp_load_read_ident(buf, n, pos, name_buf)
118
119 // Expect ','
120 nx_tptp_load_skip(buf, n, pos)
121 if pos[0] >= n { return nx_result_err(NX_ERR_PARSE_FAILED) }
122 if buf[pos[0]] != 44 { return nx_result_err(NX_ERR_PARSE_FAILED) }
123 pos[0] = pos[0] + 1
124
125 // Read role
126 nx_tptp_load_skip(buf, n, pos)
127 let _rlen: nx_int = nx_tptp_load_read_ident(buf, n, pos, role_buf)
128 let is_conj: nx_int = nx_str_eq(role_buf, "conjecture" as *u8)
129
130 // Expect ','
131 nx_tptp_load_skip(buf, n, pos)
132 if pos[0] >= n { return nx_result_err(NX_ERR_PARSE_FAILED) }
133 if buf[pos[0]] != 44 { return nx_result_err(NX_ERR_PARSE_FAILED) }
134 pos[0] = pos[0] + 1
135
136 if is_cnf == 1 {
137 // Parse formula body as CNF clause -- variables clause-local.
138 nx_tptp_symtab_reset_vars(loaded.symtab)
139 let c_raw: *Clause = nx_tptp_parse_cnf_clause(buf, n, pos, loaded.symtab, eq_sym)
140 if (c_raw as nx_int) == 0 { return nx_result_err(NX_ERR_PARSE_FAILED) }
141 let c: *Clause = nx_clause_dedup_lits(c_raw)
142 if loaded.n >= NX_LOAD_ANY_MAX_CLAUSES { return nx_result_err(NX_ERR_OVERFLOW) }
143 let dest: *Clause = ((loaded.clauses as nx_int) + (loaded.n * NX_CLAUSE_BYTES)) as *Clause
144 dest.n_lits = c.n_lits
145 dest.lits = c.lits
146 loaded.n = loaded.n + 1
147 }
148 if is_fof == 1 {
149 nx_tptp_symtab_reset_vars(loaded.symtab)
150 let f: *Fof = nx_fof_parse(buf, n, pos, loaded.symtab, eq_sym)
151 if (f as nx_int) == 0 { return nx_result_err(NX_ERR_PARSE_FAILED) }
152 // Conjecture: negate before CNF conversion. Standard
153 // TPTP convention is "prove UNSAT of axioms ∪ ¬conjecture".
154 var f_use: *Fof = f
155 if is_conj == 1 { f_use = nx_fof_neg(f) }
156 // Heuristic CNF strategy: if the formula has 4+ IFF/IMP
157 // nodes, distribute would blow up exponentially -- use
158 // Tseitin (linear-size). Otherwise distribute (fewer
159 // clauses on small formulas). Threshold tuned to keep
160 // simple Pelletier 1-9 on distribute (faster) and switch
161 // pel012-style 4-IFF formulas to Tseitin.
162 let n_iff_imp: nx_int = nx_fof_count_iff_imp(f_use)
163 let cnf_buf: *Clause = (sys_mmap((NX_LOAD_ANY_FOF_CLAUSE_CAP * NX_CLAUSE_BYTES) as i64)) as *Clause
164 let cnf_n_p: *nx_int = sys_mmap(8) as *nx_int
165 cnf_n_p[0] = 0
166 var rc: nx_int = 0
167 if n_iff_imp >= 4 {
168 let nnf_qf: *Fof = nx_fof_to_nnf_quantifier_free(f_use)
169 rc = nx_fof_to_cnf_tseitin(nnf_qf, cnf_buf, cnf_n_p, NX_LOAD_ANY_FOF_CLAUSE_CAP)
170 }
171 if n_iff_imp < 4 {
172 rc = nx_fof_to_cnf(f_use, cnf_buf, cnf_n_p, NX_LOAD_ANY_FOF_CLAUSE_CAP)
173 }
174 if rc != 0 { return nx_result_err(NX_ERR_PARSE_FAILED) }
175 // Append all generated CNF clauses to loaded, deduping
176 // literals on the way (FOF distribution can produce
177 // {p, p} shapes that resolution can't reduce without
178 // factoring being wired into the discount loop).
179 var k: nx_int = 0
180 while k < cnf_n_p[0] {
181 if loaded.n >= NX_LOAD_ANY_MAX_CLAUSES { return nx_result_err(NX_ERR_OVERFLOW) }
182 let src: *Clause = ((cnf_buf as nx_int) + (k * NX_CLAUSE_BYTES)) as *Clause
183 let deduped: *Clause = nx_clause_dedup_lits(src)
184 let dest2: *Clause = ((loaded.clauses as nx_int) + (loaded.n * NX_CLAUSE_BYTES)) as *Clause
185 dest2.n_lits = deduped.n_lits
186 dest2.lits = deduped.lits
187 loaded.n = loaded.n + 1
188 k = k + 1
189 }
190 }
191
192 // Expect ')' then '.'
193 nx_tptp_load_skip(buf, n, pos)
194 let p1: nx_int = pos[0]
195 if p1 >= n { return nx_result_err(NX_ERR_PARSE_FAILED) }
196 if buf[p1] != 41 { return nx_result_err(NX_ERR_PARSE_FAILED) }
197 pos[0] = p1 + 1
198 nx_tptp_load_skip(buf, n, pos)
199 let p2: nx_int = pos[0]
200 if p2 >= n { return nx_result_err(NX_ERR_PARSE_FAILED) }
201 if buf[p2] != 46 { return nx_result_err(NX_ERR_PARSE_FAILED) }
202 pos[0] = p2 + 1
203 }
204 }
205 }
206 return nx_result_ok(loaded as nx_int)
207}