code wiki / (root) / nx_tptp_term.nx

nx_tptp_term.nx

buildroot/runtime/nx_tptp_term.nx

5140 B142 linesdepth 5pulls 8 transitivereach 15 importersview sourcekind librarytopic tptp
docsdependenciesstructsconstsfunctions

about

nx_tptp_term.nx -- TPTP term grammar -> *Term constructor. TPTP term grammar (subset, sufficient for CNF problems): term ::= variable | constant | function "(" term { "," term } ")" variable ::= [A-Z][A-Za-z0-9_]* constant ::= [a-z][A-Za-z0-9_]* function ::= [a-z][A-Za-z0-9_]* (constant with arguments) Caller passes (buf, length, *pos, symtab); on success the function returns the parsed *Term and advances *pos past the term. On parse failure returns null *Term (use nx_tptp_term_last_err to inspect).

dependencies 7 imports · 15 importers

nx_syscalls.nx nx_runtime.nx nx_tier.nx nx_str.nx nx_result.nx nx_unify.nx nx_tptp_symtab.nx nx_tptp_term.nx nx_avatar_solve_test.nx nx_casc_runner_test.nx nx_fof_cnf_test.nx nx_fof_parse.nx nx_fof_parse_test.nx nx_fof_tseitin_test.nx nx_solve.nx nx_solve_test.nx nx_tptp_emit_test.nx nx_tptp_formula.nx

diagram shows first 10 each side; +0 more imports, +5 more importers in the complete lists below.

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

imported by: nx_avatar_solve_test.nxnx_casc_runner_test.nxnx_fof_cnf_test.nxnx_fof_parse.nxnx_fof_parse_test.nxnx_fof_tseitin_test.nxnx_solve.nxnx_solve_test.nxnx_tptp_emit_test.nxnx_tptp_formula.nxnx_tptp_formula_test.nxnx_tptp_load.nxnx_tptp_load_any.nxnx_tptp_load_test.nxnx_tptp_write_test.nx

structs

none

consts

27const NX_TPTP_TERM_MAX_ARGS: nx_int = 8

functions

30func nx_tptp_term_skip_ws(buf: *u8, n: nx_int, pos: *nx_int)
51func nx_tptp_term_read_ident(buf: *u8, n: nx_int, pos: *nx_int, out_buf: *u8) -> nx_int
79func nx_tptp_parse_term(buf: *u8, n: nx_int, pos: *nx_int,