nx_tptp_emit.nx source
↩ module page · 206 lines · 8140 B
1// nx_tptp_emit.nx -- TPTP CNF emitter.
2//
3// Per Vampire-displacement roadmap Phase 2. Closes the substrate's
4// TPTP I/O loop: nx_tptp_load reads CNF files; this writes them
5// back. Lets the substrate round-trip, normalize, archive, or
6// share intermediate clause sets in a tool-interchange format.
7//
8// Emit functions append to a caller-provided buffer. Caller
9// pre-allocates and tracks the cursor position.
10//
11// API:
12// nx_emit_term(t, symtab, buf, *pos, cap)
13// nx_emit_literal(l, symtab, eq_sym, buf, *pos, cap)
14// nx_emit_clause_body(c, symtab, eq_sym, buf, *pos, cap)
15// nx_emit_cnf_stmt(c, name, role, symtab, eq_sym, buf, *pos, cap)
16//
17// All return number of bytes written; -1 on capacity overflow.
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_unify.nx"
31import "nx_resolution.nx"
32import "nx_tptp_symtab.nx"
33
34// Forward declaration -- emit_term recurses on itself for arglists.
35func nx_emit_term(t: *Term, symtab: *TptpSymtab, buf: *u8, pos: *nx_int, cap: nx_int) -> nx_int;
36
37// Append one byte to buf at *pos. Returns 1 on success, -1 on overflow.
38func nx_emit_byte(b: nx_int, buf: *u8, pos: *nx_int, cap: nx_int) -> nx_int {
39 if pos[0] >= cap { return 0 - 1 }
40 buf[pos[0]] = b as u8
41 pos[0] = pos[0] + 1
42 return 1
43}
44
45// Append a null-terminated string. Returns count or -1.
46func nx_emit_str(s: *u8, buf: *u8, pos: *nx_int, cap: nx_int) -> nx_int {
47 var i: nx_int = 0
48 while s[i] != 0 {
49 if nx_emit_byte(s[i] as nx_int, buf, pos, cap) < 0 { return 0 - 1 }
50 i = i + 1
51 }
52 return i
53}
54
55// Emit one term, recursive.
56func nx_emit_term(t: *Term, symtab: *TptpSymtab, buf: *u8, pos: *nx_int, cap: nx_int) -> nx_int {
57 if t.kind == NX_TERM_VAR {
58 let name: *u8 = nx_tptp_var_name_at(symtab, t.sym)
59 return nx_emit_str(name, buf, pos, cap)
60 }
61 let name2: *u8 = nx_tptp_symtab_name_for(symtab, t.sym)
62 if (name2 as nx_int) == 0 { return 0 - 1 }
63 if nx_emit_str(name2, buf, pos, cap) < 0 { return 0 - 1 }
64 if t.kind == NX_TERM_CONST { return 1 }
65 // APP -- emit "(arg, arg, ...)"
66 if t.n_args == 0 { return 1 }
67 if nx_emit_byte(40, buf, pos, cap) < 0 { return 0 - 1 } // '('
68 var i: nx_int = 0
69 while i < t.n_args {
70 if i > 0 {
71 if nx_emit_byte(44, buf, pos, cap) < 0 { return 0 - 1 } // ','
72 if nx_emit_byte(32, buf, pos, cap) < 0 { return 0 - 1 } // ' '
73 }
74 if nx_emit_term(nx_term_arg(t, i), symtab, buf, pos, cap) < 0 { return 0 - 1 }
75 i = i + 1
76 }
77 if nx_emit_byte(41, buf, pos, cap) < 0 { return 0 - 1 } // ')'
78 return 1
79}
80
81// Emit one literal: optional "~", then atom OR "lhs = rhs" / "lhs != rhs".
82func nx_emit_literal(l: *Literal, symtab: *TptpSymtab, eq_sym: nx_int,
83 buf: *u8, pos: *nx_int, cap: nx_int) -> nx_int {
84 // Equality / inequality: special-cased so we emit "lhs = rhs"
85 // rather than "eq(lhs, rhs)" syntax.
86 if l.atom.kind == NX_TERM_APP {
87 if l.atom.sym == eq_sym {
88 if l.atom.n_args == 2 {
89 if nx_emit_term(nx_term_arg(l.atom, 0), symtab, buf, pos, cap) < 0 { return 0 - 1 }
90 if l.sign == NX_LIT_NEG {
91 if nx_emit_byte(32, buf, pos, cap) < 0 { return 0 - 1 } // ' '
92 if nx_emit_byte(33, buf, pos, cap) < 0 { return 0 - 1 } // '!'
93 if nx_emit_byte(61, buf, pos, cap) < 0 { return 0 - 1 } // '='
94 } else {
95 if nx_emit_byte(32, buf, pos, cap) < 0 { return 0 - 1 }
96 if nx_emit_byte(61, buf, pos, cap) < 0 { return 0 - 1 }
97 }
98 if nx_emit_byte(32, buf, pos, cap) < 0 { return 0 - 1 }
99 if nx_emit_term(nx_term_arg(l.atom, 1), symtab, buf, pos, cap) < 0 { return 0 - 1 }
100 return 1
101 }
102 }
103 }
104 // General predicate atom.
105 if l.sign == NX_LIT_NEG {
106 if nx_emit_byte(126, buf, pos, cap) < 0 { return 0 - 1 } // '~'
107 }
108 return nx_emit_term(l.atom, symtab, buf, pos, cap)
109}
110
111// Emit clause body: lit | lit | ...
112func nx_emit_clause_body(c: *Clause, symtab: *TptpSymtab, eq_sym: nx_int,
113 buf: *u8, pos: *nx_int, cap: nx_int) -> nx_int {
114 if c.n_lits == 0 {
115 // Empty clause -- TPTP convention "$false".
116 return nx_emit_str("$false" as *u8, buf, pos, cap)
117 }
118 var i: nx_int = 0
119 while i < c.n_lits {
120 if i > 0 {
121 if nx_emit_byte(32, buf, pos, cap) < 0 { return 0 - 1 } // ' '
122 if nx_emit_byte(124, buf, pos, cap) < 0 { return 0 - 1 } // '|'
123 if nx_emit_byte(32, buf, pos, cap) < 0 { return 0 - 1 }
124 }
125 let l: *Literal = nx_clause_lit_at(c, i)
126 if nx_emit_literal(l, symtab, eq_sym, buf, pos, cap) < 0 { return 0 - 1 }
127 i = i + 1
128 }
129 return 1
130}
131
132// Emit the full "cnf(name, role, body).\n" statement.
133func nx_emit_cnf_stmt(c: *Clause, name: *u8, role: *u8,
134 symtab: *TptpSymtab, eq_sym: nx_int,
135 buf: *u8, pos: *nx_int, cap: nx_int) -> nx_int {
136 if nx_emit_str("cnf(" as *u8, buf, pos, cap) < 0 { return 0 - 1 }
137 if nx_emit_str(name, buf, pos, cap) < 0 { return 0 - 1 }
138 if nx_emit_str(", " as *u8, buf, pos, cap) < 0 { return 0 - 1 }
139 if nx_emit_str(role, buf, pos, cap) < 0 { return 0 - 1 }
140 if nx_emit_str(", " as *u8, buf, pos, cap) < 0 { return 0 - 1 }
141 if nx_emit_clause_body(c, symtab, eq_sym, buf, pos, cap) < 0 { return 0 - 1 }
142 if nx_emit_byte(41, buf, pos, cap) < 0 { return 0 - 1 } // ')'
143 if nx_emit_byte(46, buf, pos, cap) < 0 { return 0 - 1 } // '.'
144 if nx_emit_byte(10, buf, pos, cap) < 0 { return 0 - 1 } // '\n'
145 return 1
146}
147
148// Write a sequence of CNF clauses to disk at `path`. Each clause
149// gets a generated name "c0", "c1", ... and the role "axiom" -- the
150// caller can supply different name/role schemes by emitting via
151// nx_emit_cnf_stmt directly.
152//
153// Returns Result<bytes_written, NX_ERR_*>:
154// NX_ERR_FILE_NOT_FOUND -- open failed
155// NX_ERR_OVERFLOW -- buffer cap (32 KiB) exceeded
156// NX_ERR_INVALID_STATE -- short write
157const NX_TPTP_WRITE_BUF_CAP: nx_int = 32768
158
159func nx_int_to_decimal(n: nx_int, out: *u8) -> nx_int {
160 if n == 0 { out[0] = 48 as u8; out[1] = 0; return 1 }
161 var len: nx_int = 0
162 var v: nx_int = n
163 let tmp: *u8 = sys_mmap(32)
164 while v > 0 {
165 tmp[len] = ((v - ((v / 10) * 10)) + 48) as u8
166 v = v / 10
167 len = len + 1
168 }
169 var i: nx_int = 0
170 while i < len {
171 out[i] = tmp[len - 1 - i]
172 i = i + 1
173 }
174 out[len] = 0
175 return len
176}
177
178func nx_tptp_write_cnf_file(path: *u8, clauses: *Clause, n: nx_int,
179 symtab: *TptpSymtab, eq_sym: nx_int) -> *NxResult {
180 let fd: i64 = sys_openat_wr(path, 0o644 as i64)
181 if fd < 0 { return nx_result_err(NX_ERR_FILE_NOT_FOUND) }
182
183 let buf: *u8 = sys_mmap(NX_TPTP_WRITE_BUF_CAP as i64)
184 let pos: *nx_int = sys_mmap(8) as *nx_int
185 pos[0] = 0
186 let name_buf: *u8 = sys_mmap(32)
187
188 var i: nx_int = 0
189 while i < n {
190 let c: *Clause = ((clauses as nx_int) + (i * NX_CLAUSE_BYTES)) as *Clause
191 // Build "c<i>" name.
192 name_buf[0] = 99 as u8 // 'c'
193 let _nl: nx_int = nx_int_to_decimal(i, ((name_buf as nx_int) + 1) as *u8)
194 if nx_emit_cnf_stmt(c, name_buf, "axiom" as *u8, symtab, eq_sym,
195 buf, pos, NX_TPTP_WRITE_BUF_CAP) < 0 {
196 let _close1: i64 = sys_close(fd)
197 return nx_result_err(NX_ERR_OVERFLOW)
198 }
199 i = i + 1
200 }
201
202 let written: i64 = sys_write(fd, buf, pos[0] as i64)
203 let _close: i64 = sys_close(fd)
204 if written != (pos[0] as i64) { return nx_result_err(NX_ERR_INVALID_STATE) }
205 return nx_result_ok(written)
206}