nx_tptp_symtab.nx
buildroot/runtime/nx_tptp_symtab.nx
about
nx_tptp_symtab.nx -- TPTP identifier -> integer id table.
Per Vampire-displacement roadmap Phase 1.6: feeds the formula
parser. Maps TPTP identifiers to the integer sym_id / var_id
space that nx_unify Term structs use.
TPTP convention:
First character UPPERCASE -> variable (X, Y, Var0)
First character lowercase -> function or predicate or constant
(arity is determined by use site)
Variables are scoped to a single clause in TPTP CNF semantics --
the parser MUST call nx_tptp_symtab_reset_vars between clauses to
give each clause fresh variable ids. Symbols persist globally so
the same predicate name in different clauses gets the same sym_id.
dependencies 5 imports · 20 importers
diagram shows first 10 each side; +0 more imports, +10 more importers in the complete lists below.
imports: nx_syscalls.nxnx_runtime.nxnx_tier.nxnx_str.nxnx_result.nx
imported by: nx_avatar_solve_test.nxnx_casc_runner_test.nxnx_fof_cnf.nxnx_fof_cnf_test.nxnx_fof_parse.nxnx_fof_parse_test.nxnx_fof_tseitin_test.nxnx_solve.nxnx_solve_test.nxnx_tptp_emit.nxnx_tptp_emit_test.nxnx_tptp_formula.nxnx_tptp_formula_test.nxnx_tptp_load.nxnx_tptp_load_any.nxnx_tptp_load_test.nxnx_tptp_term.nxnx_tptp_write_test.nxnx_tstp_emit.nxnx_tstp_emit_test.nx
structs
| 37 | struct TptpSymtab |
consts
| 29 | const NX_TPTP_SYM_MAX: nx_int = 256 |
| 30 | const NX_TPTP_SYM_NAME_MAX: nx_int = 64 |
| 31 | const NX_TPTP_VAR_MAX: nx_int = 64 |
| 35 | const NX_TPTP_SYM_BASE: nx_int = 1000 |
| 45 | const NX_TPTP_SYMTAB_BYTES: nx_int = 32 |
functions
| 47 | func nx_tptp_symtab_new() -> *TptpSymtab |
| 57 | func nx_tptp_symtab_reset_vars(st: *TptpSymtab) |
| 62 | func nx_tptp_is_variable_name(name: *u8) -> nx_int |
| 70 | func nx_tptp_sym_name_at(st: *TptpSymtab, i: nx_int) -> *u8 |
| 74 | func nx_tptp_var_name_at(st: *TptpSymtab, i: nx_int) -> *u8 |
| 81 | func nx_tptp_symtab_intern(st: *TptpSymtab, name: *u8) -> nx_int |
| 115 | func nx_tptp_symtab_name_for(st: *TptpSymtab, sym_id: nx_int) -> *u8 |