nx_tptp_emit.nx

buildroot/runtime/nx_tptp_emit.nx

8140 B206 linesdepth 6pulls 9 transitivereach 4 importersview sourcekind librarytopic tptp

docs dependencies structs consts functions

about

nx_tptp_emit.nx -- TPTP CNF emitter. Per Vampire-displacement roadmap Phase 2. Closes the substrate's TPTP I/O loop: nx_tptp_load reads CNF files; this writes them back. Lets the substrate round-trip, normalize, archive, or share intermediate clause sets in a tool-interchange format. Emit functions append to a caller-provided buffer. Caller pre-allocates and tracks the cursor position. API: nx_emit_term(t, symtab, buf, *pos, cap) nx_emit_literal(l, symtab, eq_sym, buf, *pos, cap) nx_emit_clause_body(c, symtab, eq_sym, buf, *pos, cap) nx_emit_cnf_stmt(c, name, role, symtab, eq_sym, buf, *pos, cap) All return number of bytes written; -1 on capacity overflow.

dependencies 8 imports · 4 importers

imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_str.nxnx_result.nxnx_unify.nxnx_resolution.nxnx_tptp_symtab.nx

imported by: nx_tptp_emit_test.nxnx_tptp_write_test.nxnx_tstp_emit.nxnx_tstp_emit_test.nx

structs

none

consts

157	const NX_TPTP_WRITE_BUF_CAP: nx_int = 32768

functions

35	func nx_emit_term(t: Term, symtab: TptpSymtab, buf: u8, pos: nx_int, cap: nx_int) -> nx_int; called by 2: nx_emit_term nx_emit_literal
38	func nx_emit_byte(b: nx_int, buf: u8, pos: nx_int, cap: nx_int) -> nx_int called by 5: nx_emit_str nx_emit_term nx_emit_literal nx_emit_clause_body nx_emit_cnf_stmt
46	func nx_emit_str(s: u8, buf: u8, pos: *nx_int, cap: nx_int) -> nx_int called by 4: nx_emit_term nx_emit_clause_body nx_emit_cnf_stmt nx_tstp_emit_clause calls 1: nx_emit_byte
56	func nx_emit_term(t: Term, symtab: TptpSymtab, buf: u8, pos: nx_int, cap: nx_int) -> nx_int calls 6: nx_tptp_var_name_at nx_emit_str nx_tptp_symtab_name_for nx_emit_byte nx_emit_term nx_term_arg
82	func nx_emit_literal(l: Literal, symtab: TptpSymtab, eq_sym: nx_int, called by 1: nx_emit_clause_body calls 3: nx_emit_term nx_term_arg nx_emit_byte
112	func nx_emit_clause_body(c: Clause, symtab: TptpSymtab, eq_sym: nx_int, called by 4: nx_emit_cnf_stmt roundtrip roundtrip_lit_count nx_tstp_emit_clause calls 4: nx_emit_str nx_emit_byte nx_clause_lit_at nx_emit_literal
133	func nx_emit_cnf_stmt(c: Clause, name: u8, role: *u8, called by 1: nx_tptp_write_cnf_file calls 3: nx_emit_str nx_emit_clause_body nx_emit_byte
159	func nx_int_to_decimal(n: nx_int, out: *u8) -> nx_int called by 1: nx_tptp_write_cnf_file calls 1: sys_mmap
178	func nx_tptp_write_cnf_file(path: u8, clauses: Clause, n: nx_int, called by 1: main calls 8: sys_openat_wr nx_result_err sys_mmap nx_int_to_decimal nx_emit_cnf_stmt sys_close+2