nx_tptp.nx
buildroot/runtime/nx_tptp.nx
about
nx_tptp.nx -- TPTP (Thousands of Problems for Theorem Provers) format
reader. Foundation for CASC competition entry.
Per user 2026-05-14: "we need to win our qed system must be a leap
forward from the bits up". TPTP at tptp.org defines the canonical
benchmark format every CASC entrant must read. This is bits-up:
no external Vampire/E/Otter dependency; pure NishiLang substrate.
TPTP FOF format (subset supported here):
fof(<name>, <role>, <formula>).
where:
<name> = identifier (a000_1, my_axiom, etc.)
<role> = axiom | hypothesis | conjecture | lemma | definition | ...
<formula> = first-order logic expression
CNF format:
cnf(<name>, <role>, <literal-disjunction>).
Subset implemented today: name + role extraction. Formula parsing
queued for nx_tptp_formula.nx (next session).
dependencies 5 imports · 1 importers
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_str.nxnx_result.nx
imported by: nx_tptp_test.nx
structs
| 72 | struct TptpStmt |
| 82 | struct TptpReader |
consts
| 35 | const NX_TPTP_ROLE_AXIOM: nx_int = 1 |
| 36 | const NX_TPTP_ROLE_HYPOTHESIS: nx_int = 2 |
| 37 | const NX_TPTP_ROLE_CONJECTURE: nx_int = 3 |
| 38 | const NX_TPTP_ROLE_LEMMA: nx_int = 4 |
| 39 | const NX_TPTP_ROLE_DEFINITION: nx_int = 5 |
| 40 | const NX_TPTP_ROLE_NEG_CONJ: nx_int = 6 |
| 41 | const NX_TPTP_ROLE_PLAIN: nx_int = 7 |
| 42 | const NX_TPTP_ROLE_UNKNOWN: nx_int = 0 |
| 67 | const NX_TPTP_KIND_FOF: nx_int = 1 |
| 68 | const NX_TPTP_KIND_CNF: nx_int = 2 |
| 69 | const NX_TPTP_KIND_THF: nx_int = 3 |
| 70 | const NX_TPTP_KIND_TFF: nx_int = 4 |
| 79 | const NX_TPTP_STMT_BYTES: nx_int = 32 |
| 91 | const NX_TPTP_MAX_STMTS: nx_int = 4096 |
| 92 | const NX_TPTP_READER_BYTES: nx_int = 40 |
| 93 | const NX_TPTP_IDENT_CAP: nx_int = 128 |
functions
| 44 | func nx_tptp_role_name(r: nx_int) -> *u8 called by 1: main |
| 55 | func nx_tptp_role_from_str(s: *u8) -> nx_int |
| 95 | func nx_tptp_reader_new(buf: *u8, n: nx_int) -> *TptpReader |
| 107 | func nx_tptp_skip_ws(r: *TptpReader) |
| 137 | func nx_tptp_read_ident(r: *TptpReader, out_buf: *u8) -> nx_int called by 1: nx_tptp_read_stmt |
| 159 | func nx_tptp_read_fml_raw(r: *TptpReader, out_start: *nx_int, out_end: *nx_int) -> nx_int calls 1: nx_tptp_skip_ws |
| 184 | func nx_tptp_read_stmt(r: *TptpReader) -> *NxResult called by 1: main calls 7: nx_tptp_skip_wsnx_result_errsys_mmapnx_tptp_read_identnx_str_eqnx_tptp_role_from_str+1 |
| 248 | func nx_tptp_n_stmts(r: *TptpReader) -> nx_int { return r.n_stmts } called by 1: main |
| 249 | func nx_tptp_stmt_at(r: *TptpReader, idx: nx_int) -> *TptpStmt called by 1: main |